"failed to generate unfold theorem" for recursive nested match

[JamesGallicchio]

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

Unfold lemma generator fails on the following:

def replace (f : Nat → Option Nat) (t : Nat) : Nat :=
  match f t with
  | some u => u
  | none =>
    match t with
    | .zero => .zero
    | .succ t' => replace f t'

It also fails for the following, where f is applied to a different value than the value being recursed on:

def replace2 (f : Nat → Option Nat) (t1 t2 : Nat) : Nat :=
  match f t1 with
  | some u => u
  | none =>
    match t2 with
    | .zero => .zero
    | .succ t' => replace2 f t1 t'

However, it succeeds if the matches are swapped:

def replace' (f : Nat → Option Nat) (t : Nat) : Nat :=
  match t with
  | .zero =>
    match f t with
    | some u => u
    | none => .zero
  | .succ t' =>
    match f t with
    | some u => u
    | none => replace' f t'

Context

Reported on Zulip

Steps to Reproduce

example : replace f 0 = 0 := by
  unfold replace

Expected behavior: Unfolds replace in tactic state

Actual behavior: Emits an error: failed to generate unfold theorem for 'replace'

Versions

4.3.0-rc2
NixOS (unstable branch)

Impact

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

[soulsource]

I am unsure if the issue I'm currently running into is the same or a different bug. In order to prevent duplicates, I thought it might be worth first asking if a separate bug report seems warranted:

Here's my problem: Lean 4 Web

If you think it's a different issue, then please tell me and I'll open another bug report. If it's the same issue, then the above minimal example is way better than mine, as it's much shorter.

[nomeata]

I think it’s a separate issue, it says “failed to generate equational theorem for 'popLast'”, not “failed to generate unfold theorem” (which is a later step), so a separate issue make sense. Thanks for reporting!

[soulsource]

Thanks! I'll try to minify the code example further, and then file a full bug report.