Coq as a lean type checker

Stream: general

[Bas Spitters]

Gaetan Gilbert made a Coq type checker for lean in order the help understand the differences. I think it's very useful in that way.
https://coq.discourse.group/t/alpha-announcement-coq-is-a-lean-typechecker/581

[Johan Commelin]

That seems like a really thorough comparison. Chapeau!

[Rob Lewis]

This is cool! I'm not really clear what's meant by this line:

The whole stdlib cannot be checked as some conversion problems are
pathological. two_pos seems a typical example (0 < 2 in an ordered
field).

I'm probably missing something, does anyone know what the issue is with 0 < 2?

[Johan Commelin]

I just saw that @Gaëtan Gilbert also has an account here. So we can ask him directly :wink:

[Floris van Doorn]

Yes, this looks really cool indeed. Also interesting to see some small kernel differences between Coq and Lean I have never seen before.

[Gaëtan Gilbert]

It means that some conversion problem involved in checked the proof of 0<2 is difficult for Coq. I haven't investigated yet, I guess it starts unfolding the wrong thing then gets lost.

[Floris van Doorn]

I also don't know what the problem is with two_pos.
For the lazy:

lemma two_pos : (2:α) > 0 :=
begin unfold bit0, exact add_pos zero_lt_one zero_lt_one end

and #print two_pos gives

theorem two_pos : ∀ {α : Type u} [_inst_1 : linear_ordered_field α], 2 > 0 :=
λ {α : Type u} [_inst_1 : linear_ordered_field α],
  eq.mpr
    (id
       ((λ [_inst_1 : has_lt α] (a a_1 : α) (e_2 : a = a_1) (b b_1 : α) (e_3 : b = b_1),
           congr (congr_arg gt e_2) e_3)
          2
          (1 + 1)
          (bit0.equations._eqn_1 1)
          0
          0
          (eq.refl 0)))
    (add_pos zero_lt_one zero_lt_one)

Maybe it's the weird identity function generated by unfold that causes problems.

[Rob Lewis]

Hmm, maybe. I would have guessed that the proof of two_pos doesn't have that much that's even possible to unfold. But Lean isn't happy with #reduce two_pos either.

[Rob Lewis]

@Kevin Buzzard remember when you used to complain about proving things about numerals? Turns out the proofs are actually hard :p

[Floris van Doorn]

For me, #reduce @two_pos takes a couple of seconds. There is still a bunch to unfold, with all the substitutions involved in the following definitions (used in two_pos):

#print add_pos
#print add_lt_add_right

Maybe Coq is busy unfolding all these, which doesn't seem to be necessary.

[Kevin Buzzard]

yeah my ideas about what maths is "hard" have changed rather radically in the last 2.5 years...

[Gaëtan Gilbert]

OK I figured out why two_pos is slow
In Coq we try reducing terms before testing if they're proof irrelevant
If I change that order two_pos checks basically instantly

The reason we picked that order is basically that all our benches use only relevant terms (since sprop is still new), and for those it's faster to reduce first

[Kevin Buzzard]

What is Coq's sprop?

[Floris van Doorn]

It's Lean's Prop: a universe that is definitionally proof irrelevant.

[Floris van Doorn]

Coq's Prop is not definitionally proof irrelevant, but you can add proof irrelevance as an axiom.

[Kevin Buzzard]

I see. So the issue is rfl working or not?

[Kevin Buzzard]

Hey this is a really cool way to check sprop :-)

[Kevin Buzzard]

There will be issues with quotients as well, presumably? I never quite understood the Lean reference manual here: it seems to give a definition of rfl which doesn't seem (to me) to imply that quot.lift f h (quot.mk r a) = f a is defeq.

[Floris van Doorn]

Yes, quotients are also an issue, but there is a trick in Coq using so-called Private Inductive types. This has also been used to implement higher inductive types in the Coq-HoTT library (a quotient is an example of a higher inductive type).

[Floris van Doorn]

It's quite a hack, the idea is the following. You privately define the quotient A / ~ to be just A (or a inductive type that is isomorphic to A): then it's very easy to define functions quot.lift and quot.mk such that the rule quot.lift f h (quot.mk r a) = f a holds definitionally. Of course, you don't get the rule that if x ~ x' then [x] = [x'], but you can add that as as an (inconsistent) axiom. Then you declare everything that you don't want to use as "private" (for example the fact that A / ~ was implemented as A), so that you cannot use these things anymore.
The final result is that from outside the private module, everything you can see is exactly the behavior of a quotient.

[Floris van Doorn]

Here is another explanation: https://dl.acm.org/doi/pdf/10.1145/3018610.3018615?download=true
(Section "Higher Inductive Types")

[Kevin Buzzard]

You CS guys are so imaginative ;-)

