Email Gateway (Dec 15 2022 at 16:03): Email Gateway (Dec 15 2022 at 16:03):From: Frédéric Blanqui <frederic.blanqui@inria.fr>
Dear all,
I am very pleased to announce that one can now export all the proofs of
the Isabelle/HOL library (that is up to Complex_Main) to the Dedukti and
Lambdapi languages, using the Isabelle component
https://github.com/Deducteam/isabelle_dedukti.
This allows cross-checking of Isabelle developments. There are also
ongoing works for translating Dedukti files to other systems like Coq,
Lean, PVS or Agda.
Generating the proof terms takes about 47 minutes to Isabelle on my laptop.
The translation to Dedukti or Lambdapi takes about 26 minutes.
The verification of all the generated Dedukti files (4.5 Go) takes about
3 minutes with kocheck -j 7.
This currently works with Isabelle-2021-1 only. We hope to update it to
Isabelle-2022 in the coming months. Help is very welcome!
This is the result of several contributors: Makarius Wenzel, Michael
Färber, Yann Leray, Akihisa Yamada, Jérémy Dubut, that I want to thank
very much.
Best regards,
Frédéric Blanqui.
Useful links:
Isabelle_Dedukti: https://github.com/Deducteam/isabelle_dedukti
Dedukti: https://github.com/Deducteam/dedukti
Lambdapi: https://github.com/Deducteam/lambdapi
Kocheck: https://github.com/01mf02/kontroli-rs
Email Gateway (Dec 19 2022 at 08:36):From: Nicolas Méric <nicolas.meric@lri.fr>
Dear Frédéric,
I looked at the code of the exporter, and I do not understand the
initialization of the build options
(https://github.com/Deducteam/isabelle_dedukti/blob/0f25057f268c13c9c6e6699512370442a71d5ff6/src/exporter.scala#L30).
I thought that setting the record_proofs session option to 2 had the same
meaning as enabling the export_standard_proofs option, but in the code
Makarius chose, for both cases, that is if export_standard_proofs is set or
not, to have the record_proofs option set to 2.
Do you know why he did that?
I quickly looked at the sources of Isabelle, and both export_standard_proofs
and record_proofs=2 seem to set Proofterm.proofs to 2.
Best regards,
Nicolas Méric
Email Gateway (Dec 27 2022 at 09:59):From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Dear Frédéric,
I have done some proofterm exporting myself (to Lean, work-in-progress),
and I was wondering whether your exporting relates one issue that I
encountered.
In Isabelle (or maybe specifically Isabelle/HOL), definitions are
outside the trusted kernel. When a definition (e.g., *definition "a =
1"*) is encountered, an axiom is simply added (in this case *a::'a::one
= 1*). It is possible to even give several definitions for the same
constant on different types (i.e., we could end up with axioms *a::nat =
1* and a::int = 2 at the same time). This is used under the hood in
the type-class mechanism, and can also be accessed directly.
The question is how to handle definitions when exporting proofterms. One
obvious solution is to simply treat definitions like any other axiom,
and simply add them in the exported theory as axioms. However, this
seems to defeat the purpose of external checking of Isabelle proofs
(i.e., when we do not trust the Isabelle implementation). Namely, there
is no guarantee that these axioms will be consistent. (I am aware that
there are proofs that the Isabelle/HOL definitional framework with
typeclasses that these axiomatizations are a conservative extension but
that does not guarantee that the Isabelle implementation does it
correctly, and in my understanding, the point of external checking is
not to trust the existing implementation.)
The second obvious idea would be to replace definitional axioms by
proper definitions. That is, in the target logic, we would have
something that says that a is basically an abbreviation for 1.
However, this would need a target logic with overloading or with type
equality checks. (For example, if I translate the example above into a
definition, I would have to write something like *a ('a) := if 'a=nat
then 1::nat else if 'a=int then 2::int else undefined*('a). (Here I am
writing the type variables as arguments to a and undefined as an
explicit argument ('a) for clarity.) If I want to use those
definitions in exported proofs, I will have to use facts like *nat !=
int* which are probably unprovable in many logics and might be unsound
in logics that have provable parametricity.
The third idea (which I am using in my approach) is to process the
proofs to get rid of all the overloading first (after all, it's a
conservative extension). For example, in the above example, we end up
with definition a_nat := 1 and a_int := 2 and then all theorems need
to be rewritten to use one or the other, or, if the theorem is stated at
a larger type, take an all-quantified argument a and be proven for all
a. Doing this in practice isn't straightforward, but it seems to work
(work-in-progress!).
So I wonder how you deal with this difficulty in your formalization. Do
you export definitions as trusted axioms or do you use a different approach?
Best wishes,
Dominique.
Last updated: Oct 31 2025 at 16:27 UTC