Is it possible to translate Coq to Isabelle (and Lean) using Dedukti?

brando90 commented 3 years ago

Is it possible to translate Coq to Isabelle using Dedukti?

fblanqui commented 3 years ago

In theory, yes. We currently have a translator from Coq to Dk/Coq, the instance of Dedukti with the encoding of Coq logic. See https://github.com/Deducteam/CoqInE . We also have tools to translate proofs from Dk/Coq to Dk/STTfa. See https://github.com/Deducteam/universo. Finally, we have a translator from Dk/STTfa to OpenTheory. See https://github.com/Deducteam/Logipedia. I believe that Isabelle/HOL can read OpenTheory files but I am not sure of the current status of this. Anyway, it would be better to extend Logipedia to directly output Isabelle/HOL from Dk/STTfa (this is already done for PVS; so it should not be very difficult). So, most of the tools are already available to translate Coq files to Isabelle/HOL files. What is missing is to glue them together and automate this tool chain. If you are interested in contributing to this, you are very welcome!

brando90 commented 3 years ago

In theory, yes. We currently have a translator from Coq to Dk/Coq, the instance of Dedukti with the encoding of Coq logic. See https://github.com/Deducteam/CoqInE . We also have tools to translate proofs from Dk/Coq to Dk/STTfa. See https://github.com/Deducteam/universo. Finally, we have a translator from Dk/STTfa to OpenTheory. See https://github.com/Deducteam/Logipedia. I believe that Isabelle/HOL can read OpenTheory files but I am not sure of the current status of this. Anyway, it would be better to extend Logipedia to directly output Isabelle/HOL from Dk/STTfa (this is already done for PVS; so it should not be very difficult). So, most of the tools are already available to translate Coq files to Isabelle/HOL files. What is missing is to glue them together and automate this tool chain. If you are interested in contributing to this, you are very welcome!

Yes I am interested! Let my try to write it as a list so I know how to execute this:

translate Coq to Dk
translate Dk to STTfa
translate STTfa to OpenTheory
check if Isabelle can open OpenTheory files.

is this how this is done? I want to try it if this is what has to be done. How long do you estimate it takes to do in time (to get a feel while I am doing it if I am on the right path or stuck)?

brando90 commented 3 years ago

Anyway, it would be better to extend Logipedia to directly output Isabelle/HOL from Dk/STTfa (this is already done for PVS; so it should not be very difficult).

I think this sounds different from your first suggestion. It does sound better to output Isabelle directly but I have to admit I have no idea how to even start doing that. If you have a suggestion (more concrete outline of what is needed) that might be helpful but myself being a non-expert in PL and TP I am unsure if I could actually do it myself. Let me know if you have a more concrete plan for this so I can assess what is easiest/tractable for me to do.

brando90 commented 3 years ago

@fblanqui do you have a small OpenTheory file I can use to test point 4?

btw this looks useful: http://www.gilith.com/opentheory/ and this too https://github.com/gilith/opentheory

brando90 commented 3 years ago

With the risk of making this thread harder to follow...Is it possible to do HOLight to Isabelle using Dedukti?

I am interested in translating as many of these to Isabelle as possible:

http://www.cs.ru.nl/F.Wiedijk/100/index.html

Perhaps we can focus with Coq to Isabelle first and then we can explore the rest later.

brando90 commented 3 years ago

Sorry for yet another comment. Would it translate the proofs too or just the statements? Since isabelle has "two modes" (at least in my head). Isar/declarative vs apply style scripts.

fblanqui commented 3 years ago

Le 06/10/2020 à 16:46, brando90 a écrit :

Sorry for yet another comment. Would it translate the proofs too or just the statements? Since isabelle has "two modes" (at least in my head). Isar/declarative vs apply style scripts.

Coqine translates Coq proof terms as recorded in vo files, not proof scripts. So, what you will get in Isabelle or any other prover is a low-level proof, which is not aimed at being read by humans.

