Descending induction for Finset

Stream: Is there code for X?

[Bolton Bailey]

docs#Finset.induction_on tells you that if you prove a property true for the empty set and you prove that for any element, inserting it into the Finset preserves the property, then the property is true of all Finsets.

But it seems strictly easier to prove that for any subset that doesn't satisfy the property, there is an element we can remove from it so that the property is still not satisfied. This way, we can choose the element we want to remove, rather than having to prove that it works for all elements we could remove. Do we have a theorem like this?

[Aaron Liu]

You can use docs#Finset.strongInduction

[Bolton Bailey]

Is there a version of this that isn't strong?

[Kyle Miller]

Is the motivation for not using strong induction that you want to skip doing cases inside the induction on empty vs nonempty and also skip passing in docs#Finset.erase_ssubset to the induction hypothesis? (Do you want it to be in terms of erase? Or something else?)

[Bolton Bailey]

It just feels like too powerful a tool. Rather than having to specify later that the set I'm talking about is S.erase s, I want to have a lemma where if I am applying it, it automatically knows that the set is of this form.

[Bolton Bailey]

@Aaron Liu thanks for the tip, here is my proof in case anyone is interested:

import Mathlib

open Finset Classical

/--
To prove a proposition for an arbitrary `Finset α`,
it suffices to prove that for any `Finset α` that does not satisfy the proposition,
one can remove an element and obtain a smaller `Finset α`
that also does not satisfy the proposition.
-/
theorem Finset.weakInduction {α : Type u_1} {p : Finset α → Prop}
    (H : (S : Finset α) → (¬ p S → ∃ s ∈ S, ¬ p (S.erase s))) (S : Finset α) : p S := by
  -- Use strong induction on `s` to show that `p s` holds.
  induction S using Finset.strongInduction with
  | H S ih =>
    by_contra hS
    specialize H S hS
    rcases H with ⟨s, hs, hps⟩
    apply hps
    apply ih
    exact erase_ssubset hs

[Ruben Van de Velde]

I'm not sure we have any infinite descent lemmas; they're just contraposed induction if you squint anyway

[Kyle Miller]

Strong induction is more configurable, but it's not any more powerful — having a custom induction principle that puts things into the form of S.erase s for convenience is a stronger argument I think.

[Kyle Miller]

By the way, with induction you can now avoid the indentation:

theorem Finset.weakInduction {α : Type u_1} {p : Finset α → Prop}
    (H : (S : Finset α) → (¬ p S → ∃ s ∈ S, ¬ p (S.erase s))) (S : Finset α) : p S := by
  -- Use strong induction on `s` to show that `p s` holds.
  induction S using Finset.strongInduction with | H S ih
  by_contra hS
  specialize H S hS
  rcases H with ⟨s, hs, hps⟩
  apply hps
  apply ih
  exact erase_ssubset hs

[Kyle Miller]

(for a one-case induction principle, you can also write | _ S ih instead, since the name H doesn't matter)

[Bolton Bailey]

Yes, what I'm saying is that the configurability is a form of power that I would rather avoid for simplicity.

[Bolton Bailey]

Ruben Van de Velde said:

I'm not sure we have any infinite descent lemmas; they're just contraposed induction if you squint anyway

I am a bit confused by this, it was exactly my point in the OP that this is not the case for Finset.

[Kenny Lau]

Bolton Bailey said:

Ruben Van de Velde said:

I'm not sure we have any infinite descent lemmas; they're just contraposed induction if you squint anyway

I am a bit confused by this, it was exactly my point in the OP that this is not the case for Finset.

I am quite confused by what you mean that it "is not induction"; if you look at your proof, the first thing you use is Finset.strongInduction.

[Bolton Bailey]

Sorry, I don't mean to say that the weakInduction above is not induction or doesn't use induction, what I am trying to say is that it not the contraposition of Finset.induction_on. Maybe Ruben's point is that while it isn't the contrapose of that induction lemma, it would be the contrapose of a different induction principle?

[Andrew Yang]

I think their point is that "infinite descent" is a weaker version of the contrapose of docs#Finset.strongInduction

[Bolton Bailey]

Indeed, I see now that you can phrase it as an induction principle, maybe I was getting confused by the necessity of the parentheses in (∀ s ∈ S, p (S.erase s))

import Mathlib

open Finset Classical

/--
To prove a proposition for an arbitrary `Finset α`,
it suffices to prove that for any `Finset α` that does not satisfy the proposition,
one can remove an element and obtain a smaller `Finset α`
that also does not satisfy the proposition.
-/
theorem Finset.weakInduction {α : Type u_1} {p : Finset α → Prop}
    (H : (S : Finset α) → ((∀ s ∈ S, p (S.erase s)) -> p S)) (S : Finset α) : p S := by
  -- Use strong induction on `s` to show that `p s` holds.
  induction S using Finset.strongInduction with
  | H S ih =>
    specialize H S
    apply H
    intro s hs
    apply ih
    exact erase_ssubset hs

[Eric Wieser]

Or golfed,

theorem Finset.weakInduction {α : Type u_1} {p : Finset α → Prop}
    (H : (S : Finset α) → ((∀ s ∈ S, p (S.erase s)) -> p S)) (S : Finset α) : p S :=
  S.strongInduction fun S ih => H S fun _ hs => ih _ (erase_ssubset hs)