Porting the HOL Light metric space library
[general Isabelle sledgehammer locales HOL Light I’m sorry that there have been no posts since April. I’ve been busy with a side project: porting the HOL Light metric space library to Isabelle in time for the upcoming release. It was a big job: the chunk I grabbed initially comprised some 1335 lemmas, over 24K lines and nearly 1.2M bytes. Some of the lemmas turned out to have been ported previously, or otherwise turned out to be unnecessary; on the other hand, quite a few additional lemmas were needed. The material included metric spaces and many associated concepts, advanced material about toplogical spaces, the relationships among different kinds of spaces, and finally closure properties, especially under general products. Major contributions include Urysohn’s lemma and the Tietze extension theorem, the Baire Category Theorem and the Banach Fixed-Point Theorem.
But what about the existing typeclass for metric spaces?
It’s worth recalling that Isabelle/HOL already includes a huge amount of material ported from HOL Light, a lot of it about metric spaces and including results bearing the names of Urysohn and Tietze. These relate to the metric space type class, which governs types that can be seen as metric spaces, including real norned vector spaces and Euclidean spaces, and in particular $\mathbb{R}^n$. However, type classes only work for types, and many interesting metric spaces cannot be expressed as types. By working more abstractly, we can work with metric spaces over arbitrary carrier sets.
Declaring metric spaces as a locale
The HOL Light version defines an abstract type of metric spaces, which is given as an argument to the numerous metric space operations. This approach is flexible when we need to mix several metric space constructions. However, it’s clunky when working within a single metric space, which is so often done. The best way to handle that situation is through a locale: a packaged context that can be re-entered at any time. The metric space locale declares the carrier set (M) and the distance function (d).
locale Metric_space = fixes M :: "'a set" and d :: "'a ⇒ 'a ⇒ real" assumes nonneg [simp]: "⋀x y. 0 ≤ d x y" assumes commute: "⋀x y. d x y = d y x" assumes zero [simp]: "⋀x y. ⟦x ∈ M; y ∈ M⟧ ⟹ d x y = 0 ⟷ x=y" assumes triangle: "⋀x y z. ⟦x ∈ M; y ∈ M; z ∈ M⟧ ⟹ d x z ≤ d x y + d y z"
Working within the locale, declaring concepts such as open balls is straightforward.
We can treat M and d as constants, and their governing assumptions as axioms:
definition mball where "mball x r ≡ {y. x ∈ M ∧ y ∈ M ∧ d x y < r" lemma centre_in_mball_iff [iff]: "x ∈ mball x r ⟷ x ∈ M ∧ 0 < r" using in_mball mdist_zero by force lemma mball_subset_mspace: "mball x r ⊆ M" by auto
It also works for rather more sophisticated proofs, such as the uniqueness of fixed points of a contraction mapping. The theorem statement is surprisingly natural, and the proof shown below can be found (thanks to sledgehammer) by a single mouse click.
lemma (in Metric_space) contraction_imp_unique_fixpoint: assumes "f x = x" "f y = y" and "f ∈ M → M" and "k < 1" and "⋀x y. ⟦x ∈ M; y ∈ M⟧ ⟹ d (f x) (f y) ≤ k * d x y" and "x ∈ M" "y ∈ M" shows "x = y" by (smt (verit, ccfv_SIG) mdist_pos_less mult_le_cancel_right1 assms)
Locales nest naturally, as when we introduce the notion of a subspace of a metric space:
locale Submetric = Metric_space + fixes A assumes subset: "A ⊆ M" sublocale Submetric ⊆ sub: Metric_space A d by (simp add: subset subspace)
The declaration above state that every submetric can be viewed as a metric space in its own right.
An abstract type of metric spaces
Although the locale-based approach is general – you work outside the locale merely by quoting the desired values of M and d every time – it can get tedious, especially when working with multiple metric spaces.
So it’s helpful to follow HOL Light in also declaring an abstract type of metric spaces.
typedef 'a metric = "{(M::'a set,d). Metric_space M d}" morphisms "dest_metric" "metric" proof - have "Metric_space {} (λx y. 0)" by (auto simp: Metric_space_def) then show ?thesis by blast qed definition mspace where "mspace m ≡ fst (dest_metric m)" definition mdist where "mdist m ≡ snd (dest_metric m)"
We can prove a few results linking the two levels. It’s then easy to switch back to the locale approach at any point in a proof, starting with any available metric space.
lemma Metric_space_mspace_mdist [iff]: "Metric_space (mspace m) (mdist m)" by (metis Product_Type.Collect_case_prodD dest_metric mdist_def mspace_def) lemma (in Metric_space) mspace_metric[simp]: "mspace (metric (M,d)) = M" by (simp add: mspace_def Metric_space_axioms metric_inverse) lemma (in Metric_space) mdist_metric[simp]: "mdist (metric (M,d)) = d" by (simp add: mdist_def Metric_space_axioms metric_inverse)
Declaring a few of the most frequently used concepts (here, the associated topology) for the abstract type makes it even easier to work at the most appropriate level:
definition mtopology_of :: "'a metric ⇒ 'a topology" where "mtopology_of ≡ λm. Metric_space.mtopology (mspace m) (mdist m)" lemma topspace_mtopology_of [simp]: "topspace (mtopology_of m) = mspace m" by (simp add: Metric_space.topspace_mtopology Metric_space_mspace_mdist mtopology_of_def)
I must confess, I was not always certain which way was best. Fortunately, such decisions are not committal, and I frequently started by proving a theorem within the locale, from which the abstract type analogue could immediately be optained.
Interoperability with the type class level
Having declared the Metric_space locale, my development immediately
interprets it using the type class version.
What’s going on not obvious; the clue is dist, which is the distance function for the
metric_space type class.
We’ve just established that anything involving the type class now applies as well to the more general locale framework.
interpretation Met_TC: Metric_space UNIV dist by (simp add: dist_commute dist_triangle Metric_space.intro)
Now the equivalence between the type class and locale concepts is proved trivially:
lemma mball_eq_ball [simp]: "Met_TC.mball = ball" by force lemma mopen_eq_open [simp]: "Met_TC.mopen = open" by (force simp: open_contains_ball Met_TC.mopen_def) lemma limitin_iff_tendsto [iff]: "limitin Met_TC.mtopology σ x F = tendsto σ x F" by (simp add: Met_TC.mtopology_def) lemma mtopology_is_euclidean [simp]: "Met_TC.mtopology = euclidean" by (simp add: Met_TC.mtopology_def)
And so, simplification alone will drop us from the locale level to the type class level whenever this is possible: that is, whenever the carrier set is actually a type.
The role of type classes is a key difference between simply typed and dependent typed formalisms. Type classes play a bigger role in the latter (but with the risk of performance issues and the impossibility of multiple inheritance); with the former, we may be stuck with having to duplicate some proofs.
On the horrors of HOL Light proofs
I commented on the tribulations last time. But seriously:
- Why would you use
xas a Cauchy sequence and a real number in the same formula, just because you can? - Why would you generate an induction formula through an opaque series of transformations when you could simply type it in?
- Why would you instantiate a lemma by applying syntactic functions to the current goal when you could simply type in the necessary terms?
- Why unfold all definitions at once, turning your nice concise goal into a full page of formulas?
Well, in HOL Light that’s how you roll.
A ubiquitous horror is MP_TAC,
introduced by yours truly around 1984. It stuffs a given theorem $T$
into the current goal $G$ to create the implication $T\Longrightarrow G$.
Typically $T$ would have been produced from something else, by instantiation at least, and is about to undergo rewriting and other transformations.
(In HOL Light, as in its predecessors, the simplifier never alters a goal’s assumptions, which is why we want $T$ in the goal formula itself.)
Having simplified $T$ to say $T_1\land T_2$, the following tactic might move one of them to the assumptions (via ASSUME_TAC)
and put back the other, via another MP_TAC call, to work on some more.
It’s basically a stack machine computation, slowly massaging the goal into T (true).
Some of these proofs are grimly incomprehensible.
Then the next proof might consist of a pleasant string of SUBGOAL_TAC calls,
almost as nice as an Isabelle proof.
Sometimes I was able to port proofs just by eyeballing the HOL Light versions, but often I had to run them in a HOL Light session, occasionally line by line. Sledgehammer did most of the work, and half the time I had no idea what the actual argument was. Well, I don’t really need to know.