weird nat unification behaviour

Stream: lean4

[Edward van de Meent]

i came across the following:

inductive foo : Nat → Type _ where
  | zero : foo 0
  | succ n : foo n → foo (n + 1)

example (x : foo 5) : x = x := by
  cases x with
  | succ _ a =>
    /-
    a : foo (0 + 4)
    ⊢ foo.succ (0 + 4) a = foo.succ (0 + 4) a
    -/
    cases a with
    | succ _ b =>
      /-
      b : foo (0 + 3)
      ⊢ foo.succ (0 + 4) (foo.succ (0 + 3) b) = foo.succ (0 + 4) (foo.succ (0 + 3) b)
      -/
      sorry

for whatever reason, lean uses 0+n here rather than just n. is there a reason for this?
I did a simple test unifying 5 with Nat.succ ?m and it doesn't display this behaviour:

import Lean.Expr
import Lean.Meta

open Lean Meta
run_meta do
  let four? ← mkFreshExprMVar (.some (.const ``Nat []))
  four?.mvarId!.setUserName `four
  let five? ← mkAppM ``Nat.succ #[four?]
  let five : Expr := .lit (.natVal 5)
  logInfo m!"five?:{five?}, five:{five}" -- five?:Nat.succ ?four, five:5
  let b ← isDefEq five? five
  logInfo m!"isDefEq:{b}" -- isDefEq:true
  let four ← instantiateMVars four?
  logInfo m!"four:{four}" -- four:4

i have two questions:

• What is the mechanism that causes this to happen?
• Is this behaviour chosen on purpose, and if so, why?

[Jovan Gerbscheid]

That's very strange. It's specifically the cases tactic doing this. It behaves normally with match.