WF Induction bug

Stream: lean4

[Peter Nelson]

This isn't quite as minimized as it could be (the problem has nothing to do with Finset), but the following looks like a bug.

The only difference between foo1 and foo2 is that foo1 uses an indented tactic line to prove h_lt, and foo2 uses :=. The former fails with a generic WF induction error, and the latter works.

import Mathlib.Data.Finset.Card

def P : Finset ℕ → Prop := sorry

theorem hP {s : Finset ℕ} (hs : ¬ P s) : ∃ t, t ⊂ s ∧ ¬ P t  := sorry

theorem foo1 (s : Finset ℕ) : P s := by
  by_contra h
  obtain ⟨t, ht, hPt⟩ := hP h
  have h_lt : t.card < s.card
  · exact Finset.card_lt_card ht
  exact hPt <| foo1 t
termination_by _ => s.card
-- failed to prove termination, possible solutions:
--   - Use `have`-expressions to prove the remaining goals
--   - Use `termination_by` to specify a different well-founded relation
--   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal

theorem foo2 (s : Finset ℕ) : P s := by
  by_contra h
  obtain ⟨t, ht, hPt⟩ := hP h
  have h_lt : t.card < s.card := Finset.card_lt_card ht
  exact hPt <| foo2 t
termination_by _ => s.card
-- works fine

[Joachim Breitner]

With decreasing_by simp_wf we can see the goals in both cases. This is the goal that fails

s: Finset ℕ
a✝: ∀ (y : Finset ℕ), (invImage (fun a => Finset.card a) instWellFoundedRelation).1 y s → P y
h: ¬P s
t: Finset ℕ
h✝: t ⊂ s ∧ ¬P t
ht: t ⊂ s
hPt: ¬P t
⊢ Finset.card t < Finset.card s

and this is the corresponding goal that succeeds

s: Finset ℕ
a✝: ∀ (y : Finset ℕ), (invImage (fun a => Finset.card a) instWellFoundedRelation).1 y s → P y
h: ¬P s
t: Finset ℕ
h✝: t ⊂ s ∧ ¬P t
ht: t ⊂ s
hPt: ¬P t
h_lt: Finset.card t < Finset.card s
⊢ Finset.card t < Finset.card s

So it loses the l_lt premise somehow.

[Joachim Breitner]

With set_option trace.Elab.definition.wf true we see more:

 foo1 :=
    WellFounded.fix (invImage (fun a => Finset.card a) instWellFoundedRelation).2 fun s a =>
      Classical.byContradiction fun h =>
        Exists.casesOn (hP h) fun t h =>
          And.casesOn h fun ht hPt =>
            hPt (a t (Eq.mpr (id Std.Classes.Order._auxLemma.4) (sorryAx (Finset.card t < Finset.card s) true)))

vs.

foo2 :=
    WellFounded.fix (invImage (fun a => Finset.card a) instWellFoundedRelation).2 fun s a =>
      Classical.byContradiction fun h =>
        Exists.casesOn (hP h) fun t h =>
          And.casesOn h fun ht hPt =>
            let_fun h_lt := Finset.card_lt_card ht;
            hPt (a t (Eq.mpr (id Std.Classes.Order._auxLemma.4) (sorryAx (Finset.card t < Finset.card s) true)))

so the let_fun is dropped somewhere along the way, and it seems to be happening before it reaches the code that deals with recursion.

Maybe someone who knows more about the implementation of have can spot the issue. In any case, feel free to open an issue. Maybe you can minimize it further; it can also be very helpful to know when the issue disappears.

[Mario Carneiro]

this is a known issue, you can work around it by putting the have in the same term as the exact

[Joachim Breitner]

Is there a lean issue for it?