WellFoundedRelation on Finset

Stream: mathlib4

[Johan Commelin]

Currently there is no instance of docs#WellFoundedRelation for Finset. Is that for a reason? I think it would be nice to have, for slick recursive proofs about finsets that don't explicitly mention inducting on the cardinality.

[Yaël Dillies]

Are you sure it's missing? I'm pretty certain it's there, stated using \subset.

[Johan Commelin]

I haven't found it yet

[Yaël Dillies]

@Johan Commelin: docs#Finset.wellFoundedLT

[Johan Commelin]

Merci!

[Johan Commelin]

But that doesn't give an automatic instance of WellFoundedRelation (Finset X). Should we add that?

[Yaël Dillies]

I don't actually know what docs#WellFoundedRelation does. Certainly you can add it but note that A ⊂ B is a stronger relation than A.card < B.card, so I'm not sure < should be registered as WellFoundedRelation.

[Johan Commelin]

WellFoundedRelation is what the termination checker uses for definition using well-founded recursion.

[Kevin Buzzard]

So wouldn't A.card < B.card be better in general?

[Johan Commelin]

Why can't we have both?

[A.]

I had a little play to see if I could understand what was being suggested here but it leaves me with some questions :smile:
Johan Commelin said:

I think it would be nice to have, for slick recursive proofs about finsets that don't explicitly mention inducting on the cardinality.

What would a "slick recursive proof" look like? As it stands we write

import Mathlib.Data.Finset.Card

def strongInduction {α : Type*} {p : Finset α → Sort*} (H : ∀ s, (∀ t ⊂ s, p t) → p s) :
    ∀ s : Finset α, p s
  | s => H s (fun t h =>
    have : t.card < s.card := Finset.card_lt_card h
    strongInduction H t)
  termination_by s => s.card

But if there is a way to get rid of the termination_by by creating an instance of WellFoundedRelation then it eludes me. This works

import Mathlib.Data.Finset.Basic

instance {α : Type*} : WellFoundedRelation (Finset α) := ⟨_, Finset.wellFoundedLT.wf⟩

def strongInduction {α : Type*}  {p : Finset α → Sort*} (H : ∀ s, (∀ t ⊂ s, p t) → p s) :
    ∀ s : Finset α, p s
  | s => H s (fun t _ => strongInduction H t)
  termination_by s => s

as does this

import Mathlib.Data.Finset.Card

instance {α : Type*}  : WellFoundedRelation (Finset α) := measure Finset.card

def strongInduction {α : Type*}  {p : Finset α → Sort*} (H : ∀ s, (∀ t ⊂ s, p t) → p s) :
    ∀ s : Finset α, p s
  | s => H s (fun t h =>
    have : t.card < s.card := Finset.card_lt_card h
    strongInduction H t)
  termination_by s => s

but I'm not sure either is slicker! Unless you include the termination_by line, the termination checker seems always to want to induct on SizeOf.sizeOf even if you remove the SizeOf (Finset α) instance manually.