decreasing_by goal with nested recursion mentions internal induction hypothesis

Consider

def ack : Nat → Nat → Nat
  | 0,   y   => y+1
  | x+1, 0   => ack x 1
  | x+1, y+1 => ack x (ack (x+1) y)
termination_by a b => (a, b)
decreasing_by
  · decreasing_tactic
  · decreasing_tactic
  · trace_state
    decreasing_tactic

This will show

x y : Nat
x✝ : (y_1 : (_ : Nat) ×' Nat) →
  (invImage (fun x => PSigma.casesOn x fun a a_1 => (a, a_1)) Prod.instWellFoundedRelation).1 y_1 ⟨x.succ, y.succ⟩ → Nat
⊢ (invImage (fun x => PSigma.casesOn x fun a a_1 => (a, a_1)) Prod.instWellFoundedRelation).1 ⟨x, x✝ ⟨x + 1, y⟩ ⋯⟩
  ⟨x.succ, y.succ⟩

Note the scary-looking and unhelpful x✝ assumption. This is an artifact of the internal. construction using WellFounded.fix, namely the “induction hypothesis” of that function.

Usually lean hides that by calling MVarId.cleanup, and that’s why it is not shown in in the first to subgoals. But here, it is not cleaned up because the goal mentions it.

Sometimes running simp_wf will remove the dependency, so in some cases running cleanup again after that (possible by default after #5016) helps, but it would not in this case; after simp_wf the goal is still

⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (x, x✝ ⟨x + 1, y⟩ ⋯) (x + 1, y + 1)

and mentions x✝.

Maybe it should generalize all applications of x✝, leaving the whole expression abstract, i.e.

x y : Nat
a✝ : Nat
⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => a₁ < a₂) (x, a✝) (x + 1, y + 1)

which obscures the origin of this term a bit, but on the other hand makes it clear that there is nothing useful to be known about it.

Versions

4.11

Additional Information

I guess this is mostly a cosmetic issue, in the sense that a user can lean to ignore these assumptions, but it does look very scary and for example Mario writes about this:

I actually use decreasing_by very rarely, because the goals are such a mess that it's easier to just work in situ using have :=

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60simp_wf.60.20in.20.60decreasing_by.60/near/462208515

Impact

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

Reproduce the nested-recursion ack example and inspect the decreasing_by goals, especially the internal induction-hypothesis application. Start by tracing MVarId.cleanup and simp_wf behavior; done means the generated goal no longer exposes an unhelpful internal hypothesis, or the intended generalization behavior is established.