fblanqui commented 3 years ago

Le 06/10/2020 à 14:12, brando90 a écrit :

Is it possible to do HOLight to HOL using Dedukti?

HOL-Light and HOL both use OpenTheory I believe, which is a low-level proof format for higher-order logic. So, it should be possible to translated proofs from one to the other by simply using OpenTheory.

But it should also be possible to use Dedukti as well:

1) You can already translate OpenTheory files to Dedukti/STTfa by using https://github.com/Deducteam/Holide. Then, you need to implement in Logipedia an output to HOL-Light or HOL.

2) I believe that @EmilieGrienenberger developed a translator from HOL-Light to Dedukti/STTfa as well, and perhaps from Dedukti/STTfa to HOL-Light.

fblanqui commented 3 years ago

Le 06/10/2020 à 14:02, brando90 a écrit :

In theory, yes. We currently have a translator from Coq to Dk/Coq,
the instance of Dedukti with the encoding of Coq logic. See
https://github.com/Deducteam/CoqInE . We also have tools to
translate proofs from Dk/Coq to Dk/STTfa. See
https://github.com/Deducteam/universo. Finally, we have a
translator from Dk/STTfa to OpenTheory. See
https://github.com/Deducteam/Logipedia. I believe that
Isabelle/HOL can read OpenTheory files but I am not sure of the
current status of this. Anyway, it would be better to extend
Logipedia to directly output Isabelle/HOL from Dk/STTfa (this is
already done for PVS; so it should not be very difficult). So,
most of the tools are already available to translate Coq files to
Isabelle/HOL files. What is missing is to glue them together and
automate this tool chain. If you are interested in contributing to
this, you are very welcome!
Yes I am interested! Let my try to write it as a list so I know how to execute this:

translate Coq to Dk

translate Dk to STTfa

translate STTfa to OpenTheory

check if Isabelle can open OpenTheory files.

is this how this is done? I want to try it if this is what has to be done. How long do you estimate it takes to do in time (to get a feel while I am doing it if I am on the right path or stuck)?

Dk/Coq is the instance of Dk with the logic of Coq, Dk/STTfa is the instance of Dk with the logic STTfa (simple type theory with prenex polymorphism), like Isabelle/HOL is the instance of Isabelle with HOL (higher-order logic), Isabelle/ZF is the instance of Isabelle with ZF set theory.

So, to be precise, we have:

use coqine to translate Coq vo files to Dk/Coq files
use universo and perhaps other tools to translate Dk/Coq files to Dk/STTfa files
develop an extension of logipedia to translate Dk/STTfa files to Isabelle/HOL files or use logipedia to translate Dk/STTfa to OpenTheory if Isabelle/HOL can import OpenTheory files

Concerning 3, if you are familiar with Isabelle/HOL, it should not be too long, a few days or weeks. In https://github.com/Deducteam/Logipedia/tree/master/src/sttfa/export you will find the code for exporting STTfa proofs to Coq, HOL-Light, Lean, Matita, PVS, and OpenTheory. This will give you an idea. There is one file for each system, and each file has between 150 and 415 lines of OCaml.

francoisthire commented 3 years ago

@brando90 : As Frédéric said, in theory I explained in my PhD thesis how this could be achieved. If you are interested I can send you a draft (almost final version) of my manuscript.

In practice, we are quite far from it because we lack of manpower. However, a project has been submitted to get funds for financing such translation.

The current shortcomings are:

