Zulip Chat Archive

Stream: new members

Topic: proving the eliminator for equality


view this post on Zulip Patrick Thomas (Apr 10 2021 at 19:09):

Would someone be able to point me to a good text explaining how this is done? I've seen the proof in Coq using pattern matching, but I haven't been able to follow it.

view this post on Zulip Kevin Buzzard (Apr 10 2021 at 21:13):

Do you mean eq.rec? This isn't proved in Lean, this is generated as an axiom when eq is defined as an inductive type.

view this post on Zulip Patrick Thomas (Apr 10 2021 at 21:53):

As an axiom? I thought it was a proof that was automatically generated?

view this post on Zulip Mario Carneiro (Apr 10 2021 at 21:57):

In Coq, pattern matching on inductive types is primitive. In Lean, T.rec is primitive

view this post on Zulip Mario Carneiro (Apr 10 2021 at 21:59):

There are reasons to prefer the latter, because it turns out that equation compilation (transforming a match statement into recursor applications) is complicated, and there have been soundness bugs in Coq before due to the termination checker

view this post on Zulip Patrick Thomas (Apr 10 2021 at 22:00):

Oh. So does pattern matching follow from T.rec somehow?

view this post on Zulip Mario Carneiro (Apr 10 2021 at 22:01):

Yes, if you pattern match on rfl that gets translated into an appropriate application of eq.rec

view this post on Zulip Mario Carneiro (Apr 10 2021 at 22:03):

def foo :   
| 0 := 0
| (n+1) := foo n + 2

-- is equivalent to

def foo' :    :=
λ n, nat.rec_on n 0 (λ n ih, ih + 2)

view this post on Zulip Patrick Thomas (Apr 10 2021 at 22:06):

I see. Would you happen to know of a good explanation for how it works for equality in Coq?

view this post on Zulip Patrick Thomas (Apr 10 2021 at 22:10):

I'm currently working on learning Coq, since I was able to audit a course on it, and it seems very close to Lean, so hoping the knowledge should be transferable.

view this post on Zulip Yury G. Kudryashov (Apr 10 2021 at 22:22):

While some basics are very similar, there are quite a few important differences. Here are some of them (not sure that I'm listing the most important ones):

  • lean can have tactic inside expr inside tactic;
  • lean and coq treat universes differently (cumulative universes in coq, non-cumulative in lean; more universe polymorphism in the lean stdlib);
  • very different libraries and tactics; e.g., lean mathlib is much more classical than mathcomp;

view this post on Zulip Patrick Thomas (Apr 10 2021 at 22:44):

Actually, I'm not certain I follow how the equivalence between foo and foo' works.

view this post on Zulip Patrick Thomas (Apr 10 2021 at 22:45):

nat.rec is the eliminator? What is nat.rec_on?

view this post on Zulip Mario Carneiro (Apr 10 2021 at 22:48):

nat.rec_on is the same as nat.rec but the nat argument comes first instead of last

view this post on Zulip Mario Carneiro (Apr 10 2021 at 22:51):

Here's an implementation of eq.rec using pattern matching:

def {u l} eq.rec' {α : Sort u} {a : α} {C : α  Sort l} (h : C a) {b : α} (e : a = b) : C b :=
match b, e with
| .(a), rfl := h
end

The proof in Coq would be similar to this, although in lean it's circular because the equation compiler will compile the match into a proof using eq.rec

view this post on Zulip Daniel Fabian (Apr 10 2021 at 22:53):

when you write the def foo ... it translates to a call on the nat.rec recursor. In this particular example it is simple. But if you make the pattern any more complicated, it doesn't translate nearly as straight-forwardly anymore. E.g. if you define fib, the translation is a good deal more complicated.

view this post on Zulip Daniel Fabian (Apr 10 2021 at 22:54):

just define it and look at the generated code using #print fib

view this post on Zulip Daniel Fabian (Apr 10 2021 at 22:54):

the point is, that nat.rec always eliminates the nat.zero and nat.succ constructors.

view this post on Zulip Daniel Fabian (Apr 10 2021 at 22:55):

whereas pattern matching can do all kinds of things, even structural recursion like in the case of fib.

view this post on Zulip Patrick Thomas (Apr 10 2021 at 23:03):

In foo', what is the implicitC set to in the call to nat.rec_on?

view this post on Zulip Mario Carneiro (Apr 10 2021 at 23:06):

(\lam _: nat, nat)

view this post on Zulip Mario Carneiro (Apr 10 2021 at 23:07):

This is a nondependent function, so the type doesn't depend on the input value. In eq.rec' the motive is dependent, because we are producing a value of C b but we provide h : C a

view this post on Zulip Patrick Thomas (Apr 10 2021 at 23:20):

So foo' expands toλ n, nat.rec 0 (λ n ih, ih + 2) n
I'm not sure how to expand nat.rec though if it is an axiom without a function. Trying to follow an example of how applying a number to foo' results in the same value as applying it to foo.

view this post on Zulip Daniel Fabian (Apr 10 2021 at 23:27):

you can build an intuition of roughly like this: C is the motive what you are trying to prove. And nat.rec is an induction principle. nat -> nat can be read like "for all x of nat, provide a proof, i.e. a witness, of nat".

And you use the induction principle by saying how to construct the witness for 0, by using 0. And to provide the witness for n+1, you choose foo n + 2. Where foo n is your ih.

view this post on Zulip Daniel Fabian (Apr 10 2021 at 23:28):

and nat.rec gives you the function that "for all x of nat, build the witness".

view this post on Zulip Daniel Fabian (Apr 10 2021 at 23:28):

According to your two cases.

view this post on Zulip Daniel Fabian (Apr 10 2021 at 23:28):

That's why it is related to pattern matching.

view this post on Zulip Daniel Fabian (Apr 10 2021 at 23:29):

But it's a version of pattern matching, where you are only allowed the constructors of your inductive type.

view this post on Zulip Mario Carneiro (Apr 10 2021 at 23:30):

Perhaps it helps to see the "computational rules" for nat.rec to understand how it works:

nat.rec z s 0 = z
nat.rec z s (n+1) = s n (nat.rec z s n)

These are definitional equalities. We say that nat.rec z s n is "defined by recursion" with z being the value at 0 and s saying how the value at n+1 depends on the value at n.

view this post on Zulip Patrick Thomas (Apr 10 2021 at 23:43):

Yes, I think that helps. Thank you.


Last updated: May 12 2021 at 05:19 UTC