## Stream: new members

### Topic: Pattern matching and proving with rfl

#### Brandon Brown (May 10 2021 at 04:01):

[Lean4]

inductive nat : Type where
| zero : nat
| succ : nat → nat

open nat

protected def nat.add : nat → nat → nat :=
fun a b =>
match a, b with
| a, zero => a
| zero, b => b -- removing this case makes the theorem below work
| a, succ b => succ (nat.add a b)

theorem add_zero (a : nat) : a + nat.zero = a := rfl -- type mismatch


I understand the second case in my nat.add is unnecessary, but why does it result in the theorem not being provable by rfl anymore? a + zero = a is still true by definition in the add function.

#### Brandon Brown (May 10 2021 at 04:29):

Also is there any reason why the pattern matching in the induction doesn't accept parentheses around (succ a)

theorem zero_add (a : nat) : zero + a = a := by
induction a with
| zero => rfl
| (succ a) c =>  -- error with "(succ a) c" but not with "succ a c"


#### Kevin Buzzard (May 10 2021 at 06:58):

My guess for the first question (which I could check if I was sitting in front of lean) is that like lean 3 when you do random matches like you're doing, the equation compiler has to make some sense of what's going on and so will probably just end up splitting into the obvious four cases internally, meaning that aou'll have to do cases on a before refl will work

#### Kevin Buzzard (May 10 2021 at 07:01):

Think about it this way: you defined zero+succ(b) twice and so you can't expect to predict which choice is the one which is true by definition, which then means that you can't expect to predict what is going on by definition more generally

#### Kevin Buzzard (May 10 2021 at 07:35):

I've just tried to verify my claim with Lean 4 and unlike with Lean 3 I don't know how to do it. In mathlib4_experiments there is #print prefix but it only gives this:

nat.add : nat → nat → nat
nat.add._cstage1 : nat → nat → nat
nat.add._cstage2 : _obj → _obj → _obj
nat.add._sunfold : nat → nat → nat
nat.add._unsafe_rec : nat → nat → nat
nat.add.match_1 : (motive : nat → nat → Sort u_1) →
(a b : nat) →
((a : nat) → motive a nat.zero) →
((b : nat) → motive nat.zero b) → ((a b : nat) → motive a (nat.succ b)) → motive a b
nat.add.match_1._cstage1 : (motive : nat → nat → Sort u_1) →
(a b : nat) →
((a : nat) → motive a nat.zero) →
((b : nat) → motive nat.zero b) → ((a b : nat) → motive a (nat.succ b)) → motive a b
nat.add.match_1._rarg._cstage2 : _obj → _obj → _obj → _obj → _obj → _obj


#### Kevin Buzzard (May 10 2021 at 07:38):

In Lean 3 you get equation compiler error, equation #2 has not been used in the compilation (possible solution: delete equation)

#### Kevin Buzzard (May 10 2021 at 07:39):

PS can you fix your example so it's a #mwe ? You haven't defined notation + but you're using it.

#### Mario Carneiro (May 10 2021 at 08:23):

Lean 4 is not (yet) generating equation lemmas for definitions

Last updated: Dec 20 2023 at 11:08 UTC