leanprover/lean4

Recursive theorems with `cases` vs `match`

Opened this issue · 3 comments

hargoniX commented

Prerequisites

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

Description

Consider:

inductive C : Nat → Type where
| C0  : C 0
| C1  : C n → C (1 + n)
| C2  : C n → C n → C n

open C

def id_C (c : C n) : C n :=
  match c with
  | C0       => C0
  | C1 c     => C1 (id_C c)
  | C2 c₁ c₂ => C2 (id_C c₁) (id_C c₂)

We can prove the following theorem with match or induction:

theorem id_c_is_identity (c : C n) : id_C c = c := by
  match c with
  | C0 => simp [id_C]
  | C1 inner => simp [id_C, id_c_is_identity inner]
  | C2 lhs rhs => simp [id_C, id_c_is_identity lhs, id_c_is_identity rhs]

this will use the structural termination metric on c as expected.
However the following:

theorem id_c_is_identity (c : C n) : id_C c = c := by
  cases c with
  | C0 => simp [id_C]
  | C1 inner => simp [id_C, id_c_is_identity inner]
  | C2 lhs rhs => simp [id_C, id_c_is_identity lhs, id_c_is_identity rhs]

Fails to prove termination, if we force a use of the structural metric:

theorem id_c_is_identity (c : C n) : id_C c = c := by
  cases c with
  | C0 => simp [id_C]
  | C1 inner => simp [id_C, id_c_is_identity inner]
  | C2 lhs rhs => simp [id_C, id_c_is_identity lhs, id_c_is_identity rhs]
termination_by structural c

We get

failed to infer structural recursion:
Cannot use parameter c:
  failed to eliminate recursive application
    id_c_is_identity lhs

Steps to Reproduce

Expected behavior: Given that it works with match it should either also work with cases or there should be a better error message explaining why that is not the case (haha).

Actual behavior: match works, cases doesn't.

Versions

"4.12.0-nightly-2024-10-13"

Impact

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

nomeata commented

What happens if you pass explicit arguments to the theorem before passing them to rw? I.e. is the problem with rw or with cases?

hargoniX commented

Breaks in the same fashion, updated the issue to align the code.

  • 👍1
nomeata commented

Interestingly the issue is only with C2, not with C1.

Initial debugging with set_option trace.Elab.definition true: This is the predefinition with cases

id_c_is_identity : ∀ {n : Nat} (c : C n), id_C c = c :=
    fun {n} c =>
      C.casesOn (motive := fun a t => n = a → HEq c t → id_C c = c) c
        (fun h =>
          Eq.ndrec (motive := fun {n} => ∀ (c : C n), HEq c C.C0 → id_C c = c)
            (fun c h => Eq.symm (eq_of_heq h) ▸ of_eq_true (eq_self C.C0)) (Eq.symm h) c)
        (fun {n_1} inner h =>
          Eq.ndrec (motive := fun {n} => ∀ (c : C n), HEq c inner.C1 → id_C c = c)
            (fun c h =>
              Eq.symm (eq_of_heq h) ▸
                of_eq_true
                  (Eq.trans (congrArg (fun x => x.C1 = inner.C1) (_root_.id_c_is_identity n_1 inner))
                    (eq_self inner.C1)))
            (Eq.symm h) c)
        (fun {n_1} lhs rhs h =>
          Eq.ndrec (motive := fun {n_2} => ∀ (lhs rhs : C n_2), HEq c (lhs.C2 rhs) → id_C c = c)
            (fun lhs rhs h =>
              Eq.symm (eq_of_heq h) ▸
                of_eq_true
                  (Eq.trans
                    (congrArg (fun x => x = lhs.C2 rhs)
                      (congr (congrArg C.C2 (_root_.id_c_is_identity n lhs)) (_root_.id_c_is_identity n rhs)))
                    (eq_self (lhs.C2 rhs))))
            h lhs rhs)
        (Eq.refl n) (HEq.refl c)

and this with match:

id_c_is_identity : ∀ {n : Nat} (c : C n), id_C c = c :=
    fun {n} c =>
      match n, c with
      | .(0), C.C0 => of_eq_true (eq_self C.C0)
      | .(1 + n), inner.C1 =>
        of_eq_true (Eq.trans (congrArg (fun x => x.C1 = inner.C1) (_root_.id_c_is_identity n inner)) (eq_self inner.C1))
      | n, lhs.C2 rhs =>
        of_eq_true
          (Eq.trans
            (congrArg (fun x => x = lhs.C2 rhs)
              (congr (congrArg C.C2 (_root_.id_c_is_identity n lhs)) (_root_.id_c_is_identity n rhs)))
            (eq_self (lhs.C2 rhs)))

Clearly the cases construction, with C.casesOn, is more complicated. There is still a chance that the transformation done for structural recursion (with the C.below value pushed into the C.casesOn could work here, but hard to tell without digging deeper (i.e. adding more tracing.)

Using well-founded recursion one gets

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
n✝ : Nat
c : C n✝
a✝² : ∀ (y : C n✝), (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y c → id_C y = y
n : Nat
a✝¹ a✝ : C n
x✝ : ∀ (y : C n), (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 y (a✝¹.C2 a✝) → id_C y = y
h✝¹ : n✝ = n
lhs rhs : C n✝
h✝ : HEq c (lhs.C2 rhs)
⊢ sizeOf lhs < 1 + n + sizeOf a✝¹ + sizeOf a✝

and notices that there is a HEq that isn't actually heterogenous at this point, so maybe that’s also a lead.

Anyways, this first investigation does not point to a quick fix, and there seems to be a work-around, so will not dig deeper until this happens more often or becomes a clear blocker.