## Stream: new members

### Topic: proving the eliminator for equality

#### 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.

#### 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.

#### Patrick Thomas (Apr 10 2021 at 21:53):

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

#### Mario Carneiro (Apr 10 2021 at 21:57):

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

#### 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

#### Patrick Thomas (Apr 10 2021 at 22:00):

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

#### 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

#### 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)


#### 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?

#### 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.

#### 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;

#### Patrick Thomas (Apr 10 2021 at 22:44):

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

#### Patrick Thomas (Apr 10 2021 at 22:45):

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

#### 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

#### 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

#### 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.

#### Daniel Fabian (Apr 10 2021 at 22:54):

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

#### Daniel Fabian (Apr 10 2021 at 22:54):

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

#### 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.

#### Patrick Thomas (Apr 10 2021 at 23:03):

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

#### Mario Carneiro (Apr 10 2021 at 23:06):

(\lam _: nat, nat)

#### 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

#### 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.

#### 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.

#### Daniel Fabian (Apr 10 2021 at 23:28):

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

#### Daniel Fabian (Apr 10 2021 at 23:28):

That's why it is related to pattern matching.

#### 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.

#### 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.

#### Patrick Thomas (Apr 10 2021 at 23:43):

Yes, I think that helps. Thank you.

Last updated: May 12 2021 at 05:19 UTC