# Zulip Chat Archive

## 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 implicit`C`

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

According to your two cases.

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