Can one translate from one ITP language to another automatically?

Is it possible to translate from one language to another (e.g. from Coq to Isabelle or Coq to Lean or Coq to HOL Light etc.) using an intermediate language (e.g. TPTP or whatever Hammers use)?

What I had in mind was that since most ITPs have some sort of ability to talk to ATPs/Hammers it should be possible to translate between languages automatically (e.g. TPTP or whatever Hammers use).

Motivation(s): This could increase the number of facts users, ATPs, etc have in their disposal for further proving more things etc. Also, removing the dependence on any specific ITP seems valuable as they are hard to learn, so one can just learn 1 and then get the benefits of all of them.

Rebuilding a proof term from an ATP/Hammer is a much harder problem then you would expect. If I understand correctly, the reason for that is that automated techniques (e.g. SAT solvers) tends to do all sorts of simplifications that are hard to translate back to an actual proof term.

Take a look on Dedukti, they are working on such an intermediate representation between ITPs.

1 Like

We all dream of this! There have been several PhD theses started on this topic, I remember at least the work of Ewen Denney and Chantal Keller (and sorry for the others that I forget). Pedro Also cites the Dedukti project.

One of the problems is that you want not only the basic logic to correspond, but also the higher level concepts (the defined ones) to fit together. but this is not so simple. I was looking at a Lean tutorial yesterday, and it turns out that it defines natural number addition in an equivalent but not interchangeable way. In Coq “0 + x” and “x” are convertible (so some proofs
won’t have a trace of this reasoning step) but “x + 0” and “x” are only provably equal (so any use of this fact needs to be explicit in proofs). In the Lean I was studying , it is the other way round. (“x + 0” “x” convertible, “x” “0 + x” provably equal). So this is a difficulty: you would like the proofs you obtain from one system to use the concepts of the other system in a way that feels natural to the reader, but the theorems are often formulated in a way that is specific to the “idioms” of the library you are looking at.

2 Likes

Thanks! Will take a look.

Perhaps if I lower the bar something can be done.

What about a translation of only these 4 (or a subset of them):

  • Mizar
  • Coq
  • Isabelle
  • Lean

might that exist?

Interesting, I need to take a look at that later…

I am curious. Why is the intermediate language of an ATP difficult to parse to a term of a different language if it seems that all major ITPs (Coq, Mizar, Isabelle, idk if lean but likely?) all have hammers. Couldn’t we just re-use their code to translate one proof script in one language to the other using this intermediate representation (given hammers exist already)?

Assuming such a translation even exists. Keep in mind that different theories have different expressive powers, and their axioms may not even be consistent with each other. Even two Coq libraries may be inconsistent if put together because of the same reason.

Again, I mentioned this in my other answer, but automatic solvers make huge simplifications that are very hard (if possible at all) to parse back to an actual proof script.

Since Isabelle is designed to rely a lot on hammer, I suggest that you make this same question at the Isabelle mailing list, they will probably give you a more descriptive answer around this problem. And if you do please post a link here, I’d like to follow such a discussion.

1 Like