`induct_unfolding` fails to unfold some `match` expressions

[Rob23oba]

Prerequisites

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

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• 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

The induct_unfolding and fun_cases_unfolding constructions sometimes splits match cases without unfolding.

Context

This occurred while working on tree maps, in particular trying to use unfolding induction on Std.DTreeMap.Internal.Impl.explore.

Steps to Reproduce

def test (l : List Nat) : Nat :=
  match l with
  | [] => 0
  | x :: l =>
    match x == 3 with
    | false => test l
    | true => test l

#print test.induct_unfolding

The generated induction looks like this:

test.induct_unfolding (motive : List Nat → Nat → Prop) (case1 : motive [] 0)
  (case2 :
    ∀ (x : Nat) (l : List Nat),
      (x == 3) = false →
        motive l (test l) →
          motive (x :: l)
            (match x == 3 with
            | false => test l
            | true => test l))
  (case3 :
    ∀ (x : Nat) (l : List Nat),
      (x == 3) = true →
        motive l (test l) →
          motive (x :: l)
            (match x == 3 with
            | false => test l
            | true => test l))
  (l : List Nat) : motive l (test l)

You can see that the match x == 3 has been split into cases 2 and 3, however, the match expression was not reduced. The expected behavior would've been something like:

test.induct_unfolding2 (motive : List Nat → Nat → Prop) (case1 : motive [] 0)
  (case2 : ∀ (x : Nat) (l : List Nat), (x == 3) = false → motive l (test l) → motive (x :: l) (test l))
  (case3 : ∀ (x : Nat) (l : List Nat), (x == 3) = true → motive l (test l) → motive (x :: l) (test l))
  (l : List Nat) : motive l (test l)

where the match x == 3 has been reduced into its cases, here test l.
Note: The same problem occurs with fun_cases_unfolding. Writing test using an if-then-else instead causes the issue to disappear.

Versions

Lean 4.20.0-nightly-2025-05-01

Impact

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

[nomeata]

Thanks for the report! I'm not entirely surprised, rewriting matches is hairy. At least the principle isn't wrong per se, and a suitable simp will clean up the goal, will it?

Anyways, thanks for the test cases and keep em coming.

[Rob23oba]

Yes it will for this one but when the match gets dependent it gets worse:

opaque someFunction (x : Nat) (h : (x == 3) = false) : Nat
opaque someOtherFunction (x : Nat) (h : (x == 3) = true) : Nat

def test (l : List Nat) : Nat :=
  match l with
  | [] => 0
  | x :: l =>
    match h : x == 3 with
    | false => test l + someFunction x h
    | true => test l + someOtherFunction x h

#print test.induct_unfolding

example (l : List Nat) : test l = sorry := by
  induction l using test.induct_unfolding with
  | case1 => sorry
  | case2 x l h ih =>
    simp [h] -- fails
  | case3 x l h ih =>
    simp [h] -- fails

Another test case for you :-)
I imagine the way you could make splitting work is by using whatever split is doing (because that actually works at the place of the simp [h]).
Edit: Arguably simp should work here but that's another thing to worry about.

[nomeata]

I imagine the way you could make splitting work is by using whatever split is doing

I was hoping I was doing that :-)

[Rob23oba]

I'm not sure whether this should really be reported as a bug but:

def aaffcadvr {β : Nat → Sort _} (f : (n : Nat) → β n) : β 24 :=
  letFun 24 (fun n => f n)

/--
error: Failed to realize constant aaffcadvr.fun_cases_unfolding:
  Cannot derive functional cases principle (please report this issue)
  
    application type mismatch
      motive f (f n)
    argument
      f n
    has type
      β n : Sort u_1
    but is expected to have type
      β 24 : Sort u_1
---
error: unknown constant 'aaffcadvr.fun_cases_unfolding'
---
error: constructed functional cases principle is not type correct:
  fun motive case1 {β} f =>
    Eq.mpr (congrArg (motive f) (aaffcadvr.eq_def f))
      (let_fun n := 24;
      Eq.mpr (Eq.refl (motive f (f n))) (case1 f n))

-/
#guard_msgs in
#print aaffcadvr.fun_cases_unfolding

[nomeata]

Yes, definitely a (separate) bug. The code should at least recognize if there is a case it can’t handle.

[nomeata]

I imagine the way you could make splitting work is by using whatever split is doing (because that actually works at the place of the simp [h]).

I had a look, optimistically thinking this would be a relatively easy late evening bug fixing, but it really looks gnarly.

We have

(x == 3) = false

in the context (put there by the match splitter) and want to reliably rewrite the expression

match x == 3 with
| false => test l
| true => test l

Its at least tedious to let simp reduce the matcher without rewriting too much, and as you showed, simp may not be able to do it.

But “Using what split is doing” is also not simple, because it’s a big complicated tactic. Maybe if I expose Lean.Meta.Split.substDiscrEqs and use that together with Lean.Meta.Split.simpMatchTargetCore?

This is all very annoying, and kinda throws a wrench into my planning for this feature here.

[Rob23oba]

One idea I had was a "match cases" lemma, so something like:

def myTest (x : List α) : Nat := by
  match h : x with
  | a :: dc => sorry
  | _ => sorry

attribute [elab_as_elim] myTest.match_1.splitter

