23
$\begingroup$

Is there any way to easily translate proofs from one proof assistant to another? If so, how does it work?

Credit to: Kevin Buzzard's question.
Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ The Flyspeck project came close with their translation from Isabelle/HOL to HOL Light, but they translated only propositoins, not proofs. $\endgroup$
    – Joachim Breitner
    Commented Feb 9, 2022 at 13:06

7 Answers 7

Reset to default
26
$\begingroup$

Gaëtan Gilbert was able to translate Lean's library into Coq.

However, note that this is a translation at the level of proof terms, not proof scripts: in order to prove a theorem in Lean, you usually write a proof script using tactics (such as intro, or cases), and Lean will compile it down to a proof term that can be checked by Lean's kernel. The translation happens after the compilation phase, and will produce a proof term that can be checked by Coq's kernel, not a readable proof script for Coq.

So, how does this work? While Lean and Coq's tactics and idioms are quite different, it turns out that their proof terms are very similar, as their internal logics are both based on the Calculus of Inductive Constructions. There are some subtle differences, however: the universes are not handled in the exact same way, and Lean has definitional quotients as well as elimination rules for proof-irrelevant types that are not supported by vanilla Coq. But Coq can be modified to handle these, making it into a Lean type-checker.

Improve this answer
$\endgroup$
2
  • $\begingroup$ But wouldn't that mean that Lean is not translated into Coq, but rather that Lean is translated into a patch of Coq that implements Lean's logic? $\endgroup$
    – Dominique Unruh
    Commented Mar 4, 2022 at 10:35
  • $\begingroup$ If I understand correctly, the only required tweak in Coq's kernel is the "definitional UIP" which did not exist in the main branch at the time but is now available as a flag ( coq.inria.fr/doc/addendum/sprop.html#definitional-uip ). Everything else is optional (conversion checking flag) or happens in the outer layers of the software. $\endgroup$
    – Loïc Pujet
    Commented Mar 4, 2022 at 19:10
16
$\begingroup$

Some impressive work was done a while ago by Chantal Keller, which translated the entirety of HOL Light's library into Coq.

On the face of it, HOL is close to being a subset of the underlying logic of Coq (with some classical axioms), but the technical challenges were non-trivial: because HOL systems usually do not keep proof objects, there can be a size explosion in the translation, which must create them.

Another interesting point is that a "naive" translation would give unintelligible statements from HOL, with its own natural numbers, quantifiers, etc, but Chantal came up with a way to send some definitions to their appropriate targets.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Do you have a short description of her alignment method? This is by far the hardest part of any translation and I’m curious how it works, especially if it is in any way automatic. $\endgroup$
    – Jason Rute
    Commented Feb 10, 2022 at 1:52
  • $\begingroup$ No short description, I'm afraid. It involves some user-supplied input, see Section 11.4 of her dissertation: lri.fr/~keller/Documents-recherche/Publications/thesis13.pdf $\endgroup$
    – cody
    Commented Feb 10, 2022 at 15:30
14
$\begingroup$

Mario Carneiro also has worked on this with Metamath Zero, which can directly translate proofs to Lean. As Loïc mentioned, though, this is a term-wise translation, which means that the code between the two libraries won't interact well; for example, the two ring types would be different, and won't work together directly without more glue.

A similar example is mathport, which attempts to copy proofs from Lean3 to Lean4. This is done at many levels, but the hope is that eventually only the tactic level is needed; however, for example, tactics need to be ported by hand, so this is far from automatic.

Improve this answer
$\endgroup$
9
$\begingroup$

I would discourage people to do so, unless the proofs and theorems are super simple (like natural number properties). Reasons:

  1. In different systems, there are (nontrivially) different ways to represent certain things. For example, quotients in Lean and cubical Agda and Arend are all different from each other (they have different computation rules). It's very very hard for a translation algorithm to work across these differences.
  2. The type theories and design philosophy are mostly likely to be different. For instance, in Agda, the identity type lives in Type, but in Coq (and maybe Lean), the identity type lives in Prop (and note that Coq Prop and Lean Prop are different in strictness). This can make proofs in Agda to not work in other systems, or vice versa. Not to mention simple type theory proofs and dependent type theory proofs.
  3. A translated theorem can be hard to use, because the best practices of different systems can be different. For example, mathlib embraces classical math, so probably constructivists will not appreciate proofs translated from there. Also, the translated proofs can be hard to read.

