Proof by descent on finite sets

Stream: Is there code for X?

[Xavier Xarles]

In the middle of a proof I would need something similar to a descent argument for finsets, that say if a property of Finsets is true for the empty one, false for the singletons and if it is true for a Finset with more than one element (called non-trivial), then it is true for the subset removing one element, then the property is only true for the empty set. I tried to prove it using induction on Finsets but I am completely stuck.

import Mathlib.Data.Finset.Basic

theorem descent {α : Type*}[DecidableEq α]{p : ∀ s : Finset α, Prop}{s : Finset α}
    (hempty: p ∅) (hsingle:  ∀ (a : α), ¬ p {a} )
    (hind : ∀ (s) (hn :s.Nontrivial), p s → (∃ (a : α), a∈ s ∧  p (Finset.erase s a)) ):
    (p s) ↔ s= ∅ := by sorry

Any suggestion will be very much appreciated. Also suggestions proposing more natural but essentially equivalent results.

[Andrew Yang]

I suspect it will be easier to do induction on fun s ↦ p s → s = ∅ in your application.
EDIT: maybe not

[Yaël Dillies]

Here's a more natural statement:

import Mathlib.Data.Finset.Basic

open Finset

variable {α : Type*} {p : Finset α → Prop} {s : Finset α}

theorem descent (hempty : p ∅) (hsingle : ∀ a, ¬ p {a})
   (hind : ∀ s, s.Nonempty → ∀ a ha, p (cons a s ha) → p s) :
   p s ↔ s = ∅ := by
  refine ⟨fun hs ↦ ?_, by rintro rfl; exact hempty⟩
  contrapose! hs
  refine (nonempty_iff_ne_empty.2 hs).cons_induction hsingle fun a s ha hs ih h ↦ ?_
  exact ih $ hind _ hs _ ha h

[Yaël Dillies]

It's not quite what you want, though

[Andrew Yang]

import Mathlib.Data.Finset.Card

theorem descent' {α : Type*}[DecidableEq α]{p : Finset α → Prop}{s : Finset α}
    (hempty: p ∅) (hsingle: ∀ (a : α), ¬ p {a})
    (hind : ∀ s, s.Nonempty → p s → (∃ (a : α), a ∈ s ∧ p (Finset.erase s a))) :
    (p s) ↔ s= ∅ := by
  refine ⟨?_, fun e ↦ e ▸ hempty⟩
  rw [← Finset.card_eq_zero]
  generalize hn : s.card = n
  induction n generalizing s with
  | zero => exact fun _ ↦ rfl
  | succ n ih =>
    intro H
    have : s.Nonempty
    · rw [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero, hn]
      exact Nat.succ_ne_zero n
    obtain ⟨x, hxs, hs⟩ := hind s this H
    obtain rfl := ih (by rw [Finset.card_erase_of_mem hxs, hn]; rfl) hs
    obtain ⟨y, rfl⟩ := Finset.card_eq_one.mp hn
    exact (hsingle _ H).elim

