section\Introduction\ text\This is the second assessed exercise for the L21 ``Interactive Formal Verification'' MPhil course in academic year 2017--2018. In this exercise you will prove some properties of structures called metric spaces and two closely associated concepts: continuity and open balls. The exercise will test your ability to write structured proofs, work with sets and quantifiers, and carefully select relevant auxiliary lemmas and introduction and elimination principles to make theorem proving easier. Indeed, all proofs should be written as Isar structured proofs, as far as possible. Concretely, the marking scheme for this exercise is as follows (out of a total of 100): \<^item> \textbf{50 marks} for correct definitions, lemma statements and structured proofs, in accordance with the distribution of marks outlined in the body of this document, \<^item> \textbf{30 marks} for extra proofs of properties about metric spaces, continuity and open balls presented in this exercise, more definitions related to metric spaces and properties about them, or the use of features of Isabelle not lectured in class, or similar along these lines. Any reasonable evidence that you have gone ``above and beyond'' in your use of Isabelle will be considered here, and obviously the more ambitious you are, the more marks you accrue, \<^item> \textbf{20 marks} for a nice writeup detailing all decisions made in your choice of lemmas, proof strategies, and so on, and an explanation as to what extensions you have decided to implement, or novel features of Isabelle that you have used, to merit some of the 30 marks mentioned above. Your submissions should be submitted electronically on the L21 Moodle site before 4pm Cambridge local time on submission day. See the course website for submission dates for the two assessed exercises. Submissions should consist of an edited version of the theory file that this document is based on (also available from the course website) that includes your solutions to the exercises contained within, along with a PDF document containing your writeup. Your writeup need not be especially long---2 sides of A4 will suffice---but it should be detailed, describing auxilliary lemmas and definitions that you introduced, if any, design decisions, and so on. Late submissions will of course be penalised, and as always students should not confer with each other when answering the sheet. \paragraph{Before beginning:} for those who have not encountered metric spaces before it may be a good idea for you to skim-read the Wikipedia article on the subject to familiarise yourself with key concepts before beginning.\footnote{See \url{https://en.wikipedia.org/wiki/Metric_space}} However, the exercises have been written in such a way that consulting any such background material on metric spaces is not strictly necessary, with enough background information embedded within this document to help you through. \pagebreak\ section\Metric spaces, and some examples\ text\As the definition of metric spaces relies crucially on the real numbers, we will be working with the Isabelle/HOL theory \texttt{Complex\_Main}---rather than the more usual \texttt{Main}---for this exercise. This theory imports an implementation of the real and complex numbers, as well as associated definitions and theorems:\ theory Assessed_Exercise_Two_Questions imports Complex_Main begin text\Consider the distance between any two points in $\mathbb{R}^{3}$, the absolute distance between two integers, or the Lehvenstein (edit) distance between a pair of strings. Many mathematical objects have a notion of distance associated with them---and some even have multiple different reasonable notions of distance. \emph{Metric spaces} are intended as an abstraction of all of these notions of distance, and of our own informal understanding of this concept. Formally, a metric space $\langle C, \delta \rangle$ is a carrier set $C$ paired with a \emph{metric} (or distance) function $\delta : C \times C \rightarrow \mathbb{R}$ that intuitively represents the distance between any two points of the carrier set, $C$. We can capture this structure in Isabelle/HOL using a record with two fields, one corresponding to the carrier, and the other to the metric function:\ record 'a metric_space = carrier :: "'a set" metric :: "'a \ 'a \ real" text\I note here that, differing slightly from the standard mathematical presentation, I have Curried the metric function in the Isabelle/HOL modelling of a metric space. This is a minor difference that has no impact on the theory. Also, I use Isabelle's type polymorphism to express an ambivalence in the type of the contents of the carrier set. As a supposed generalisation of our intuitive notion of distance, a metric function must satisfy a number of important laws, or properties, in order for the pair $\langle C, \delta \rangle$ to be a valid metric space. These are as follows: \<^item> It makes no sense to state that one object is a negative distance from some other object: distances are only ever zero or positive, and never negative. Therefore the real number returned by a metric space's metric function for any two points must be non-negative. \<^item> The distance travelled when walking from Cambridge to St.~Neots is the same as the distance travelled when walking from St.~Neots to Cambridge. Generalising, the distance between a point $x$ and a point $y$ must be the same as the distance between the point $y$ and the point $x$. That is: a metric space's metric function is \emph{symmetric}, \<^item> The distance between any two points is zero if and only if the two points are identical. This law is a little harder to justify intuitively, as in natural language we often say that the distance between two touching objects is zero. However, if we think of the elements of the carrier set as ``points'' with no internal volume then the axiom asserts that any two co-located points are identical, \<^item> There are no shortcuts: a metric function must capture the \emph{shortest} distance between any two points. The distance travelled when travelling from point $x$ to $z$ via an intermediary point $y$ must be at least as long as the distance travelled simply moving between points $x$ and $z$ directly. The third law above is sometimes known as the ``identity of indiscernibles'', whilst the last law is sometimes referred to as the ``triangular inequality''. These laws can be easily captured as a HOL predicate on \texttt{metric\_space} records, asserting that a carrier set and metric function pairing constitute a valid metric space:\ definition metric_space :: "'a metric_space \ bool" where "metric_space M \ (\x\carrier M. \y\carrier M. metric M x y \ 0) \ (\x\carrier M. \y\carrier M. metric M x y = metric M y x) \ (\x\carrier M. \y\carrier M. metric M x y = 0 \ x = y) \ (\x\carrier M. \y\carrier M. \z\carrier M. metric M x z \ metric M x y + metric M y z)" text\Note here that I use the same name, \texttt{metric\_space}, to denote both the underlying type of metric space records as well as the predicate asserting that those records correctly model a metric space. This does not matter---the two names live in different namespaces. Now that we have a suitable set of definitions for modelling metric spaces in Isabelle/HOL we can begin showing that some concrete carrier set and metric function pairings are indeed valid metric spaces. As a first example, a metric space can be constructed from the set of real numbers by taking the distance between any two reals, $j$ and $k$, to be their absolute difference, $\mid j - k \mid$. We can capture this by defining a suitable instance of the \texttt{metric\_space} record:\ definition real_abs_metric_space :: "real metric_space" where "real_abs_metric_space \ \ carrier = UNIV, metric = \x y. abs (x - y) \" text\Note here that the carrier set of the metric space is \texttt{UNIV}, the universal set. Isabelle correctly infers that this has type \texttt{real} \texttt{set} as the type of \texttt{real\_abs\_metric\_space} has been constrained to the type \texttt{real} \texttt{metric\_space}. Now that we have a pairing of a carrier set and metric function, we must show that this pairing is indeed a valid metric space. We do this by proving that the \texttt{metric\_space} predicate holds of this record. \textbf{Exercise (4 marks)}: prove that the predicate \texttt{metric\_space} holds of \texttt{real\_abs\_metric\_space} by proving the following theorem. That is, replace the \texttt{oops} command below with a complete structured proof.\ theorem shows "metric_space real_abs_metric_space" oops text\The set of real numbers can be lifted into a metric space in another way, using the so-called \emph{British Rail metric} which models the tendency of all rail journeys between any two points in the United Kingdom to proceed by first travelling to London, and then travelling onwards. (The French call this the \emph{SNCF metric} due to a similar tendency in Metropolitan France.) This metric space can again be captured quite easily in Isabelle/HOL, by following the same pattern as before. \textbf{Exercise (4 marks)}: prove that the predicate \texttt{metric\_space} holds of \texttt{br\_metric\_space} by proving the following theorem. That is, replace the \texttt{oops} command below with a complete structured proof.\ definition br_metric_space :: "real metric_space" where "br_metric_space \ \ carrier = UNIV, metric = \x y. if x = y then 0 else abs x + abs y \" theorem shows "metric_space br_metric_space" oops text\As a final example, we consider endowing pairs of integers with a metric. For pairs of integers $(i_1, j_1)$ and $(i_2, j_2)$ one can use $\mid i_1 - i_2 \mid + \mid j_1 - j_2 \mid$ as a metric---sometimes called the taxicab metric. Proving that this is a valid metric space is a little more involved than the other two examples, due to fiddling with pairs, but still fairly straightforward. \textbf{Exercise (5 marks)}: prove that the predicate \texttt{metric\_space} holds of \texttt{taxicab\_metric\_space} by proving the following theorem. That is, replace the \texttt{oops} command below with a complete structured proof.\ definition taxicab_metric_space :: "(int \ int) metric_space" where "taxicab_metric_space \ \ carrier = UNIV, metric = \p1 p2. abs (fst p1 - fst p2) + abs (snd p1 - snd p2) \" theorem shows "metric_space taxicab_metric_space" oops section\Making new metric spaces from old\ text\We now have a handful of concrete metric spaces. Given such a collection of existing metric spaces, can we produce new metric spaces using generic constructions? That is, are there operations that take an arbitrary metric space and can produce new ones? In this section, we explore three different ways of building new metric spaces from old: restricting a metric space to a subset of the carrier, shifting a metric via a non-zero constant, and finally taking the product of two metric spaces. The first two are relatively straightforward: \textbf{Exercise (3 marks)}: Suppose $\langle C, \delta\rangle$ is a metric space and suppose $S \subseteq C$. Show that $\langle S, \delta \rangle$ is also a metric space by stating and proving (with a structured proof) a relevant lemma. \textbf{Exercise (3 marks)}: Suppose $\langle C, \delta \rangle$ is a metric space. Suppose also that $k>0$ and that $\delta' (x, y) = k \cdot \delta (x, y)$. Show that $\langle C, \delta' \rangle$ is a metric space by stating and proving (with a structured proof) a relevant lemma. Lastly, we consider taking the product of two metric spaces. Recall that mathematically $S \times T$ denotes the \emph{Cartesian product} of two sets, consisting of all ordered pairs $(s, t)$ where $s \in S$ and $t \in T$. \textbf{Exercise (5 marks)}: Suppose $\langle S, \delta_1\rangle$ and $\langle T, \delta_2\rangle$ are metric spaces. Show that the set $S \times T$ can be lifted into a metric space by first finding a suitable metric and thereafter proving (with a strucured proof) a relevant lemma. Your metric on $S \times T$ must make use of both $\delta_1$ and $\delta_2$.\ section\Continuous functions, and some examples\ text\One reason why metric spaces are mathematically interesting is because they provide an abstract venue within which one can define the important notion of \emph{continuous function}, a core concept in topology and analysis. Indeed, metric spaces can be seen as a precursor to topology. Suppose that $\langle S, \delta_1\rangle$ and $\langle T, \delta_2\rangle$ are metric spaces, and $f : S \rightarrow T$ is a function mapping elements of $S$ to $T$. Suppose also that $s \in S$ is a point in $S$. We say that the function $f$ is \emph{continuous at the point $s$} if for every $\epsilon>0$ there exists $d>0$ such that $\delta_1 (x, s) < d$ then $\delta_2 (f x, f s) < \epsilon$ for all $x \in S$. Further, call the function $f : S \rightarrow T$ \emph{continuous} if $f$ is continuous at every point $s \in S$. These two definitions can be captured in Isabelle/HOL as follows:\ context fixes M1 :: "'a metric_space" and M2 :: "'b metric_space" begin definition continuous_at :: "('a \ 'b) \ 'a \ bool" where "continuous_at f a \ \\>0. (\d>0. \x\carrier M1. metric M1 x a < d \ metric M2 (f x) (f a) < \)" definition continuous :: "('a \ 'b) \ bool" where "continuous f \ \x\carrier M1. continuous_at f x" end text\As an aside, here I use a \texttt{context} block to fix two arbitrary metric spaces---\texttt{M1} and \texttt{M2}---of the correct type for the duration of my definitions. This means that I do not need to add the two metric spaces as explicit parameters to the \texttt{continuous\_at} and \texttt{continuous} functions but can declare them as parameters ``up front''. Inspect the type of the definitions to see what \texttt{context} does:\ term continuous_at term continuous text\Which functions are continuous? One obvious contender is the identity function. Suppose $\langle S, \delta\rangle$ is a metric space. Then the identity function $id : S \rightarrow S$ maps elements of the carrier $S$ onto elements of the carrier $S$---that is, the identity function can be seen as a map from a metric space back onto itself. \textbf{Exercise (3 marks)}: show that the identity function $id$ is a continuous function between a metric space and itself by stating and proving (with a strucured proof) a relevant lemma. Constant functions are also continuous. Suppose $\langle S, \delta_1\rangle$ and $\langle T, \delta_2\rangle$ are metric spaces and $t \in T$ is a point in $T$. Suppose also that $f : S \rightarrow T$ maps all $s$ to $t$ (i.e. it is a constant function that always returns $t$). Then $f$ is continuous. \textbf{Exercise (4 marks)}: show that constant functions are continuous by proving the following lemma. That is, replace the \texttt{oops} command below with a complete structured proof.\ lemma continuous_const: assumes "metric_space M1" and "metric_space M2" and "y \ carrier M2" shows "continuous M1 M2 (\x. y)" oops text\Lastly, suppose $\langle S, \delta_1\rangle$, $\langle T, \delta_2\rangle$, and $\langle U, \delta_3\rangle$ are metric spaces. Suppose also that $f : S \rightarrow T$ and $g : T \rightarrow U$ are continuous functions between relevant metric spaces. Then, providing that for every $s \in S$ we have $f s \in T$ holds, the composition $(g \circ f) : S \rightarrow U$ is also a continuous function between the metric spaces $\langle S, \delta_1\rangle$ and $\langle U, \delta_3\rangle$. \textbf{Exercise (6 marks)}: show that the composition of two continuous functions is continuous by proving the following lemma. That is, replace the \texttt{oops} command below with a complete structured proof.\ lemma continuous_comp: assumes "metric_space M1" and "metric_space M2" and "metric_space M3" and "continuous M1 M2 f" and "continuous M2 M3 g" and "\x. x \ carrier M1 \ f x \ carrier M2" shows "continuous M1 M3 (g o f)" oops section\Open balls\ text\Suppose $\langle S, \delta\rangle$ is a metric space and $c \in S$ is a point in $S$. Suppose also that $r>0$ is some strictly positive real number. Define the \emph{open ball of radius $r$ around the point $c$} as the set of all points in $S$ that are strictly less than $r$ distance away from the point $c$ when measured using the metric $\delta$. Where the underlying metric space is obvious, I will write $\mathcal{B}(c,r)$ for the open ball around point $c$ of radius $r$. \textbf{Exercise (2 marks)}: Suppose $\langle S, \delta\rangle$ is a metric space. Define the open ball $\mathcal{B}(c,r)$ in this metric space by completing the definition of \texttt{open\_ball}. That is, replace the \texttt{consts} declaration below with a complete definition.\ consts open_ball :: "'a metric_space \ 'a \ real \ 'a set" text\For any open ball $\mathcal{B}(c,r)$ in a metric space $\langle S, \delta\rangle$ we have that $\mathcal{B}(c,r) \subseteq S$, i.e. open balls are always subsets of the underlying metric space's carrier set. This fact holds for any ball of any radius. \textbf{Exercise (2 marks)}: show that an arbitrary open ball in a fixed metric space is a subset of that metric space's carrier set by stating and proving (with a structured proof) a relevant lemma. Moreover, we have that in a fixed metric space, the open ball $\mathcal{B}(c,0) = \{\}$. That is, open balls of zero radius are the empty set. \textbf{Exercise (2 marks)}: show that an open ball in a fixed metric space with radius $0$ is the empty set. Additionally, it should be intuitively obvious that for any open ball in a fixed metric space $\mathcal{B}(c, r)$ where $r > 0$ we have the property that $c \in \mathcal{B}(c, r)$, i.e. the open ball contains its own centre as a point. \textbf{Exercise (3 marks)}: show that any open ball in a fixed metric space with strictly positive radius contains its centre as a point by proving the following lemma. That is, replace the \texttt{oops} command below with a complete structured proof.\ lemma centre_in_open_ball: assumes "metric_space M" and "c \ carrier M" and "0 < r" shows "c \ open_ball M c r" oops text\Lastly, suppose we have two open balls around the same centre point---$\mathcal{B}(c, r)$ and $\mathcal{B}(c, s)$---such that $r \leq s$ where $c$ is contained within some ambient fixed metric space. Then it should be obvious that the open ball with smaller radius is a subset of the open ball with the larger radius. \textbf{Exercise (4 marks)}: show that an open ball around a fixed centre point with a smaller radius than another open ball around the same fixed centre point is a subset of the latter open ball by proving the following theorem. That is, replace the \texttt{oops} command below with a complete structured proof.\ lemma open_ball_le_subset: assumes "metric_space M" and "c \ carrier M" and "r \ s" shows "open_ball M c r \ open_ball M c s" oops end text\ \begin{center} \emph{The end\ldots} \end{center}\