proving the eliminator for equality

Stream: new members

[Patrick Thomas]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Patrick Thomas]

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]

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]

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

[Patrick Thomas]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Daniel Fabian]

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

[Daniel Fabian]

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

[Patrick Thomas]

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

[Mario Carneiro]

(\lam _: nat, nat)

[Mario Carneiro]

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]

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]

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]

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

[Daniel Fabian]

According to your two cases.

[Daniel Fabian]

That's why it is related to pattern matching.

[Daniel Fabian]

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

[Mario Carneiro]

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]

Yes, I think that helps. Thank you.