theorem descent {α : Type*}[DecidableEq α]{p : ∀ s : Finset α, Prop}{s : Finset α}
    (hempty: p ∅) (hsingle:  ∀ (a : α), ¬ p {a} )
    (hind : ∀ (s) (hn :s.Nontrivial), p s → (∃ (a : α), a∈ s ∧  p (Finset.erase s a)) ):
    (p s) ↔ s= ∅ := by
  apply descent' hempty hsingle
  intros s hn hs
  obtain (⟨a, rfl⟩|hs') := hn.exists_eq_singleton_or_nontrivial
  · exact (hsingle _ hs).elim
  · exact hind s hs' hs

[Yaël Dillies]

I have a better solution coming

[Yaël Dillies]

import Mathlib.Data.Finset.Card

namespace Finset
variable {α : Type*} [DecidableEq α] {p : Finset α → Prop} {s : Finset α} {a : α}

lemma Nontrivial.exists_ne (hs : s.Nontrivial) (a : α) : ∃ b ∈ s, b ≠ a := by
  by_contra!; exact not_nontrivial_singleton $ hs.mono fun b hb ↦ mem_singleton.2 $ this b hb

lemma Nontrivial.erase_nonempty (hs : s.Nontrivial) : (s.erase a).Nonempty :=
  (hs.exists_ne a).imp $ by aesop

/-- Suppose that, given objects defined on all nonempty strict subsets of any nontrivial finset `s`,
one knows how to define an object on `s`. Then one can inductively define an object on all finsets,
starting from singletons and iterating. This can be used either to define data, or to prove
properties.

TODO: Actually let `p` be `Sort`-valued. -/
@[elab_as_elim]
protected lemma Nonempty.strong_induction {p : ∀ s, s.Nonempty → Prop}
    (h₀ : ∀ a, p {a} (singleton_nonempty _))
    (h₁ : ∀ ⦃s⦄ (hs : s.Nontrivial), (∀ t ht, t ⊂ s → p t ht) → p s hs.nonempty) :
    ∀ ⦃s : Finset α⦄ (hs), p s hs
  | s, hs => by
    obtain ⟨a, rfl⟩ | hs := hs.exists_eq_singleton_or_nontrivial
    · exact h₀ _
    · refine h₁ hs fun t ht hts ↦ ?_
      have := card_lt_card hts
      exact ht.strong_induction h₀ h₁
termination_by Nonempty.strong_induction _ => Finset.card ‹_›

theorem descent (hempty : p ∅) (hsingle : ∀ a, ¬ p {a})
   (hind : ∀ s, s.Nontrivial → p s → ∃ a ∈ s, p (s.erase a)) :
   p s ↔ s = ∅ := by
  refine ⟨?_, by rintro rfl; exact hempty⟩
  rw [← not_nonempty_iff_eq_empty]
  rintro hps hs
  induction' hs using Nonempty.strong_induction with _ s hs ih
  · exact hsingle _ hps
  obtain ⟨a, ha, hpa⟩ := hind s hs hps
  exact ih _ hs.erase_nonempty (erase_ssubset ha) hpa

end Finset

[Yaël Dillies]

Everything but descent should be in mathlib. Feel free to PR it (or to tell me to do it).

[Xavier Xarles]

I would very pleased if you PR all these...

[Xavier Xarles]

(excluding "descent")

[Ruben Van de Velde]

Yeah, it turns out that "descent" just means "strong induction" if you squint at it right

[Junyan Xu]

It's annoying that all Finset induction principles uses Forall rather than Exists (of an element to insert), so we must relegate to induction on the cardinality. #9123 is a move in the right direction (uses Exists), but it's for Set, not Finset.

[Yaël Dillies]

But that's because the version with Exists is usually false? It's only true over finite types.

[Junyan Xu]

I don't think you assumed finiteness of α when proving theorem descent?

[Yaël Dillies]

How is that related to #9123 ?

[Junyan Xu]

Oh I see what you're saying. You're right the versions with Exists are not always true.
I see that descent is not exactly "contrapositive" of the induction principle . #9123 does assume finiteness.

[Yaël Dillies]

However #9123 seems to be a special case of what we have here (once translated to Set).

[Yaël Dillies]

(you need to apply ᶜ everywhere)

[Yaël Dillies]

Xavier Xarles said:

I would very pleased if you PR all these...

Wish granted: #9308

[Eric Rodriguez]

open Finset

theorem descent {α : Type*}[DecidableEq α]{p : ∀ s : Finset α, Prop}{s : Finset α}
    (hempty: p ∅) (hsingle:  ∀ (a : α), ¬ p {a} )
    (hind : ∀ (s) (hn :s.Nontrivial), p s → (∃ (a : α), a∈ s ∧  p (Finset.erase s a)) ):
  (p s) ↔ s= ∅ := by
  refine ⟨fun hp ↦ ?_, by rintro rfl; exact hempty⟩
  contrapose! hsingle
  induction' s using strongInduction with k ih
  obtain (⟨a, rfl⟩ | h) := (nonempty_of_ne_empty hsingle).exists_eq_singleton_or_nontrivial
  · exact ⟨a, hp⟩
  · obtain ⟨a, hak, hap⟩ := hind _ h hp
    apply ih (k.erase a) (erase_ssubset hak) hap
    sorry

this is an easier approach that is at worst missing the sorry lemma (I have to run, but it's easy i promise!)

[Xavier Xarles]

The proof by @Eric Rodriguez finished:

import Mathlib.Data.Finset.Card

open Finset

theorem descent {α : Type*}[DecidableEq α]{p : ∀ s : Finset α, Prop}{s : Finset α}
    (hempty: p ∅) (hsingle:  ∀ (a : α), ¬ p {a} )
    (hind : ∀ (s) (hn :s.Nontrivial), p s → (∃ (a : α), a∈ s ∧  p (Finset.erase s a)) ):
  (p s) ↔ s= ∅ := by
  refine ⟨fun hp ↦ ?_, by rintro rfl; exact hempty⟩
  contrapose! hsingle
  induction' s using strongInduction with k ih
  obtain (⟨a, rfl⟩ | h) := (nonempty_of_ne_empty hsingle).exists_eq_singleton_or_nontrivial
  · exact ⟨a, hp⟩
  · obtain ⟨a, hak, hap⟩ := hind _ h hp
    apply ih (k.erase a) (erase_ssubset hak) hap
    rw [← nonempty_iff_ne_empty]
    exact (Finset.erase_nonempty hak).2 h

[Yaël Dillies]

Is eric's sorry not my Finset.Nontrivial.erase_nonempty above?

[Xavier Xarles]

(deleted)