fix: WF.Fix, WF.GuessLex: Use expression cache

[nomeata]

else the termination tactic is run on duplicated terms, e.g. in

 def dup (a : Nat) (b : Nat := a) := a + b

 def rec : Nat → Nat
  | 0 => 1
  | n+1 => dup (dup (dup (rec n)))

This pattern apperas in the wild in Array.foldl and friends.

[nomeata]

Diff best viewed with Github’s “Hide whitespace” setting. I’ll be curious if this will show in the perf benchmarks.

[leanprover-community-mathlib4-bot]

• 💥 Mathlib branch lean-pr-testing-2982 build failed against this PR. (2023-11-28 18:50:28) View Log

[nomeata]

This interestingly breaks mathlib:

Error: ./././Mathlib/Logic/Denumerable.lean:279:8: error: (kernel) declaration has free variables 'Nat.Subtype.ofNat_surjective_aux'

Will have to debug and improve our test suite.

[nomeata]

Very pecuilar. Here is a reproducer:

def foo : (n : Nat) → ∃ m, m > n
 | 0 => ⟨1, Nat.zero_lt_one⟩
 | n+1 => by
  cases foo n
  · case _ m hm => exact ⟨m+1, Nat.succ_lt_succ hm⟩
decreasing_by
  -- With the case tactic, we get the recursive
  -- call as an assumption
  trace_state

On master, this runs the tactic four times, with these states:

n: Nat
x✝: ∀ (y : Nat), (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y (Nat.succ n) → ∃ m, m > y
t✝: ∃ m, m > n
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
n: Nat
x✝: ∀ (y : Nat), (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y (Nat.succ n) → ∃ m, m > y
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
n: Nat
x✝: ∀ (y : Nat), (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y (Nat.succ n) → ∃ m, m > y
w✝: Nat
h✝: w✝ > n
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)
n: Nat
x✝: ∀ (y : Nat), (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y (Nat.succ n) → ∃ m, m > y
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 n (Nat.succ n)

Why is that? Well, there are three calls to foo here:

[Elab.definition.wf] replaceRecApps:
      match n with
      | 0 => Exists.intro 1 Nat.zero_lt_one
      | Nat.succ n =>
        Exists.casesOn (motive := fun t => foo n = t → ∃ m, m > n + 1) (foo n)
          (fun w h h_1 => Exists.intro (w + 1) (Nat.succ_lt_succ h)) (Eq.refl (foo n))

(Not sure where the forth is)

Note though that they have different contexts. In particular, the first one has an assumption ∃ m, m > n. This is likely the call in the motive := argument.

Now let’s try to use that:

decreasing_by
  -- With the case tactic, we get the recursive
  -- call as an assumption
  solve
  | have this_is_in_the_context : ∃ m, m > n := by assumption
    trace_state
    cases this_is_in_the_context
    exact Nat.lt_succ_self _
  | exact Nat.lt_succ_self _

On master, we now use that extra assumption in the one call, but that’s fine, we don’t use it in the other calls.

On this branch (at the time of writing), we cache the result, ignoring the context, and 💥 .

Now it is clear that ignoring the context when caching is the basic mistake here, and could maybe be fixed (resetting the cache when going under binders for example).

But I wonder how useful it is to try to use caching here in the first place,if the duplicated terms happen to appear in so many different contexts. Maybe there is not much of a point, and instead if we have a problem (not sure we even do in practice) we should avoid too much term duplicate. Hmm.

A work-around for a user running into this is to let-bind before using cases:

def foo : (n : Nat) → ∃ m, m > n
 | 0 => ⟨1, Nat.zero_lt_one⟩
 | n+1 => by
  let r := foo n
  cases r
  · case _ m hm => exact ⟨m+1, Nat.succ_lt_succ hm⟩

[nomeata]

Better to use #3004