feat(data/finset/pi_induction): induction on Π i, finset (α i) (#8794)

Author: urkud

src/data/finset/basic.lean

@@ -356,6 +356,9 @@ lemma eq_empty_iff_forall_not_mem {s : finset α} : s = ∅ ↔ ∀ x, x ∉ s :
 
 theorem subset_empty {s : finset α} : s ⊆ ∅ ↔ s = ∅ := subset_zero.trans val_eq_zero
 
+@[simp] lemma not_ssubset_empty (s : finset α) : ¬s ⊂ ∅ :=
+λ h, let ⟨x, he, hs⟩ := exists_of_ssubset h in he
+
 theorem nonempty_of_ne_empty {s : finset α} (h : s ≠ ∅) : s.nonempty :=
 exists_mem_of_ne_zero (mt val_eq_zero.1 h)
 
@@ -1628,11 +1631,9 @@ def not_mem_range_equiv (k : ℕ) : {n // n ∉ range k} ≃ ℕ :=
 namespace option
 
 /-- Construct an empty or singleton finset from an `option` -/
-def to_finset (o : option α) : finset α :=
-match o with
-| none   := ∅
-| some a := {a}
-end
+def to_finset : option α → finset α
+| none     := ∅
+| (some a) := {a}
 
 @[simp] theorem to_finset_none : none.to_finset = (∅ : finset α) := rfl
 
@@ -2705,7 +2706,13 @@ protected def sigma (s : finset α) (t : Πa, finset (σ a)) : finset (Σa, σ a
 
 @[simp] theorem mem_sigma {p : sigma σ} : p ∈ s.sigma t ↔ p.1 ∈ s ∧ p.2 ∈ t (p.1) := mem_sigma
 
-theorem sigma_mono {s₁ s₂ : finset α} {t₁ t₂ : Πa, finset (σ a)}
+@[simp] theorem sigma_nonempty : (s.sigma t).nonempty ↔ ∃ x ∈ s, (t x).nonempty :=
+by simp [finset.nonempty]
+
+@[simp] theorem sigma_eq_empty : s.sigma t = ∅ ↔ ∀ x ∈ s, t x = ∅ :=
+by simp only [← not_nonempty_iff_eq_empty, sigma_nonempty, not_exists]
+
+@[mono] theorem sigma_mono {s₁ s₂ : finset α} {t₁ t₂ : Πa, finset (σ a)}
   (H1 : s₁ ⊆ s₂) (H2 : ∀a, t₁ a ⊆ t₂ a) : s₁.sigma t₁ ⊆ s₂.sigma t₂ :=
 λ ⟨x, sx⟩ H, let ⟨H3, H4⟩ := mem_sigma.1 H in mem_sigma.2 ⟨H1 H3, H2 x H4⟩
 

src/data/finset/pi_induction.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import data.fintype.basic
+
+/-!
+# Induction principles for `Π i, finset (α i)`
+
+In this file we prove a few induction principles for functions `Π i : ι, finset (α i)` defined on a
+finite type.
+
+* `finset.induction_on_pi` is a generic lemma that requires only `[fintype ι]`, `[decidable_eq ι]`,
+  and `[Π i, decidable_eq (α i)]`; this version can be seen as a direct generalization of
+  `finset.induction_on`.
+
+* `finset.induction_on_pi_max` and `finset.induction_on_pi_min`: generalizations of
+  `finset.induction_on_max`; these versions require `Π i, linear_order (α i)` but assume
+  `∀ y ∈ g i, y < x` and `∀ y ∈ g i, x < y` respectively in the induction step.
+
+## Tags
+finite set, finite type, induction, function
+-/
+
+open function
+
+variables {ι : Type*} {α : ι → Type*} [fintype ι] [decidable_eq ι] [Π i, decidable_eq (α i)]
+
+namespace finset
+
+/-- General theorem for `finset.induction_on_pi`-style induction principles. -/
+lemma induction_on_pi_of_choice (r : Π i, α i → finset (α i) → Prop)
+  (H_ex : ∀ i (s : finset (α i)) (hs : s.nonempty), ∃ x ∈ s, r i x (s.erase x))
+  {p : (Π i, finset (α i)) → Prop} (f : Π i, finset (α i)) (h0 : p (λ _, ∅))
+  (step : ∀ (g : Π i, finset (α i)) (i : ι) (x : α i),
+    r i x (g i) → p g → p (update g i (insert x (g i)))) :
+  p f :=
+begin
+  induction hs : univ.sigma f using finset.strong_induction_on with s ihs generalizing f, subst s,
+  cases eq_empty_or_nonempty (univ.sigma f) with he hne,
+  { convert h0, simpa [funext_iff] using he },
+  { rcases sigma_nonempty.1 hne with ⟨i, -, hi⟩,
+    rcases H_ex i (f i) hi with ⟨x, x_mem, hr⟩,
+    set g := update f i ((f i).erase x) with hg, clear_value g,
+    have hx' : x ∉ g i, by { rw [hg, update_same], apply not_mem_erase },
+    obtain rfl : f = update g i (insert x (g i)),
+      by rw [hg, update_idem, update_same, insert_erase x_mem, update_eq_self],
+    clear hg, rw [update_same, erase_insert hx'] at hr,
+    refine step _ _ _ hr (ihs (univ.sigma g) _ _ rfl),
+    rw ssubset_iff_of_subset (sigma_mono (subset.refl _) _),
+    exacts [⟨⟨i, x⟩, mem_sigma.2 ⟨mem_univ _, by simp⟩, by simp [hx']⟩,
+      (@le_update_iff _ _ _ _ g g i _).2 ⟨subset_insert _ _, λ _ _, le_rfl⟩] }
+end
+
+/-- Given a predicate on functions `Π i, finset (α i)` defined on a finite type, it is true on all
+maps provided that it is true on `λ _, ∅` and for any function `g : Π i, finset (α i)`, an index
+`i : ι`, and `x ∉ g i`, `p g` implies `p (update g i (insert x (g i)))`.
+
+See also `finset.induction_on_pi_max` and `finset.induction_on_pi_min` for specialized versions
+that require `Π i, linear_order (α i)`.  -/
+lemma induction_on_pi {p : (Π i, finset (α i)) → Prop} (f : Π i, finset (α i)) (h0 : p (λ _, ∅))
+  (step : ∀ (g : Π i, finset (α i)) (i : ι) (x : α i) (hx : x ∉ g i),
+    p g → p (update g i (insert x (g i)))) :
+  p f :=
+induction_on_pi_of_choice (λ i x s, x ∉ s) (λ i s ⟨x, hx⟩, ⟨x, hx, not_mem_erase x s⟩) f h0 step
+
+/-- Given a predicate on functions `Π i, finset (α i)` defined on a finite type, it is true on all
+maps provided that it is true on `λ _, ∅` and for any function `g : Π i, finset (α i)`, an index
+`i : ι`, and an element`x : α i` that is strictly greater than all elements of `g i`, `p g` implies
+`p (update g i (insert x (g i)))`.
+
+This lemma requires `linear_order` instances on all `α i`. See also `finset.induction_on_pi` for a
+version that `x ∉ g i` instead of ` does not need `Π i, linear_order (α i)`. -/
+lemma induction_on_pi_max [Π i, linear_order (α i)] {p : (Π i, finset (α i)) → Prop}
+  (f : Π i, finset (α i)) (h0 : p (λ _, ∅))
+  (step : ∀ (g : Π i, finset (α i)) (i : ι) (x : α i),
+    (∀ y ∈ g i, y < x) → p g → p (update g i (insert x (g i)))) :
+  p f :=
+induction_on_pi_of_choice (λ i x s, ∀ y ∈ s, y < x)
+  (λ i s hs, ⟨s.max' hs, s.max'_mem hs, λ y, s.lt_max'_of_mem_erase_max' _⟩) f h0 step
+
+/-- Given a predicate on functions `Π i, finset (α i)` defined on a finite type, it is true on all
+maps provided that it is true on `λ _, ∅` and for any function `g : Π i, finset (α i)`, an index
+`i : ι`, and an element`x : α i` that is strictly less than all elements of `g i`, `p g` implies
+`p (update g i (insert x (g i)))`.
+
+This lemma requires `linear_order` instances on all `α i`. See also `finset.induction_on_pi` for a
+version that `x ∉ g i` instead of ` does not need `Π i, linear_order (α i)`. -/
+lemma induction_on_pi_min [Π i, linear_order (α i)] {p : (Π i, finset (α i)) → Prop}
+  (f : Π i, finset (α i)) (h0 : p (λ _, ∅))
+  (step : ∀ (g : Π i, finset (α i)) (i : ι) (x : α i),
+    (∀ y ∈ g i, x < y) → p g → p (update g i (insert x (g i)))) :
+  p f :=
+@induction_on_pi_max ι (λ i, order_dual (α i)) _ _ _ _ _ _ h0 step
+
+end finset