My code ran on Dedukti 2.7. However, the team which maintain Dedukti decided for the version 3 of Dedukti to use completely fresh implementation of Dedukti (see the project lambdapi). This makes the tools mentioned by Frédéric obsolete for the version 3 of Dedukti. The version Dedukti 2.7 is still usable but is not maintained currently. Translating my tools to Dedukti 3 requires a lot of manpower (probably several man-months) and I am not aware of any progress regarding this (maybe if we get funds, things will be a lot better though).
The Universo tool mentioned by Frédéric is not enough to go from the encoding of Coq in Dedukti to Sttfa. For two reasons:
1. First the translation is partial and might not even work for your use case. For example if the proofs in Coq relies on (full) polymorphism which is not possible in the theory of Isabelle/HOL since only prenex polymorphism is allowed.
2. If proofs in Coq uses dependent types, we cannot translate them to Isabelle/HOL for the same reason
3. Part of the translation has not been automatized yet. Mainly the part which replaces computable functions by axioms. This is may be not needed for Isabelle/HOL but it is needed to go to STTfa
4. As Frédéric said, a lot of glueing is needed. I am working on this on my free time but honestly I won't finish soon
5. The output is type checkable but not directly usable because we do not provide any concept alignment: no implicit parameters, no notations, etc... Such thing can be rebuilt easily in Isabelle but it needs to be done manually for the moment.

I have several ideas to overcome all of these issues, but as I said, we are lacking of manpower and if people wish to contributing, it is very welcome.

Because people maintaining Dedukti aim to use the version 3, the first thing would be to translate the interoperability I wrote during my PhD from Dedukti 2.7 to Dedukti 3. However, I have to admit that I am not 100% convinced that it is the only way to go. While Dedukti 3 is designed to be used as a proof assistant, Dedukti 2.7 was designed to be used for interoperability, and I am not sure that both views are compatible. However, it is not my responsibility to decide this, and I am just giving my opinion here. But on the midterm, things would be a lot easier if some people could maintain Dedukti 2.7.

brando90 commented 3 years ago

thanks everyone for the feedback!

My current plan was to have a translator of most of the HOL languages to open theory (http://www.gilith.com/opentheory/). Then translate the OT to Isabelle. Isabelle is my main target.

It seems that the direction from Coq to Isabelle is unfeasible for now. If that changes let me know!

Is Open Theory to Coq just as unfeasible (and visa versa)? Sorry, I'm not a super expert in TP but have a strong interest.

(btw found this related SO Q: https://stackoverflow.com/questions/51586820/automatic-translation-from-isabelle-hol-to-hol)

brando90 commented 4 months ago

@francoisthire sorry for the spam, but is it also possible to translate Coq, Isabelle -> Lean? I'd like to generate more high quality (correct!) code for Lean4.

fblanqui commented 4 months ago

Hi. Currently no. But there are various ongoing works to do this. From Coq, you can go to Dedukti using https://github.com/Deducteam/coqine/, and from Isabelle, you can go to Dedukti and Lambdapi using https://github.com/Deducteam/isabelle_dedukti. In the first case, you get Dedukti proofs in the logics of Coq. In the second case, you get Dedukti proofs in the logic of Isabelle, that is, higher-order logic, though there is a number of things that are internally added by Isabelle which are not completely understood yet (type classes) that need to be properly represented in Dedukti. Now, from the encoding of higher-order logic in Dedukti, you can go to several other formats (PVS, Lean2or3, Matita, Coq, OpenTheory) using https://github.com/Deducteam/sttfaxport. From Dedukti and Lambdapi files using an encoding of higher-order logic, you can also go to Coq using https://github.com/Deducteam/lambdapi. It shouldn't be too difficult to extend lambdapi to add an export to Lean4. If you start from Coq, you possibly need to transform the Dedukti proofs you get with coqine to higher-order logic by using https://github.com/Deducteam/universo. François Thiré did this for the Matita arithmetic library: he translated it to Dedukti using https://github.com/Deducteam/krajono, transform it to arrive in higher-order logic, and used sttfaxport to translate it to PVS, Coq, Lean2or3 and OpenTheory. You can see the result on http://logipedia.inria.fr/. If you want to contribute to one or several of these steps, you are very welcome!

Deducteam / Dedukti

Is it possible to translate Coq to Isabelle (and Lean) using Dedukti? #224