theorem myTest.match_1.cases {α : Type u}
    (motive : (x : List α) → Sort v)
    {motive' : (x : List α) → motive x → Prop}
    (x : List α) :
    (h_1 : (a : α) → (dc : List α) → x = a :: dc → motive (a :: dc)) →
    (h_2 : (x' : List α) → x = x' → motive x') →
    (case1 : (a : α) → (dc : List α) → (h : x = a :: dc) → motive' (a :: dc) (h_1 a dc h)) →
    (case2 : (x' : List α) → (∀ (a : α) (dc : List α), x = a :: dc → False) → (h : x = x') → motive' x' (h_2 x' h)) →
    motive' x (myTest.match_1 motive x h_1 h_2) := by
  refine myTest.match_1.splitter _ x ?_ ?_
  · intro a dc h h_1 h_2 case1 case2
    refine Eq.substr (myTest.match_1.eq_1 motive a dc h_1 h_2) ?_
    apply case1
  · intro x hx! h h_1 h_2 case1 case2
    refine Eq.substr (myTest.match_1.eq_2 motive x h_1 h_2 hx!) ?_
    apply case2
    exact hx!

This comes with a problem though which is, that in practice, the motive must not depend on anything but the function application (example where it does work is iteInduction), motive' here depends on x as well which causes problems because then suddenly the body changes type within the cases. This is somewhat to be expected and comes from the fact that sometimes it's simply impossible to reliably rewrite without introducing a cast (exactly then when the motive / return type of match depends on its parameters).
Thankfully, for the case where the motive is fixed, this is easily avoidable:

theorem myTest.match_1.cases {α : Type u} {β : Sort v}
    {motive : β → Prop} (x : List α) :
    (h_1 : (a : α) → (dc : List α) → x = a :: dc → β) →
    (h_2 : (x' : List α) → x = x' → β) →
    (case1 : (a : α) → (dc : List α) → (h : x = a :: dc) → motive (h_1 a dc h)) →
    (case2 : (x' : List α) → (∀ (a : α) (dc : List α), x = a :: dc → False) → (h : x = x') → motive (h_2 x' h)) →
    motive (myTest.match_1 (fun _ => β) x h_1 h_2) := by
  refine myTest.match_1.splitter _ x ?_ ?_
  · intro a dc h h_1 h_2 case1 case2
    refine Eq.substr (myTest.match_1.eq_1 _ a dc h_1 h_2) ?_
    apply case1
  · intro x hx! h h_1 h_2 case1 case2
    refine Eq.substr (myTest.match_1.eq_2 (fun _ => β) x h_1 h_2 hx!) ?_
    apply case2
    exact hx!

This now actually works as a usable lemma to split with (note: we might not need to generate such a lemma but instead maybe just use this general shape (using match_1.splitter in combination with Eq.substr and match_1.eq_n)).

[Rob23oba]

Oops that was not my intention

[nomeata]

That looks a bit like a functional cases theorem with unfolding for the match statement, doesn't it?

It's somewhat natural that such a thing would be a good, compositional building block for building unfolding theorems for functions using match statements.

[nomeata]

This comes with a problem though which is, that in practice, the motive must not depend on anything but the function application

Your first theorem myTest.match_1.cases seems to pretty close to what what myTest.fun_cases_unfolding should look like, though. So it seems that if we can pull off the whole .fun_cases_unfolding trick, then this is what we need, isn’t it?

Where exactly do you see a problem with that theorem?

[nomeata]

I wonder if we can have more general rewriting equations for the match that include the rewriting of the match discriminant? But (as you said above) that doesn't work easily without a cast:

theorem myTest.match_1.gen_eq_1 {α : Type u}
  (motive : (x : List α) → Sort v)
  (x : List α)
  (h_1 : (a : α) → (dc : List α) → x = a :: dc → motive (a :: dc))
  (h_2 : (x' : List α) → x = x' → motive x')
  (a : α) (dc : List α) (h : x = a :: dc)
  : myTest.match_1 motive x h_1 h_2 = h ▸ h_1 a dc h := by
  subst h; rfl

But then, maybe that’s good enough, using HEq

theorem myTest.match_1.heq_1 {α : Type u}
  (motive : (x : List α) → Sort v)
  (x : List α)
  (h_1 : (a : α) → (dc : List α) → x = a :: dc → motive (a :: dc))
  (h_2 : (x' : List α) → x = x' → motive x')
  (a : α) (dc : List α) (h : x = a :: dc)
  : HEq (myTest.match_1 motive x h_1 h_2) (h_1 a dc h) := by
  subst x
  apply heq_of_eq
  apply myTest.match_1.eq_1 motive a dc h_1 h_2

theorem myTest.match_1.heq_2 {α : Type u}
  (motive : (x : List α) → Sort v)
  (x : List α)
  (h_1 : (a : α) → (dc : List α) → x = a :: dc → motive (a :: dc))
  (h_2 : (x' : List α) → x = x' → motive x')
  (x' : List α)
  (hoverlap : ∀ (a : α) (dc : List α), x' = a :: dc → False)
  (h : x = x')
  : HEq (myTest.match_1 motive x h_1 h_2) (h_2 x' h) := by
  subst x
  apply heq_of_eq
  apply myTest.match_1.eq_2 motive x' h_1 h_2 hoverlap

and then using HEq.subst may actually help us here (if my withRewrittenMotiveArg function can handle HEq here.)

But I am somewhat out of my depth here, I admit.