"failed to generate unfold theorem" for recursive nested match

JamesGallicchio commented 1 year ago

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

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

soulsource commented 10 months ago

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%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%20p%20%3A%200%20%3D%20(n%2Bm)%20then%0A%20%20%20%20%20%20(a%2C%20p%E2%96%B8Tree.leaf)%0A%20%20%20%20else%0A%20%20%20%20%20%20let%20rightIsFull%20%3A%20Bool%20%3A%3D%20(m%2B1).nextPowerOfTwo%20%3D%20m%2B1%0A%20%20%20%20%20%20have%20m_gt_0_or_rightIsFull%20%3A%20m%20%3E%200%20%E2%88%A8%20rightIsFull%20%3A%3D%20by%20cases%20m%20%3C%3B%3E%20simp_arith%0A%20%20%20%20%20%20if%20r%20%3A%20m%20%3C%20n%20%E2%88%A7%20rightIsFull%20then%0A%20%20%20%20%20%20%20%20--remove%20left%0A%20%20%20%20%20%20%20%20match%20n%2C%20left%20with%0A%20%20%20%20%20%20%20%20%7C%20(l%2B1)%2C%20left%20%3D%3E%0A%20%20%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%20%20have%20q%20%3A%20l%20%2B%20m%20%2B%201%20%3D%20l%20%2B%201%20%2Bm%20%3A%3D%20by%20simp_arith%0A%20%20%20%20%20%20%20%20%20%20(res%2C%20q%E2%96%B8Tree.branch%20a%20newLeft%20right)%0A%20%20%20%20%20%20else%0A%20%20%20%20%20%20%20%20--remove%20right%0A%20%20%20%20%20%20%20%20have%20%3A%20m%20%3E%200%20%3A%3D%20by%0A%20%20%20%20%20%20%20%20%20%20cases%20m_gt_0_or_rightIsFull%0A%20%20%20%20%20%20%20%20%20%20case%20inl%20%3D%3E%20assumption%0A%20%20%20%20%20%20%20%20%20%20case%20inr%20h%20%3D%3E%20%0A%20%20%20%20%20%20%20%20%20%20%20%20simp_arith%20%5Bh%5D%20at%20r%0A%20%20%20%20%20%20%20%20%20%20%20%20cases%20n%0A%20%20%20%20%20%20%20%20%20%20%20%20case%20zero%20%3D%3E%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20simp%5BNat.zero_lt_of_ne_zero%5D%20at%20p%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20exact%20Nat.zero_lt_of_ne_zero%20(Ne.symm%20p)%0A%20%20%20%20%20%20%20%20%20%20%20%20case%20succ%20q%20%3D%3E%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20cases%20m%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20have%20%3A%3D%20Nat.not_succ_le_zero%20q%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20contradiction%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20simp_arith%0A%20%20%20%20%20%20%20%20match%20%20m%2C%20right%20with%0A%20%20%20%20%20%20%20%20%7C%20(l%2B1)%2C%20right%20%3D%3E%0A%20%20%20%20%20%20%20%20%20%20let%20(res%2C%20(newRight%20%3A%20Tree%20%CE%B1%20l))%20%3A%3D%20popLast%20right%0A%20%20%20%20%20%20%20%20%20%20(res%2C%20Tree.branch%20a%20left%20newRight)%0A%0Adef%20HeapPredicate%20(heap%20%3A%20Tree%20%CE%B1%20n)%20%3A%20Prop%20%3A%3D%20True%20--%20obviously%20not%20true%2C%20but%20minimal%20example...%0A%0Atheorem%20whatever%20%7Bheap%20%3A%20Tree%20%CE%B1%20(o%2B1)%7D%20%7Ble%20%3A%20%CE%B1%20%E2%86%92%20%CE%B1%20%E2%86%92%20Bool%7D%20(h%E2%82%81%20%3A%20HeapPredicate%20heap)%20%3A%20HeapPredicate%20((popLast%20heap).snd)%20%3A%3D%0A%20%20match%20o%2C%20heap%20with%0A%20%20%7C%20(n%2Bm)%2C%20.branch%20v%20l%20r%20%3D%3E%0A%20%20%20%20if%20h%E2%82%84%20%3A%200%20%3D%20(n%2Bm)%20then%20by%0A%20%20%20%20%20%20unfold%20popLast%0A%20%20%20%20else%0A%20%20%20%20%20%20sorry)

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 commented 10 months ago

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 commented 10 months ago

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

leanprover / lean4