Nat.add n 0 expressions appear when unfolding with simp (but not with rw)

[kmill]

Description

When using unfold or simp to unfold a recursive function, the expression Nat.add n 0 appears inside the body of the unfolded function rather than n. In the following example, you can uncomment the unfold or simp lines to see the given goal state. In contrast, rw results in the wanted state.

def foo : Nat → Nat
  | 0 => 2
  | n + 1 => foo n

example (n : Nat) : foo (n + 1) = 2 := by
  --unfold foo      -- ⊢ foo (Nat.add n 0) = 2
  --simp only [foo] -- ⊢ foo (Nat.add n 0) = 2
  --rw [foo]        -- ⊢ foo n = 2
  sorry

Expected behavior: In each of these three commented out lines, the goal state becomes ⊢ foo n = 2.

Actual behavior: Only the rw tactic results in the expected goal state.

Context

When using a custom eliminator in the induction or cases tactic for Nat that uses 0 and n + 1 rather than Nat.zero and Nat.succ n, expressions such as foo (n + 1) occur. If this is a proof about foo, then it is natural to unfold it. However, using unfold or simp results in expressions with Nat.add n 0. Eliminating these requires further application of lemmas such as Nat.add_eq and add_zero to clean up the expression.

protected def Nat.recAux {motive : Nat → Sort _}
    (zero : motive 0) (succ : ∀ n, motive n → motive (n+1)) : (t : Nat) → motive t
  | 0 => zero
  | _+1 => succ _ (Nat.recAux zero succ _)

example (n : Nat) : foo n = 2 := by
  induction n using Nat.recAux with
  | zero => rfl
  | succ n ih =>
    --unfold foo      -- ⊢ foo (Nat.add n 0) = 2
    --simp only [foo] -- ⊢ foo (Nat.add n 0) = 2
    --rw [foo]        -- ⊢ foo n = 2
    exact ih

This is an obstruction to the "beautiful induction for Nat" project. We do not want users to see Nat.add expressions.

Versions

MacOS arm64

#eval Lean.versionString -- "4.4.0-rc1"

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[kmill]

@leodemoura This issue is an obstruction to moving forward with using nicer eliminators when doing Nat induction. Do you think it could be easily fixed?