induction on finite set

Stream: Is there code for X?

[Bernd Losert]

Is there a version set.finite.induction_on with the added assumption in the inductive hypothesis that it is a subset of the original finite set. I basically want finset.induction_on' but without the decidable_eq part.

[Yaël Dillies]

You can use classical before.

[Patrick Johnson]

finset.induction_on' can easily be converted to set.finite.induction_on'

import tactic

lemma set.finite.induction_on' {α : Type*} {p : Π (s : set α), s.finite → Prop}
  {S : set α} (h : S.finite) (h₁ : ∀ h, p ∅ h)
  (h₂ : ∀ {a s h₁ h₂}, a ∈ S → s ⊆ S → a ∉ s → p s h₁ → p (insert a s) h₂) : p S h :=
begin
  classical,
  have h₃ := @finset.induction_on' α (λ s, p (s : set α) (finset.finite_to_set _))
    (by apply_instance) h.to_finset (h₁ set.finite_empty),
  specialize h₃ _,
  { rintro x t h₃ h₄ h₅ h₆, push_cast,
    apply @h₂ x t (finset.finite_to_set _) (set.finite_of_fintype _)
    ((set.finite.mem_to_finset h).mp h₃) ((set.subset_to_finset_iff h).mp h₄)
    (mt finset.mem_coe.mp h₅) h₆ },
  simp only [set.finite.coe_to_finset] at h₃,
  assumption,
end

[Bernd Losert]

Thanks, although that doesn't look easy to me.

[Reid Barton]

It's easier to start from set.finite.induction_on

lemma set.finite.induction_on' {α : Type*} {p : Π (s : set α), Prop}
  {S : set α} (h : S.finite) (h₁ : p ∅)
  (h₂ : ∀ {a s}, a ∈ S → s ⊆ S → a ∉ s → p s → p (insert a s)) : p S :=
begin
  refine @set.finite.induction_on α (λ s, s ⊆ S → p s) S h (λ _, h₁) _ (set.subset.refl S),
  intros a s h₃ h₄ h₅ h₆,
  rw set.insert_subset at h₆, cases h₆ with h₆ h₇,
  exact h₂ h₆ h₇ h₃ (h₅ h₇)
end

[Patrick Johnson]

Right, I should have used {p : Π (s : set α), Prop} instead. The proof is now simpler:

import tactic

lemma set.finite.induction_on' {α : Type*} {p : Π (s : set α), Prop}
  {S : set α} (h : S.finite) (h₁ : p ∅)
  (h₂ : ∀ {a s}, a ∈ S → s ⊆ S → a ∉ s → p s → p (insert a s)) : p S :=
begin
  convert @finset.induction_on' α (λ s, p s) (classical.dec_eq α) h.to_finset h₁ _, { simp },
  push_cast, rintro x t h₃ h₄ h₅ h₆, refine @h₂ x t _ _ _ h₆;
  simp [*, set.finite.mem_to_finset h, set.subset_to_finset_iff h] at *,
end

[Bernd Losert]

Do you mind if I make a pull request to commit that to mathlib?

[Patrick Johnson]

I don't mind and I guess Reid doesn't mind either (whichever proof you decide to choose).

[Junyan Xu]

Π (s : set α), Prop is usually written set α → Prop.

[Bernd Losert]

PR: https://github.com/leanprover-community/mathlib/pull/15444