"failed to generate equational theorem" with nested matches

Prerequisites

[X] 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%20%3A%20(%CE%B1%20%C3%97%20Tree%20%CE%B1%20o)%20%3A%3D%0A%20%20match%20o%2C%20heap%20with%0A%20%20%7C%20(n%2Bm)%2C%20.branch%20a%20(left%20%3A%20Tree%20%CE%B1%20n)%20(right%20%3A%20Tree%20%CE%B1%20m)%20%20%3D%3E%0A%20%20%20%20if%20r%20%3A%20m%20%3D%200%20then%0A%20%20%20%20%20%20--remove%20left%0A%20%20%20%20%20%20match%20n%2C%20left%20with%0A%20%20%20%20%20%20%7C%200%2C%20_%20%3D%3E%20(a%2C%20(Eq.symm%20%24%20r.subst%20%24%20Nat.zero_add%20m%20%3A%200%3D0%2Bm)%E2%96%B8Tree.leaf)%0A%20%20%20%20%20%20%7C%20(l%2B1)%2C%20left%20%3D%3E%0A%20%20%20%20%20%20%20%20let%20(res%2C%20(newLeft%20%3A%20Tree%20%CE%B1%20l))%20%3A%3D%20popLast%20left%0A%20%20%20%20%20%20%20%20(res%2C%20(Nat.add_rightcomm%20l%20m%201)%E2%96%B8Tree.branch%20a%20newLeft%20right)%0A%20%20%20%20else%0A%20%20%20%20%20%20--remove%20right%0A%20%20%20%20%20%20match%20%20m%2C%20right%20with%0A%20%20%20%20%20%20%7C%20(r%2B1)%2C%20right%20%3D%3E%0A%20%20%20%20%20%20%20%20let%20(res%2C%20(newRight%20%3A%20Tree%20%CE%B1%20r))%20%3A%3D%20popLast%20right%0A%20%20%20%20%20%20%20%20(res%2C%20Tree.branch%20a%20left%20newRight)%0A%0Adef%20SomePredicate%20(%20%3A%20Tree%20%CE%B1%20n)%20%3A%20Prop%20%3A%3D%20True%0A%0Atheorem%20whatever%20%3A%20SomePredicate%20((popLast%20heap).snd)%20%3A%3D%20by%0A%20%20unfold%20popLast%0A%20%20sorry))

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%20%3A%20(%CE%B1%20%C3%97%20Tree%20%CE%B1%20o)%20%3A%3D%0A%20%20match%20o%2C%20heap%20with%0A%20%20%7C%20(n%2Bm)%2C%20.branch%20a%20(left%20%3A%20Tree%20%CE%B1%20n)%20(right%20%3A%20Tree%20%CE%B1%20m)%20%20%3D%3E%0A%20%20%20%20match%20r%20%3A%20m%2C%20right%20with%0A%20%20%20%20%7C%200%2C%20%20%3D%3E%20%0A%20%20%20%20%20%20--remove%20left%0A%20%20%20%20%20%20match%20n%2C%20left%20with%0A%20%20%20%20%20%20%7C%200%2C%20%20%3D%3E%20(a%2C%20Tree.leaf)%0A%20%20%20%20%20%20%7C%20(l%2B1)%2C%20left%20%3D%3E%0A%20%20%20%20%20%20%20%20let%20(res%2C%20(newLeft%20%3A%20Tree%20%CE%B1%20l))%20%3A%3D%20popLast%20left%0A%20%20%20%20%20%20%20%20have%20blah%20%3A%3D%20r.subst%20(motive%20%3A%3D%20%CE%BBmx%20%E2%86%A6%20l%20%2B%20m%20%2B%201%20%3D%20l%20%2B%201%20%2B%20mx)%20(Nat.add_rightcomm%20l%20m%201)%0A%20%20%20%20%20%20%20%20(res%2C%20blah%E2%96%B8Tree.branch%20a%20newLeft%20right)%0A%20%20%20%20%7C%20(o%2B1)%2C%20right%20%3D%3E%0A%20%20%20%20%20%20--remove%20right%0A%20%20%20%20%20%20%20%20let%20(res%2C%20newRight)%20%3A%3D%20popLast%20right%0A%20%20%20%20%20%20%20%20(res%2C%20Tree.branch%20a%20left%20newRight)%0A%0Adef%20SomePredicate%20(%20%3A%20Tree%20%CE%B1%20n)%20%3A%20Prop%20%3A%3D%20True%0A%0Atheorem%20whatever%20%3A%20SomePredicate%20((popLast%20heap).snd)%20%3A%3D%20by%0A%20%20unfold%20popLast%0A%20%20sorry))

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

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 :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

leanprover / lean4