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

[brando90]

Is it possible to translate Coq to Isabelle using Dedukti?

[fblanqui]

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]

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:

1. translate Coq to Dk
2. translate Dk to STTfa
3. translate STTfa to OpenTheory
4. 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]

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]

@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]

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]

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]

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]

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]

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: 1. translate Coq to Dk 2. translate Dk to STTfa 3. translate STTfa to OpenTheory 4. 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: 1. use coqine to translate Coq vo files to Dk/Coq files 2. use universo and perhaps other tools to translate Dk/Coq files to Dk/STTfa files 3. 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]

@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]

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]

@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.

related: https://coq.discourse.group/t/alpha-announcement-coq-is-a-lean-typechecker/581/8