"failed to generate equational theorem" with nested matches

[soulsource]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The unfold tactic fails with nested matches, for instance:

inductive Tree (α : Type u) : Nat → Type u
  | leaf : Tree α 0
  | branch :
    (val : α)
    → (left : Tree α n)
    → (right : Tree α m)
    → Tree α (n+m+1)

def popLast {α : Type u} (heap : Tree α (o+1)) : (α × Tree α o) :=
  match o, heap with
  | (n+m), .branch a (left : Tree α n) (right : Tree α m)  =>
    if r : m = 0 then
      --remove left
      match n, left with
      | 0, _ => (a, (Eq.symm $ r.subst $ Nat.zero_add m : 0=0+m)▸Tree.leaf)
      | (l+1), left =>
        let (res, (newLeft : Tree α l)) := popLast left
        (res, (Nat.add_right_comm l m 1)▸Tree.branch a newLeft right)
    else
      --remove right
      match  m, right with
      | (r+1), right =>
        let (res, (newRight : Tree α r)) := popLast right
        (res, Tree.branch a left newRight)

def SomePredicate (_ : Tree α n) : Prop := True

theorem whatever : SomePredicate ((popLast heap).snd) := by
  unfold popLast
  sorry

(Lean4 Web link)

The issue seems to be related to the nested matches, because for this slightly refactored code snippet unfold does work:

inductive Tree (α : Type u) : Nat → Type u
  | leaf : Tree α 0
  | branch :
    (val : α)
    → (left : Tree α n)
    → (right : Tree α m)
    → Tree α (n+m+1)

def popLast {α : Type u} (heap : Tree α (o+1)) : (α × Tree α o) :=
  match o, heap with
  | (n+m), .branch a (left : Tree α n) (right : Tree α m)  =>
    match r : m, right with
    | 0, _ => 
      --remove left
      match n, left with
      | 0, _ => (a, Tree.leaf)
      | (l+1), left =>
        let (res, (newLeft : Tree α l)) := popLast left
        have blah := r.subst (motive := λmx ↦ l + m + 1 = l + 1 + mx) (Nat.add_right_comm l m 1)
        (res, blah▸Tree.branch a newLeft right)
    | (o+1), right =>
      --remove right
        let (res, newRight) := popLast right
        (res, Tree.branch a left newRight)

def SomePredicate (_ : Tree α n) : Prop := True

theorem whatever : SomePredicate ((popLast heap).snd) := by
  unfold popLast
  sorry

(Lean4 Web Link)

Context

I encountered this while playing around with a heap implemented in the form of a tree. Here is the full source file in its non-compiling state. A similar refactor to the one shown in the two code snippets above allowed to work around the problem there as well.

Since I was unsure if this had already been reported, I mentioned it as a comment on this other bug report, but was advised to file a different report instead.

Steps to Reproduce

1. Try to unfold the popLast function given in the first code snippet above

Expected behavior: Unfold succeeds

Actual behavior: Unfold fails and gives the error message "failed to generate equational theorem for 'popLast'"

Versions

Observed in 4.5.0-rc1 on Lean4 Web, and 4.2.0 on my local Gentoo Linux installation.

Additional Information

Impact

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

[kim-em]

(Could you include the failing code in the code samples above? It is there in the code playground link, but missing here.)

[soulsource]

Sure, I've updated the bug description.