Trouble with a `rw`

Stream: lean4

[Mac]

So I have been toying around with Nat.add that is not left or right recursive and while trying to prove add_succ I ran into the following problem, which I think may be an bug in Lean, but I am not sure.

open Nat (zero succ)

def add : Nat → Nat → Nat
| 0, 0 => 0
| succ n, 0 => succ n
| 0, succ n => succ n
| succ m, succ n => succ (succ (add m n))

infixl:65 (priority := high) " + " => add

instance : Add Nat := ⟨add⟩ -- removing this fixes the theorem error

@[simp] theorem succ_zero : succ 0 = 1 := rfl

@[simp] theorem zero_add_zero : 0 + 0 = 0 := rfl

@[simp] theorem add_zero : n + 0 = n := by cases n; repeat rfl
@[simp] theorem zero_add : 0 + n = n := by cases n; repeat rfl

theorem succ_add_succ : succ m + succ n = succ (succ (m + n)) := rfl

@[simp] theorem add_one : n + 1 = succ n := by
  cases n with | zero => rfl | succ n => rw [succ_add_succ, add_zero]

@[simp] theorem one_add : 1 + n = succ n := by
  cases n with | zero => rfl | succ => rw [succ_add_succ, zero_add]

-- error: theorem fails despite goals accomplished
theorem add_succ {m n : Nat} : m + succ n = succ (m + n) := by
  revert m
  induction n with
  | zero => simp
  | succ n ih =>
    intro m
    cases m with
    | zero => simp
    | succ m =>
      rw [succ_add_succ, succ_add_succ] -- produces an `n + 1` for some reason
      show succ (succ (m + succ n)) = succ (succ (succ (m + n)))
      rw [@ih m]

The error on add_succ is as follows:

application type mismatch
  @Eq.ndrec Nat (succ m + succ (n + 1))
    (fun _a => (succ m + succ (succ n) = succ (succ m + succ n)) = (_a = succ (succ m + succ n)))
    (Eq.refl (succ m + succ (succ n) = succ (succ m + succ n)))
argument has type
  (succ m + succ (succ n) = succ (succ m + succ n)) = (succ m + succ (succ n) = succ (succ m + succ n))
but function has type
  (fun _a => (succ m + succ (succ n) = succ (succ m + succ n)) = (_a = succ (succ m + succ n)))
      (succ m + succ (n + 1)) →
    ∀ {b : Nat},
      succ m + succ (n + 1) = b →
        (fun _a => (succ m + succ (succ n) = succ (succ m + succ n)) = (_a = succ (succ m + succ n))) b

I am very confused as to why the n + 1 is introduced during rewriting. I am also curious as to why removing the Add instance fixes the error (and why the n + 1 still appears even then). Is this some weird bug in rw (or show) or are there details I am missing?

[Mario Carneiro]

Here's a minimized version:

open Nat

def add : Nat → Nat → Nat
| 0, 0 => 0
| succ n, 0 => succ n
| 0, succ n => succ n
| succ m, succ n => succ (succ (add m n))

instance : Add Nat := ⟨add⟩ -- removing this fixes the theorem error

theorem succ_add_succ : succ m + succ n = succ (succ (m + n)) := rfl

theorem add_succ : succ m + succ (succ n) = 0 := by
  rw [succ_add_succ]
  sorry

This is certainly a bug, and my guess is that it is caused by something that has a hardcoded match on Add.add Nat thinking that it's surely Nat.add and your alternate definition is confusing it. (Lean 3 simp has the same problem with numerals encoded using nonstandard instances of standard typeclasses)

[Kevin Buzzard]

So the problem should go away if you try this on a custom nat'?