Pattern matching and proving with rfl

Stream: new members

[Brandon Brown]

[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]

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"
    rw [add_succ,c]

[Kevin Buzzard]

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]

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]

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._cstage2 : _neutral → _obj
nat.add.match_1._rarg._cstage2 : _obj → _obj → _obj → _obj → _obj → _obj

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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