What I do found useful, is to implement similar tactics among systems, then translate the tactics automatically and check them against manually translated theorems. By that we "translate" theorems but in a supervised manner. I think this should be useful, but people haven't done it as far as I know. I plan to do this in Aya.

Improve this answer
$\endgroup$
3
  • $\begingroup$ To add to that, the translate proofs probably looks ugly without proper tactic translation or styling supervision. I think there's a project translating Metamath to Lean, which produces incomprehensible proofs. $\endgroup$
    – Trebor ♦
    Commented Feb 9, 2022 at 12:41
  • 2
    $\begingroup$ A slightly pessimistic answer, and “I would advise against it” is not really an answer to the question of “is there a way”. $\endgroup$
    – Joachim Breitner
    Commented Feb 9, 2022 at 13:06
  • $\begingroup$ @JoachimBreitner I think the last paragraph answers $\endgroup$
    – ice1000 ♦
    Commented Feb 9, 2022 at 13:09
7
$\begingroup$

So around 2003-2008 (approximately), there was one effort (not sure what happened to it), to have a common host/packaging system for sharing proofs between systems, with the working name "Logosphere". A bunch of talks and working notes seem to be around online, but the underlying effort seems to have evaporated. I suspect someone could message Carsten Schürmann and ask about it! (I met him Fall of 2005 and he was pretty cool)

Here's some related papers that come up!

  • Meta-Logical Frameworks and Formal Digital Libraries by Carsten Schürmann (pdf)
  • Proofs “R” Us by Frank Pfenning (pdf)
  • Logosphere - A Digital Library of Formal Proof by Carsten Schürmann (pdf)
Improve this answer
$\endgroup$
1
  • $\begingroup$ thank you for the helpful cleanup edits! :) $\endgroup$
    – Carter Tazio Schonwald
    Commented Feb 10, 2022 at 22:23
7
$\begingroup$

I am aware of certain efforts of this nature within the Isabelle/HOL community.

(Automated translation of theorems from HOL4 to Isabelle/HOL)

  • Immler F, Rädle J, Wenzel M. Virtualization of HOL4 in Isabelle. In: Harrison J, O’Leary J, Tolmach A, editors. Proceedings of the 10th International Conference on Interactive Theorem Proving. 2019.

(Automated translation of theorems from Isabelle/HOL to Isabelle/ZF)

  • Krauss A, Schropp A. A Mechanized Translation from Higher-Order Logic to Set Theory. In: Kaufmann M, Paulson LC, editors. Proceedings of the First International Conference on Interactive Theorem Proving, ITP 2010, Edinburgh, UK, July 11-14, 2010. Heidelberg, Germany: Springer; 2010. p. 323–38. (Lecture Notes in Computer Science; vol. 6172).

(Involves translation of theorems from Mizar to HOTG = Isabelle/HOL + Tarski-Grothendieck Set Theory, but I am not certain about the status of this project and the level of automation that was used: it seems like this is an ongoing effort; I encourage you to correct me if you know more)

  • Kaliszyk C, Pąk K. Semantics of Mizar as an Isabelle Object Logic. Journal of Automated Reasoning. 2019;63(3):557–95.
  • Brown CE, Kaliszyk C, Pak K. Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. In: Harrison J, O’Leary J, Tolmach A, editors. 10th International Conference on Interactive Theorem Proving (ITP 2019). Portland, USA; 2019. p. 9:1-9:16.
  • https://bitbucket.org/cezaryka/tyset/src
Improve this answer
$\endgroup$
6
$\begingroup$

"Is there any way to easily translate proofs from one proof assistant to another? If so, how does it work?"

From the Logopedia About webpage:

"Some proofs expressed in some Dedukti theories can be translated to other proof systems, such as HOL Light, HOL 4 , Isabelle / HOL , Coq , Matita , Lean , PVS ...".

Logipedia boils down to translating proofs into Dedukti.

Currently, this is possible for:

Not always entirely automatic, and not yet complete, but it translates between several proof formats.

See also:

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.