Porting libraries of mathematics between proof assistants
[general Isabelle Archive of Formal Proofs HOL system HOL Light Coq In 2005, a student arrived who wanted to do a PhD involving formalised probability theory. I advised him to use HOL4, where theories of Lebesgue integration and probability theory had already been formalised; they were not available in Isabelle/HOL. Ironically, he eventually discovered that the HOL4 theories didn’t meet his requirements and he was forced to redo them. This episode explains why I have since devoted so much effort to porting libraries into Isabelle/HOL. But note: Isabelle/HOL already had, from 2004, a full copy of the HOL4 libraries, translated by importer tools. I never even thought of using these libraries, and they were quietly withdrawn in 2012. Why was that? And what is the right way to achieve interoperability between proof assistant libraries?
Libraries of mathematics
Just as the significance of a platform is determined by its application base, the significance of a proof assistant is largely determined by its libraries:
- Mathematical Components (among others) for Coq;
- mathlib for Lean;
- the Archive of Formal Proofs for Isabelle.
- John Harrison’s Euclidean spaces and “top 100 theorems” for HOL Light
- Although Mizar introduced a groundbreaking mathematical language, for many researchers the real attraction was the huge Mizar Mathematical Library.
Many people thought it wasteful to have so many overlapping but incompatible libraries. The proprietors of newer systems were naturally covetous of the accumulated wealth of older systems. This feeling was particularly strong among the various implementations of higher-order logic, one single formalism if we ignore each implementation’s bells and whistles. Powerful and efficient importers were built, e.g. by Obua and Skalberg, but they didn’t catch on. Despite that, research in this area continues.
I am not optimistic for the prospects of this sort of library porting, for a simple reason: we need the actual proofs. All the attempts that I have seen involve finding a lowest-common-denominator calculus for two different proof assistants and thus to emulate proofs in one system using proofs in the other. Ideally, corresponding basic libraries (e.g. of the natural numbers) are identified and matched rather than translated. Still, the very best one can hope for is a list of statements certified by the importer as having been proved somewhere, somehow. This isn’t satisfying.
Porting proofs from HOL Light to Isabelle/HOL
HOL Light is famous for its huge multivariate analysis library: nearly 300,000 lines of code and 13,000 theorems. I spent a lot of time between 2015 and 2017 porting great chunks of this material. It might seem an odd use of my time. I had spent years away from Isabelle working on MetiTarski, then returned to Isabelle to prove Gödel’s incompleteness theorems, and then—with a couple of big grant proposals falling short—found myself at a loose end.
The HOL Light library was definitely valuable, or so people told me. Regrettably, my knowledge of multivariate analysis is minimal, and please don’t utter the word “homology”.
I was ideally suited to this porting task: HOL Light is astonishingly retro, hardly different from Cambridge LCF as I left it in 1984.
Aspects of the work could be automated through Perl scripts and the porting of routine material was actually kind of relaxing, like doing a crossword (only much easier).
And oh! The nostalgia of seeing REPEAT GEN_TAC (which dates to Edinburgh LCF)
and “conversions” and “theorem continuations” (my own weird babies).
I seldom had to actually run HOL Light in order to see what was going on in a proof except for a few exceptionally long, ghastly or treacherous HOL Light scripts.
Two variables called x but with different types? No problem.
I could even figure out such horrors as
FIRST_ASSUM(ASSUME_TAC o MATCH_MP OPEN_IN_IMP_SUBSET)
The Isabelle analysis library today contains approximately 10,000 named theorems, including Cauchy’s integral and residue theorems, the Liouville theorem, the open mapping and domain invariance theorems, the maximum modulus principle and the Krein-Milman theorem. This represents 100-200K lines of HOL Light proofs (the wretched homology development alone is 11,400 lines). The material was ported by a variety of people. But for my sins, I think I ported the bulk of it.
Working through an example
At 50 lines, the following HOL Light proof counts as medium-sized. It’s not trivial, but neither is it in any way difficult. All you need is persistence.
let HOMEOMORPHIC_PUNCTURED_SPHERE_AFFINE_GEN = prove
(`!s:real^N->bool t:real^M->bool a.
convex s /\ bounded s /\ a IN relative_frontier s /\
affine t /\ aff_dim s = aff_dim t + &1
==> (relative_frontier s DELETE a) homeomorphic t`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `s:real^N->bool = {}` THEN
ASM_SIMP_TAC[AFF_DIM_EMPTY; AFF_DIM_GE; INT_ARITH
`--(&1):int <= s ==> ~(--(&1) = s + &1)`] THEN
MP_TAC(ISPECL [`(:real^N)`; `aff_dim(s:real^N->bool)`]
CHOOSE_AFFINE_SUBSET) THEN REWRITE_TAC[SUBSET_UNIV] THEN
REWRITE_TAC[AFF_DIM_GE; AFF_DIM_LE_UNIV; AFF_DIM_UNIV; AFFINE_UNIV] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real^N->bool` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN `~(t:real^N->bool = {})` MP_TAC THENL
[ASM_MESON_TAC[AFF_DIM_EQ_MINUS1]; ALL_TAC] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM MEMBER_NOT_EMPTY] THEN
DISCH_THEN(X_CHOOSE_TAC `z:real^N`) THEN STRIP_TAC THEN
MP_TAC(ISPECL
[`s:real^N->bool`; `ball(z:real^N,&1) INTER t`]
HOMEOMORPHIC_RELATIVE_FRONTIERS_CONVEX_BOUNDED_SETS) THEN
MP_TAC(ISPECL [`t:real^N->bool`; `ball(z:real^N,&1)`]
(ONCE_REWRITE_RULE[INTER_COMM] AFF_DIM_CONVEX_INTER_OPEN)) THEN
MP_TAC(ISPECL [`ball(z:real^N,&1)`; `t:real^N->bool`]
RELATIVE_FRONTIER_CONVEX_INTER_AFFINE) THEN
ASM_SIMP_TAC[CONVEX_INTER; BOUNDED_INTER; BOUNDED_BALL; CONVEX_BALL;
AFFINE_IMP_CONVEX; INTERIOR_OPEN; OPEN_BALL;
FRONTIER_BALL; REAL_LT_01] THEN
SUBGOAL_THEN `~(ball(z:real^N,&1) INTER t = {})` ASSUME_TAC THENL
[REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_INTER] THEN
EXISTS_TAC `z:real^N` THEN ASM_REWRITE_TAC[CENTRE_IN_BALL; REAL_LT_01];
ASM_REWRITE_TAC[] THEN REPEAT(DISCH_THEN SUBST1_TAC) THEN SIMP_TAC[]] THEN
REWRITE_TAC[homeomorphic; LEFT_IMP_EXISTS_THM] THEN
MAP_EVERY X_GEN_TAC [`h:real^N->real^N`; `k:real^N->real^N`] THEN
STRIP_TAC THEN REWRITE_TAC[GSYM homeomorphic] THEN
TRANS_TAC HOMEOMORPHIC_TRANS
`(sphere(z,&1) INTER t) DELETE (h:real^N->real^N) a` THEN
CONJ_TAC THENL
[REWRITE_TAC[homeomorphic] THEN
MAP_EVERY EXISTS_TAC [`h:real^N->real^N`; `k:real^N->real^N`] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [HOMEOMORPHISM]) THEN
REWRITE_TAC[HOMEOMORPHISM] THEN STRIP_TAC THEN REPEAT CONJ_TAC THENL
[ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; DELETE_SUBSET];
ASM SET_TAC[];
ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; DELETE_SUBSET];
ASM SET_TAC[];
ASM SET_TAC[];
ASM SET_TAC[]];
MATCH_MP_TAC HOMEOMORPHIC_PUNCTURED_AFFINE_SPHERE_AFFINE THEN
ASM_REWRITE_TAC[REAL_LT_01; GSYM IN_INTER] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [HOMEOMORPHISM]) THEN
ASM SET_TAC[]]);;
I should mention that I often had little grasp of the mathematics. Convex and bounded sets are simple enough. Affine? No idea. Affine dimension presumably has something to do with dimensions in linear algebra, and at the start of this work I had never come across the word homeomorphism. I did manage to learn bits and pieces while porting all this material, and I’m pretty sure that this particular theorem generalises the well-known fact that a punctured sphere can be continuously flattened to a plane: the so-called stereographic projection.
The proof script is typical of HOL Light.
Formidable though it appears, every proof is a combination of backward reasoning from the goal and forward reasoning from the assumptions, and a close look will reveal these steps.
However, the lack of a structured language means that the same effect might be obtained in strikingly different ways.
We see in the first line case analysis on whether the set s is empty, though in reality the assumptions imply that it is nonempty. Calls to MP_TAC typically involve inserting instances of previous theorems into the list of assumptions (I invented this technique, may God forgive me), when our task is to find the corresponding theorem in the Isabelle library
(porting it if it is not there) and first proving the corresponding instances of its premises, which can be read off from the explicit instance given here by ISPECL.
The line beginning DISCH_THEN(X_CHOOSE_THEN notes an existential claim from the theorem just instantiated. (Those are theorem continuations.)
Sometimes the proofs are nested but we can keep going, hoping that an induction formula is not being generated dynamically, because then you often can’t see what the induction is all about.
This process is largely mechanical, which is why I could port proofs that I didn’t understand. That’s why I believe that the future of proof porting must involve the porting of proofs at a high level, where we can see the structure of the result—and not by translating the primitive inferences of a calculus.
For this example, the result of my largely ignorant and mechanical translation at least resembles mathematics:
proposition homeomorphic_punctured_sphere_affine_gen: fixes a :: "'a :: euclidean_space" assumes "convex S" "bounded S" and a: "a ∈ rel_frontier S" and "affine T" and affS: "aff_dim S = aff_dim T + 1" shows "rel_frontier S - {a} homeomorphic T" proof - obtain U :: "'a set" where "affine U" "convex U" and affdS: "aff_dim U = aff_dim S" using choose_affine_subset [OF affine_UNIV aff_dim_geq] by (meson aff_dim_affine_hull affine_affine_hull affine_imp_convex) have "S ≠ {}" using assms by auto then obtain z where "z ∈ U" by (metis aff_dim_negative_iff equals0I affdS) then have bne: "ball z 1 ∩ U ≠ {}" by force then have [simp]: "aff_dim(ball z 1 ∩ U) = aff_dim U" using aff_dim_convex_Int_open [OF ‹convex U› open_ball] by (fastforce simp add: Int_commute) have "rel_frontier S homeomorphic rel_frontier (ball z 1 ∩ U)" by (rule homeomorphic_rel_frontiers_convex_bounded_sets) (auto simp: ‹affine U› affine_imp_convex convex_Int affdS assms) also have "... = sphere z 1 ∩ U" using convex_affine_rel_frontier_Int [of "ball z 1" U] by (simp add: ‹affine U› bne) finally have "rel_frontier S homeomorphic sphere z 1 ∩ U" . then obtain h k where him: "h ` rel_frontier S = sphere z 1 ∩ U" and kim: "k ` (sphere z 1 ∩ U) = rel_frontier S" and hcon: "continuous_on (rel_frontier S) h" and kcon: "continuous_on (sphere z 1 ∩ U) k" and kh: "⋀x. x ∈ rel_frontier S ⟹ k(h(x)) = x" and hk: "⋀y. y ∈ sphere z 1 ∩ U ⟹ h(k(y)) = y" unfolding homeomorphic_def homeomorphism_def by auto have "rel_frontier S - {a} homeomorphic (sphere z 1 ∩ U) - {h a}" proof (rule homeomorphicI) show h: "h ` (rel_frontier S - {a}) = sphere z 1 ∩ U - {h a}" using him a kh by auto metis show "k ` (sphere z 1 ∩ U - {h a}) = rel_frontier S - {a}" by (force simp: h [symmetric] image_comp o_def kh) qed (auto intro: continuous_on_subset hcon kcon simp: kh hk) also have "... homeomorphic T" by (rule homeomorphic_punctured_affine_sphere_affine) (use a him in ‹auto simp: affS affdS ‹affine T› ‹affine U› ‹z ∈ U››) finally show ?thesis . qed
In the Isabelle proof, we can see that the first step is to obtain an affine and convex set U. We prove the set S to be nonempty and from that obtain a specific element z belonging to U.
The argument continues with intelligible steps:
a chain of sets all homeomorphic to one another.
The ported proof is not only more legible than the original but it’s actually shorter, at 42 lines instead of 50; this doesn’t always happen.
A WLOG example
Many proofs contain the phrase without loss of generality. Sometimes it’s a mere appeal to symmetry: if $x\not=y$ then it is okay to assume that in fact $x<y$, provided the claim being proved is unchanged when $x$ and $y$ are swapped. The concept of WLOG is impossible to make precise; it involves an intuitive feeling that the essence of the proof of some statement is also present in the proof of some similar statement. Remember, all theorems are equivalent.
John Harrison’s paper “Without Loss of Generality” describes a suite of tactics in HOL Light for handling common cases of WLOG reasoning, with a focus on geometry. They are powerful tools in the hands of a HOL Light user and a nasty surprise to somebody trying to port these proofs. They transform the goal in a way that is often hard to work out in your head, creating one of the few occasions when it’s really necessary to launch HOL Light to figure out what is going on.
The following example states that a connected set in Euclidean space is uncountable if it contains two distinct points $a$ and $b$. The first step assumes that $b$ lies on the Origin, and the second step assumes that $a$ lies on the unit circle. Damn.
let CARD_EQ_CONNECTED = prove
(`!s a b:real^N.
connected s /\ a IN s /\ b IN s /\ ~(a = b) ==> s =_c (:real)`,
GEOM_ORIGIN_TAC `b:real^N` THEN GEOM_NORMALIZE_TAC `a:real^N` THEN
REWRITE_TAC[NORM_EQ_SQUARE; REAL_POS; REAL_POW_ONE] THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM CARD_LE_ANTISYM] THEN CONJ_TAC THENL
[TRANS_TAC CARD_LE_TRANS `(:real^N)` THEN
SIMP_TAC[CARD_LE_UNIV; CARD_EQ_EUCLIDEAN; CARD_EQ_IMP_LE];
TRANS_TAC CARD_LE_TRANS `interval[vec 0:real^1,vec 1]` THEN CONJ_TAC THENL
[MATCH_MP_TAC(ONCE_REWRITE_RULE[CARD_EQ_SYM] CARD_EQ_IMP_LE) THEN
SIMP_TAC[UNIT_INTERVAL_NONEMPTY; CARD_EQ_INTERVAL];
REWRITE_TAC[LE_C] THEN EXISTS_TAC `\x:real^N. lift(a dot x)` THEN
SIMP_TAC[FORALL_LIFT; LIFT_EQ; IN_INTERVAL_1; LIFT_DROP; DROP_VEC] THEN
X_GEN_TAC `t:real` THEN STRIP_TAC THEN
MATCH_MP_TAC CONNECTED_IVT_HYPERPLANE THEN
MAP_EVERY EXISTS_TAC [`vec 0:real^N`; `a:real^N`] THEN
ASM_REWRITE_TAC[DOT_RZERO]]]);;
This is one of those occasions when it’s best to give up. Because I could understand what the theorem was claiming, I could find another proof. It’s actually more general than the original, holding for all metric spaces. It relies on the fact that the function $d(a,{-})$, which maps an arbitrary $x$ to its distance $d(a,x)$ from $a$ is continuous, reducing the uncountability of $S$ to that of the closed interval $[0,d(a,b)]$. Remember that the operator ( ` ) denotes image, so dist a ` S denotes the image of $d(a,{-})$ under $S$. This image is uncountable, so the conclusion follows.
lemma connected_uncountable: fixes S :: "'a::metric_space set" assumes "connected S" "a ∈ S" "b ∈ S" "a ≠ b" shows "uncountable S" proof - have "continuous_on S (dist a)" by (intro continuous_intros) then have "connected (dist a ` S)" by (metis connected_continuous_image ‹connected S›) then have "closed_segment 0 (dist a b) ⊆ (dist a ` S)" by (simp add: assms closed_segment_subset is_interval_connected_1 is_interval_convex) then have "uncountable (dist a ` S)" by (metis ‹a ≠ b› countable_subset dist_eq_0_iff uncountable_closed_segment) then show ?thesis by blast qed
Concluding thoughts
A big drawback of these analysis libraries, both the HOL Light originals and the ported versions, is that the use of types was focused much more on convenience than flexibility. Already HOL Light include some attempts to generalise the material beyond $\mathbb{R}^n$, and the same is needed in Isabelle/HOL. Fortunately, because the ported proofs have a legible structure, the effort needed to do this might not be too great. Anybody who wants to steal the Isabelle/HOL library will have the advantage (compared with stealing from HOL Light) that the mathematical argument is right in front of their eyes.
As for the story that started this blog post, some people have asked me how I could allow one of my own students to use something other than Isabelle. The reason is this: while we researchers should eat our own dog food, we shouldn’t force it on others.