Failed rewrite by equation lemmas

Stream: lean4

[Heather Macbeth]

The first of these works but the second fails. Is this expected behaviour?

def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

example (a : Nat) : factorial (a + 1) = (a + 1) * factorial a := by
  rw [factorial] -- works

example (a b : Nat) : factorial ((a + b) + 1) = ((a + b) + 1) * factorial (a + b) := by
  rw [factorial] -- fails

[Heather Macbeth]

The error message is

failed to rewrite using equation theorems for 'factorial'

[Mario Carneiro]

sounds like a bug somewhere in core, probably rw latched on the wrong addition

[Mario Carneiro]

note that it works with factorial (Nat.succ (a + b)) on the left; the actual equation lemma uses Nat.succ

[Heather Macbeth]

I really appreciate having the version with a + 1 rather than Nat.succ a, when it works -- I hope it's not too hard to fix.

[Mario Carneiro]

minimized:

opaque zero : Nat → Nat
theorem foo : zero (Nat.succ a) = 0 := sorry
example : zero (a + 1) = 0 := by with_reducible exact foo -- ok
example : zero (a + a + 1) = 0 := by with_reducible exact foo -- fail

[Heather Macbeth]

I opened lean4#2136 for this.