[Kevin Buzzard]

I'll try explaining quotients using this technique to my undergraduates when I teach them next year.

[Kevin Buzzard]

if it's good enough for the computer, it's good enough for them.

[Mario Carneiro]

So basically it's controlled inconsistency? :/

[Mario Carneiro]

@Gaëtan Gilbert Have you looked at all at the reverse process, Coq -> Lean? I've been bugging all coq people I know to tell me how the kernel typechecking algorithm works, because it's not completely documented anywhere outside the ML

[Mario Carneiro]

Is there an analogue of the Lean output format for Coq?

[Gaëtan Gilbert]

Coq -> Lean is way harder due to universe cumulativity (I wouldn't be surprised if it's impossible)
Other universe issues:

• non recursively uniform parameters (AFAICT translating them to regular indices only changes the universe of the inductive)
• template universe polymorphism (a predecessor of universe polymorphism, kinda underspecified, it has caused repeated inconsistencies but hasn't been removed because it's still in use everywhere through sigma types and list and so on)

If you get past universe issues you also have

• your pattern matching to eliminator elaboration must be as strong as the termination condition implemented in Coq (not sure how hard this is, I'm not an expert on the termination checker)
• mutual and nested inductives (I think Lean already has some system to deal with those?)
• modules. You could just reduce functor applications and treat the resulting flat modules as namespaces (AFAIK the checker does something like that). If module aliases or Include are used you will not have a fun time.

Less used:

• records with definitional eta (not used in Coq's stdlib)
• coinductives (not used much afaik)
• primitive integers and floats (also not used much afaik)

No output format, parsing vo files while ignoring non-kernel stuff may be feasible if you tie yourself to a specific Coq version.

[Gaëtan Gilbert]

PS maybe using serapi or a custom plugin one could get a reasonable output format

[Kevin Buzzard]

it has caused repeated inconsistencies but hasn't been removed because it's still in use everywhere through sigma types and list and so on

So to implement this part you have to find an inconsistency in Lean?

[Gaëtan Gilbert]

There are no known inconsistencies left in it, it's just a historically buggy part of Coq

[Kevin Buzzard]

On the other hand I have seen people getting into universe messes here -- they are often sorted out in the end but I have often wondered whether cumulative universes would make life easier. I'm a believer in ZFC so I would be happy if everything sensible just lived in Type (other than the things which are "obviously not sets")

[Mario Carneiro]

I just got to the part of Coq Coq Correct! that deals with the most subtle part of the theory, the guard condition on recursion inside a fixpoint, but they axiomatized it, so there is no definition :(

[Johan Commelin]

This hit HN front page: https://news.ycombinator.com/item?id=22171305

[Johan Commelin]

@Kevin Buzzard You're getting some indirect credit. See the first comment.

[Gaëtan Gilbert]

Updated stdlib stats after fixing the issue examplified by two_pos (we need to check for proof irrelevance before comparing structurally):

Lean Import with 10s timeout, set upfront instances and set conv check:
320s, 1GB RAM
vo size 111MB
11 skips (3 timeout, 8 not instantiated)

The timeouts are bla.equations._eqn_1, where bla in

• tactic.delta_config.max_steps._default
• char.of_nat
• simp.default_max_steps
  These all involve moderately sized integers (of_nat through char.is_valid)

I actually already did a hack for std.prec.max.equations._eqn_1, setting prec.max to the Expand reduction strategy (when comparing 2 applied constants we need to decide which one we try to reduce first, Expand is the most eager strategy). That may be correct for the max_steps but doesn't seem right for of_nat.
What does Lean do here?

[Mario Carneiro]

Lean unfolds the definition with the largest definitional height, which I believe is the max of the definitional heights of all referenced definitions, plus one

[Mario Carneiro]

Looking at char.of_nat, I see no expensive unfolding at all

[Gaëtan Gilbert]

Thanks, that looks like it works. The Lean stdlib now fully passes:

• 284s runtime, 1.3GB RAM usage
• resulting vo takes 116MB
• coqchk takes 540s and 1.1GB RAM
  If we skip structure validation coqchk takes 51s and 720MB RAM
  If we use OCaml's Marshal instead of our custom Analyze coqchk takes 45s and 380MB RAM

[Bas Spitters]

So basically it's controlled inconsistency? :/

The technique was explained here in agda:
https://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/
It's a hack to add HITs to a type theory that does not have them. Really, we'd like to have a cubical type theory in the future.

[Tim Carstens]

:heart:️ to that!