coq to lean translator

Stream: new members

[Abhishek Anand]

Has there been any effort to write a Coq to Lean translator? Has anybody thought of the issues in such a project
The only discussion I could find is this one which I could not follow. I guess defeq means definitional equality in that post? I do see that the mismatch of definitional equality poses some complexity but to me those are far from unsurmountable.
I am not super familiar with Lean 4, but it seems more like an extensional dependent type theory, similar to Nuprl.
I do know Coq and Nuprl quite well and I would say it is very much possible to write a very useful translator from Coq to Nuprl, although it may take months to perfect.

[Michael Rothgang]

yes, defeq = definitional equality

[Michael Rothgang]

(And thanks for digging up the link: I found it useful. I cannot add anything to this.)

[Kevin Buzzard]

I'm not an expert in this area but having watched several of these conversations go by in the past, one observation is that there might not be much point making such a translator, because it will not translate idiomatic Coq into idiomatic Lean so it's not clear how to use the output of such a translator effectively.

[Abhishek Anand]

it will not translate idiomatic Coq into idiomatic Lean

yes, naive ways to do this translation will suffer from this problem. but again, I don't really see why this problem is unsurmountable. the translator can be tailored to take into account such idioms

[Patrick Massot]

We now have a much better answer to this question. Doing an approximate Lean 3 to Lean 4 translator was already extremely challenging and not producing fully working code. Anything else will be much harder.

[Patrick Massot]

So this problem is simply much harder than what optimistic people think.

[Abhishek Anand]

do you have any specifics on the challenging issues? Getting idiomatic code may be harder largely because the idioms are not very formally/precisely defined, but I am skeptical of the difficulty of getting working code: people have built (verified) compilers between very different languages

[Patrick Massot]

I am pretty sure the examples you have any mind do not involve anything like an elaborator.

[Abhishek Anand]

yes, but the translation input doesn't need to be the unelaborated src file. For example, in certicoq (Coq->C), we got access to the fully elaborated AST

[Mario Carneiro]

Abhishek Anand said:

I am not super familiar with Lean 4, but it seems more like an extensional dependent type theory, similar to Nuprl.

No, it is not an extensional type theory. If it was things would probably be a lot simpler, but it is similar to Coq in this respect. If you have an equality which is not a defeq then there is no way to upgrade it to one, so if this is an equality of types then you need to insert cast functions to coerce elements of those types across the equality, and then you need coherence lemmas for the casts and everything sort of piles up. It's possible that in practice the complexity stays bounded but the worst case is very bad.

[Mario Carneiro]

To be honest, my experience with the lean 3 -> lean 4 translation actually made me more positive on the possibility of Coq to Lean translation, at the syntax level. Translating already-elaborated terms will result in a mess even if you somehow manage to solve all the theory issues I mentioned in that earlier post, but syntax translation and manual cleanup can get you a long way and result in something reasonably idiomatic at the end as well. This is especially important given that both Coq and Lean have a tendency toward tactic style proofs, while the kernel terms are completely different. Throwing away the tactic structure and translating at the term level will result in something which can only be used as a black box, and it would be a lot closer to "compilation" than "translation".

[Mario Carneiro]

Of course, you can still do syntax -> syntax translation using the elaborated information as an interpretation hint. Lean 4 is good at providing that kind of information, but Coq -> Lean translation would require it from Coq and I'm not sure how feasible that is (it might be okay, I don't have enough information on the matter).

[Abhishek Anand]

for projects like iris-lean, which is what motivated me to think about this translation, it may be fine for me if the translator produces only kernel terms (no tactic scripts) for proofs. (it would help for the definitions to be lean-idiomatic though)
ultimately, the ground truth of iris will live in Coq, at least for now, so there is not much point IMO in editing those proofs in lean.
I have been using iris in Coq for several years and built hundreds of proofs on top of it, but never ever needed to look at a proof script inside iris anyway.

[Abhishek Anand]

Mario Carneiro said:

No, it is not an extensional type theory. If it was things would probably be a lot simpler, but it is similar to Coq in this respect. If you have an equality which is not a defeq then there is no way to upgrade it to one, so if this is an equality of types then you need to insert cast functions to coerce elements of those types across the equality, and then you need coherence lemmas for the casts and everything sort of piles up. It's possible that in practice the complexity stays bounded but the worst case is very bad.

Do you have example of two definitionally equal terms in Coq whose "idiomatic" translations to Lean will not be definitionally equal? I thought Lean had strictly more definitional equalities.

[Mario Carneiro]

Anything making use of universe cumulativity won't be expressible in Lean without a ULift

[Mario Carneiro]

it's a bit difficult to get an example which is as "crisp" as your request; mostly there are just a bunch of features where the translation is a bit of a ??? but where there is a mostly okay translation choice you can make, and then when you combine enough of those mostly okay translations you get something that is not okay

[Mario Carneiro]

The most obvious ??? is Coq's fixed universes and the whole partial order of constraints on these universes. Lean has no analogue of this, but Coq makes use of them extremely frequently and it is quite difficult syntactically not to introduce them