simp: maximum recursion depth

Stream: lean4

[Marcus Rossel]

Is this expected?:

variable (h : ∀ (p : Nat → Nat) (x : Nat), p x = p (x + 0))

example (f : Nat → Nat → Nat) : (f 1) x = (f 1) (x + 0) := by
  simp [h] -- tactic 'simp' failed, nested error: maximum recursion depth has been reached

[Sébastien Gouëzel]

Yes, it's expected. Lean sees (f 1) x, it replaces it with (f 1) (x + 0) thanks to h, then with (f 1) (x + 0 + 0) thanks to h, and so on. It doesn't zoom out after the first step to see that the equality becomes trivial, because it completes its work on a subexpression before zooming out.