match pattern not rfl-ing with match argument

Stream: lean4

[Dmitry Ivankov]

Or even shorter example

def countdown (x : Nat) : Nat := match x with
 | 0 => 0
 | z@(y + 1) =>
   let x_pred := x.pred -- "y" would work as well as "z.pred", but let's use "x.pred" because "x" is also in scope
   have : y = x_pred := by sorry -- is it possible to prove this? or that "z=x"?
   /- without "have" we'll get
failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
x y : Nat
x_pred : Nat := Nat.pred x
⊢ Nat.pred x < Nat.succ y
   -/
   1 + (countdown x_pred)
termination_by countdown x => x -- same as the default but with better error message

For my current thing just not referring to outer name of function argument works well enough, maybe this is never an issue and can be resolved by capturing matched name. But still not sure if it would be possible to automatically have a proof "x=z" or is it maybe contradicting how lean works

[Mario Carneiro]

def countdown (x : Nat) : Nat :=
 match e : x with
 | 0 => 0
 | (y + 1) =>
   let x_pred := x.pred
   have : y = x_pred := congrArg Nat.pred e

[Mario Carneiro]

the e : syntax gives you a proof that x is equal to the cases in the match