Well-founded induction with ENat

Stream: general

[Peter Nelson]

I'm having trouble getting well-founded induction (with decreasing_by) working with ENat. Here is a MWE

import Mathlib.Data.ENat.Basic

-- this easy lemma is provable by well-founded induction
theorem wf1 (P : ℕ∞ → Prop) (h0 : P 0) (h : ∀ k, 0 < k → ∃ t, t < k ∧ (P t → P k)) (n : ℕ∞) :
    P n := by
  refine' WellFounded.induction (r := (· < ·)) IsWellFounded.wf _ (fun x h' ↦ _)
  obtain ((rfl : x = 0) | hpos) := eq_zero_or_pos
  · exact h0
  obtain ⟨t, ht, hPt⟩ := h x hpos
  exact hPt (h' _ ht)

-- Same lemma statement; this time, we try to prove it by invoking itself on a smaller value.
theorem wf2 (P : ℕ∞ → Prop) (h0 : P 0) (h : ∀ k, 0 < k → ∃ t, t < k ∧ (P t → P k)) (n : ℕ∞) :
    P n := by
  obtain ((rfl : n = 0) | hn) := eq_zero_or_pos
  · exact h0
  obtain ⟨t, ht, hPt⟩ := h n hn
  -- (`ht : t < n`) is in context, so we should be able to invoke wf2 on `t`
  exact hPt (wf2 P h0 h t)
  -- doesn't work - so explicitly give `termination_by` and `decreasing_by`
termination_by _ => n
decreasing_by
  simp_wf
  -- goal should simplify to `t < n`, but instead simplifies to `False` ??

It seems that the well-founded relation is unfolding to something trivial rather than < as it should; but I don't understand why.

[Arthur Adjedj]

The issue is that the well-founded relation that's inferred by termination_by is the wrong one, autogenerated using SizeOf. Using the correct measure solves the issue:

import Mathlib.Data.ENat.Basic
import Mathlib.Data.Nat.Cast.WithTop
theorem wf2 (P : ℕ∞ → Prop) (h0 : P 0) (h : ∀ k, 0 < k → ∃ t, t < k ∧ (P t → P k)) (n : ℕ∞) :
    P n := by
  obtain ((rfl : n = 0) | hn) := eq_zero_or_pos
  · exact h0
  have ⟨t, ht, hPt⟩ := h n hn
  exact hPt (wf2 P h0 h t)
termination_by' instWellFoundedRelationWithTopNat
decreasing_by {
  exact ht
}

[Peter Nelson]

Thank you! I didn't know about termination_by'; are there docs for the primed version anywhere?

[Matthew Ballard]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Help.20with.20termination_by/near/368743246 (and continuing discussion) is relevant.

[Gabriel Ebner]

You should add a WellFoundedRelation ENat instance, then this will work as expected:

import Mathlib.Data.ENat.Basic
import Mathlib.Data.Nat.Cast.WithTop

instance : WellFoundedRelation ENat where
  rel := (· < ·)
  wf := IsWellFounded.wf

theorem wf2 (P : ℕ∞ → Prop) (h0 : P 0) (h : ∀ k, 0 < k → ∃ t, t < k ∧ (P t → P k)) (n : ℕ∞) :
    P n := by
  obtain ((rfl : n = 0) | hn) := eq_zero_or_pos
  · exact h0
  have ⟨t, _ht, hPt⟩ := h n hn
  exact hPt (wf2 P h0 h t)
termination_by _ => n