Termination goal for a wf recursive function involving `cases` lacks necessary hypotheses

[datokrat]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

I have a situation in which a well-founded recursive function produces a decreasing_by goal that lacks necessary information about a cases-based match on the recursion variable. If I replace the cases tactic with a match expression, it works.

This might be related to #5690 in that highlights a difference of cases and match, but the symptoms seem different.

Steps to Reproduce

Consider this example:

inductive P1 : Nat → Type where
  | nil : P1 n
  | p1 : P1 n → P1 (n + 1)

opaque P2 : Nat → Type

/--
error: unsolved goals
case refl.refl.refl.refl
n✝ : Nat
a✝ : P1 n✝
p1 : P1 (n✝ + 1)
p2 : P2 (n✝ + 1)
this : sizeOf a✝ < sizeOf a✝.p1
β : Type
⊢ sizeOf a✝ < sizeOf p1
-/
#guard_msgs in
def f (p1 : P1 ms) (p2 : P2 ms) : Unit := by
  cases hp1 : p1
  · exact ()
  · rename_i p1'
    -- recursive call is decreasing:
    have : sizeOf p1' < sizeOf p1 := by simp [hp1]; omega
    -- recursive call:
    exact f p1' sorry
termination_by sizeOf p1
decreasing_by
  · subst_eqs

(The example works with structural recursion, but my real-world use case doesn't.)

Expected behavior:

Because p1 = P1.p1 p1', it should be possible to use this fact to close the termination goal.

Actual behavior:

Because p1 is a free variable without any information about its size or its relation to a✝ (which seems to be the name for p1' in the termination goal), it is impossible to finish the termination proof.

Also note that the have :sizeOf p1' < sizeOf p was transformed into a tautology in the termination goal.

Versions

Lean 4.23.0-rc2
Target: x86_64-unknown-linux-gnu

Impact

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

[nomeata]

Confirmed. I am hesitant to attempt to fix this, though: The code produced by cases is rather gnarly, and massaging that in the wf preprocessor to expose the necessary equation feels dangerous:

f.eq_def {ms : Nat} (p1 : P1 ms) (p2 : P2 ms) :
  f p1 p2 =
    P1.casesOn (motive := fun a t => ms = a → p1 ≍ t → Unit) p1
      (fun {n} h =>
        Eq.ndrec (motive := fun {n} => p1 ≍ P1.nil → Unit)
          (fun h => Eq.ndrec (motive := fun x => p1 = x → Unit) (fun hp1 => ()) (f._proof_2 p1 h) (f._proof_3 p1)) h)
      (fun {n} a h =>
        Eq.ndrec (motive := fun {ms} => (p1 : P1 ms) → P2 ms → (x : P1 ms) → p1 = x → x ≍ a.p1 → Unit)
          (fun p1 p2 x hp1 h =>
            Eq.ndrec (motive := fun x => p1 = x → Unit)
              (fun hp1 =>
                have this := f._proof_4 a p1 hp1;
                f a sorry)
              (f._proof_5 a x h) hp1)
          (f._proof_6 h) p1 p2 p1 (f._proof_3 p1))
      (Eq.refl ms) (f._proof_7 p1)

So given that a work-around exists I’d say let’s observe the situation.

[datokrat]

Agreed!

[datokrat]

Let me point out two situations with a similar problem, this time about change/unfold/let:

def N := Nat

def f (n : N) : Nat := by
  change Nat at n -- `unfold` doesn't help either
  match n with
  | 0 => exact 0
  | n + 1 => exact f n
termination_by n
decreasing_by
  sorry

def f' (n : N) : Nat := by
  let n' : Nat := n
  match n' with
  | 0 => exact 0
  | n + 1 => exact f' n
termination_by n
decreasing_by
  sorry

def controlGroup (n : Nat) : Nat := by
  match n with
  | 0 => exact 0
  | n + 1 => exact controlGroup n
termination_by n
decreasing_by
  grind

#print f
#print f'
#print controlGroup

In both cases, it is impossible to fill the decreasing goal given the available hypotheses. Version:

Lean 4.24.0-nightly-2025-09-07
Target: x86_64-unknown-linux-gnu

Perhaps the problem might not be about cases, after all. (I must say that I haven't taken a deep enough stare at the cases gobbledygook output to understand whether the cases case is special 😬)

I'm hesitating to create a bug issue right now because it might well be a related problem, but I am happy to create a separate one if deemed worthwhile.

(I'm coming to the conclusion that the project (which is a free-time activity and not critical) I'm working on is cursed :D)