unfolding induction principle: incomplete reduction of matches

This is a continuation of #8195, which has been improved and merged, but there are certainly more more cases were it needs improvement.

I don’t expect we’ll manage to make this work in every case, so we’ll collect examples here and fix them when they become blockers or when they are easily fixed.

Here one reported by @Rob23oba:

inductive MyVec (α : Type u) : Nat → Type u where
  | nil : MyVec α 0
  | cons : α → MyVec α n → MyVec α (n + 1)

def test (f : Unit → MyVec α n) : Nat :=
  match f () with
  | .nil => 52
  | .cons _ _ => 421

/--
info: test.fun_cases_unfolding.{u_1} (motive : {α : Type u_1} → {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
  (case1 :
    ∀ {α : Type u_1} (f : Unit → MyVec α 0),
      f () = MyVec.nil →
        motive f
          (match 0, f (), f with
          | .(0), MyVec.nil, f => 52
          | .(n + 1), MyVec.cons a a_1, f => 421))
  (case2 :
    ∀ {α : Type u_1} (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
      f () = MyVec.cons a a_1 →
        motive f
          (match n + 1, f (), f with
          | .(0), MyVec.nil, f => 52
          | .(n + 1), MyVec.cons a a_2, f => 421))
  {α : Type u_1} {n : Nat} (f : Unit → MyVec α n) : motive f (test f)
-/
#guard_msgs in
#check test.fun_cases_unfolding

def alsoTest (f : Unit → MyVec α n) : Nat :=
  match h : f () with
  | .nil => 52
  | .cons _ _ => 421

/--
info: alsoTest.fun_cases_unfolding.{u_1} (motive : {α : Type u_1} → {n : Nat} → (Unit → MyVec α n) → Nat → Prop)
  (case1 :
    ∀ {α : Type u_1} (f : Unit → MyVec α 0),
      f () = MyVec.nil →
        motive f
          (match h : 0, h : f (), f with
          | .(0), MyVec.nil, f_1 => 52
          | .(n + 1), MyVec.cons a a_1, f_1 => 421))
  (case2 :
    ∀ {α : Type u_1} (n : Nat) (a : α) (a_1 : MyVec α n) (f : Unit → MyVec α (n + 1)),
      f () = MyVec.cons a a_1 →
        motive f
          (match h : n + 1, h : f (), f with
          | .(0), MyVec.nil, f_1 => 52
          | .(n_1 + 1), MyVec.cons a a_2, f_1 => 421))
  {α : Type u_1} {n : Nat} (f : Unit → MyVec α n) : motive f (alsoTest f)
-/
#guard_msgs in
#check alsoTest.fun_cases_unfolding

Versions

Lean 4.21.0-nightly-2025-05-12

Impact

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

Start by reproducing the two examples in the issue with Lean 4.21.0-nightly-2025-05-12 and inspect the generated fun_cases_unfolding output. Read the implementation and merged changes from #8195 to understand the existing unfolding behavior. Done means the reported matches reduce more completely while the guard messages pass.