Beginner's Question

Stream: new members

[Jay Sulzberger]

There are several proof assistants.
Who is working on the functor, well, the one from, the objects of, say, Coq, to the objects of LEAN?
This functor, should take an sentence and/or a proof of Coq, and give back a sentence and/or a proof of LEAN.

[Yury G. Kudryashov]

I don't remember what's the status (I guess, @Mario Carneiro should know) but I remember that there is a lot of issues like different approach to universes, different default sets of axioms. And there is no hope (at least, in the nearest future) that we'll have a way to port proofs, e.g., from mathlib to mathcomp, because of different design choices: it is too hard to align definitions from two libraries.

[Mario Carneiro]

There is a post Coq is a Lean typechecker that is used as an example of this sort of thing, but if you actually read the post you will see that they had to extend the Coq kernel to do it, and still many things are not checked (i.e. the Coq kernel is permitting lean proofs that would be unsound). In practice aligning distinct DTT systems is almost impossible. Even Lean 3 -> Lean 4 is very nontrivial and I'm sure we will have to patch lots of proofs to get around the broken defeqs for functions that are ever-so-slightly different

[Mario Carneiro]

Translating between systems where at least one side is not DTT is a lot easier because you don't have to worry about preserving defeq

[Jay Sulzberger]

Thanks very much, Yury G. Kudryashov! Heaven forwarding, I will ask M. Carneiro before the Equinox.

[Jay Sulzberger]

Ah, Mario Carneiro, I will read your post before I sleep.
Thanks! and good night!

[Mario Carneiro]

The mismatch in universe handling and axioms are actually comparatively simple to solve (the axioms are true when translated to lean, after all). The major issues are all the missing defeqs: Coq doesn't have quotient types, Lean doesn't have inductives with non-uniform parametric arguments, coinductive types, and universe cumulativity (which can be used to prove defeqs that would not be true for a ulift encoding). Defeq is a problem because you can't just work around it if it's false, you get what you get and there isn't any slot to insert your proof that in fact it's okay because such and such. And since defeq in type theory is not at all "canonical", every DTT-based system has slight variations here and you get an isolating effect.

Even if your defeqs line up, if your unfolding heuristics don't line up you can end up timing out on simple examples because the worst case scenario for defeq checking is "unfold to a normal form" which has an incredibly high asymptotic complexity (I don't have words to express it, it's somewhere in the fast growing function hierarchy past all the countable ordinals that have regular names). In practice that means that these things break down early, and that's exactly what happens in the Coq->Lean translator - it will translate core.lean but fails to translate the lean 3 core lib unless you use Unset Conversion Checking which is basically cheating and is unsound. (This was later fixed in the translator... by copying the unfolding heuristics.)

[Jay Sulzberger]

Mario, thank you! For both the translator and your answer!

Starting around 2012, I took part in a seminar on New Crazy Type Theory^W^W^W^WType Theory After Lambda. Noson Yanofsky is the patron of the seminar which meets at CUNY in New York City. We started with the HoTT book. It took me a few years to grasp that

    Curry-Howard, when applied to the most minimal Simply Typed Lambda Calculus,
    gives a convincing formalization of what it means to say
             "Proof Pr0 is really the same proof as Pr1."
     for the Intuitionist Positive Implication-Only Propositional Calculus.

The explication/formalization proceeds from, really just is, these two facts

      A correctly typed lambda term gives a proof (of its type, when the type is read as a sentence) in the
      Intuitionist Positive Implication-Only Propositional Calculus.

       Lambda Conversion is sound and complete for when two lambda terms compute the same  
       function, which function is parametrized over ground types.

Kevin Buzzard has a delightful rant, recorded in a published video, arguing for using LEAN to help teach Math 101. The above first case of Curry-Howard struck me hard. I think it will be part of a not yet delivered talk on New Crazy Type Theory. Yesterday I looked at

       https://mathoverflow.net/questions/3776/when-are-two-proofs-of-the-same-theorem-really-different-proofs/3783

and I remember Tim Gowers's post on the question. Your answer shows me that you have done work which helps toward understanding when two proofs are the same for systems beyond the Intuitionist Positive Implication-Only Propositional Calculus. Again, thank you!

[Kevin Buzzard]

In Lean, any two proofs of the same theorem are equal. This is a wonderful situation because it means that you don't get distracted by this metamathematical question of when two proofs are equal and can just get on with doing number theory or whatever mathematics you want to do. Equality of proofs might look interesting but it ties you in knots, distracts you and slows your progress.

[Kevin Buzzard]

I think this is one of the reasons why some of the serious type theory people look down on lean and conversely I think it's one of the reasons lean works so well for mathematics

[Arthur Paulino]

From a practical standpoint I can't see any use for proofs of the same theorem that have different consequences in a program (except that some proofs type check faster than others)

[Jay Sulzberger]

Kevin and Arthur, Please forgive me for not responding here with serious careful rebuttals to your claims. I hope to, some months, perhaps, years, form now, respond properly to your, admittedly subtle and complex,
claims. I wrote some stuff some years ago which may be useful to you as an outline of my dreamed-of, but so far, unwritten Counter-Blast:

https://cs.nyu.edu/pipermail/fom/2014-October/018302.html

and the dozen or so posts, some by me, with subject

 New Umbrella

on the page

 https://cs.nyu.edu/pipermail/fom/2014-October/

Again, please forgive me for such an improper response as this!

But I do not restrain myself from one tiny apposite squib:

The LEAN Project is founded on the Metamathematical Investigations of the last half of the Nineteenth Century, and the further work down to today. And it would be good to have a few functors, well checked, between the objects, of Coq, HOL, ..., and LEAN. Once we have such mechanized realizations of these as yet only partially known functors, there will be "practical"uses of such aids to thought.

Thanks, Kevin, thanks, Arthur!