feat(library/theories/combinatorics/choose): show the number of subsets of s of size k is choose (card s) k

library/theories/combinatorics/choose.lean

@@ -5,7 +5,7 @@ Author: Jeremy Avigad
 
 Binomial coefficients, "n choose k".
 -/
-import data.nat.div data.nat.fact
+import data.nat.div data.nat.fact data.finset
 open decidable
 
 namespace nat
@@ -23,7 +23,8 @@ nat.cases_on n rfl (take m, rfl)
 
 theorem choose_zero_succ (k : ℕ) : choose 0 (succ k) = 0 := rfl
 
-theorem choose_succ_succ (n k : ℕ) : choose (succ n) (succ k) = choose n (succ k) + choose n k := rfl
+theorem choose_succ_succ (n k : ℕ) : choose (succ n) (succ k) = choose n (succ k) + choose n k :=
+rfl
 
 theorem choose_eq_zero_of_lt {n : ℕ} : ∀{k : ℕ}, n < k → choose n k = 0 :=
 nat.induction_on n
@@ -74,7 +75,8 @@ begin
 end
 
 -- A key identity. The proof is subtle.
-theorem succ_mul_choose_eq (n : ℕ) : ∀ k, succ n * (choose n k) = choose (succ n) (succ k) * succ k :=
+theorem succ_mul_choose_eq (n : ℕ) :
+  ∀ k, succ n * (choose n k) = choose (succ n) (succ k) * succ k :=
 begin
   induction n with [n, ih],
     {intro k,
@@ -115,4 +117,107 @@ eq.symm (div_eq_of_eq_mul_left (mul_pos !fact_pos !fact_pos)
 theorem fact_mul_fact_dvd_fact {n k : ℕ} (H : k ≤ n) : fact k * fact (n - k) ∣ fact n :=
 by rewrite [-choose_mul_fact_mul_fact H, mul.assoc]; apply dvd_mul_left
 
+open finset
+
+/- the number of subsets of s of size k is n choose k -/
+
+section card_subsets
+variables {A : Type} [deceqA : decidable_eq A]
+include deceqA
+
+private theorem aux₀ (s : finset A) : {t ∈ powerset s | card t = 0} = '{∅} :=
+ext (take t, iff.intro
+  (assume H,
+    assert t = ∅, from eq_empty_of_card_eq_zero (of_mem_filter H),
+    show t ∈ '{ ∅ }, by rewrite [this, mem_singleton_eq'])
+  (assume H,
+    assert t = ∅, by rewrite mem_singleton_eq' at H; assumption,
+    by substvars; exact mem_filter_of_mem !empty_mem_powerset rfl))
+
+private theorem aux₁ (k : ℕ) : {t ∈ powerset (∅ : finset A) | card t = succ k} = ∅ :=
+eq_empty_of_forall_not_mem (take t, assume H,
+  assert t ∈ powerset ∅, from mem_of_mem_filter H,
+  assert t = ∅, by rewrite [powerset_empty at this, mem_singleton_eq' at this]; assumption,
+  have card (∅ : finset A) = succ k, by rewrite -this; apply of_mem_filter H,
+  nat.no_confusion this)
+
+private theorem aux₂ {a : A} {s t : finset A} (anins : a ∉ s) (tpows : t ∈ powerset s) : a ∉ t :=
+suppose a ∈ t,
+have a ∈ s, from mem_of_subset_of_mem (subset_of_mem_powerset tpows) this,
+anins this
+
+private theorem aux₃ {a : A} {s t : finset A} (anins : a ∉ s) (k : ℕ) :
+  t ∈ (insert a) '[powerset s] ∧ card t = succ k ↔
+    t ∈ (insert a) '[{t' ∈ powerset s | card t' = k}] :=
+iff.intro
+  (assume H,
+    obtain H' cardt, from H,
+    obtain t' [(t'pows : t' ∈ powerset s) (teq : insert a t' = t)], from exists_of_mem_image H',
+    assert aint : a ∈ t, by rewrite -teq; apply mem_insert,
+    assert anint' : a ∉ t', from
+      (assume aint',
+        have a ∈ s, from mem_of_subset_of_mem (subset_of_mem_powerset t'pows) aint',
+        anins this),
+    assert t' = erase a t, by rewrite [-teq, erase_insert (aux₂ anins t'pows)],
+    have card t' = k, by rewrite [this, card_erase_of_mem aint, cardt],
+    mem_image (mem_filter_of_mem t'pows this) teq)
+  (assume H,
+    obtain t' [Ht' (teq : insert a t' = t)], from exists_of_mem_image H,
+    assert t'pows : t' ∈ powerset s, from mem_of_mem_filter Ht',
+    assert cardt' : card t' = k, from of_mem_filter Ht',
+    and.intro
+      (show t ∈ (insert a) '[powerset s], from mem_image t'pows teq)
+      (show card t = succ k,
+        by rewrite [-teq, card_insert_of_not_mem (aux₂ anins t'pows), cardt']))
+
+private theorem aux₄ {a : A} {s : finset A} (anins : a ∉ s) (k : ℕ) :
+  {t ∈ powerset (insert a s)| card t = succ k} =
+    {t ∈ powerset s | card t = succ k} ∪ (insert a) '[{t ∈ powerset s | card t = k}] :=
+begin
+  apply ext, intro t,
+  rewrite [powerset_insert anins, mem_union_iff, *mem_filter_iff, mem_union_iff, and.right_distrib,
+           aux₃ anins]
+end
+
+private theorem aux₅ {a : A} {s : finset A} (anins : a ∉ s) (k : ℕ) :
+  {t ∈ powerset s | card t = succ k} ∩ (insert a) '[{t ∈ powerset s | card t = k}] = ∅ :=
+inter_eq_empty
+  (take t, assume Ht₁ Ht₂,
+    have tpows : t ∈ powerset s, from mem_of_mem_filter Ht₁,
+    have anint : a ∉ t, from aux₂ anins tpows,
+    obtain t' [Ht' (teq : insert a t' = t)], from exists_of_mem_image Ht₂,
+    have aint : a ∈ t, by rewrite -teq; apply mem_insert,
+    show false, from anint aint)
+
+private theorem aux₆ {a : A} {s : finset A} (anins : a ∉ s) (k : ℕ) :
+  card ((insert a) '[{t ∈ powerset s | card t = k}]) = card {t ∈ powerset s | card t = k} :=
+have set.inj_on (insert a) (ts {t ∈ powerset s| card t = k}), from
+  take t₁ t₂, assume Ht₁ Ht₂,
+  assume Heq : insert a t₁ = insert a t₂,
+  have t₁ ∈ powerset s, from mem_of_mem_filter Ht₁,
+  assert anint₁ : a ∉ t₁, from aux₂ anins this,
+  have t₂ ∈ powerset s, from mem_of_mem_filter Ht₂,
+  assert anint₂ : a ∉ t₂, from aux₂ anins this,
+  calc
+    t₁    = erase a (insert a t₁) : by rewrite (erase_insert anint₁)
+      ... = erase a (insert a t₂) : Heq
+      ... = t₂                    : by rewrite (erase_insert anint₂),
+card_image_eq_of_inj_on this
+
+theorem card_subsets (s : finset A) : ∀k, card {t ∈ powerset s | card t = k} = choose (card s) k :=
+begin
+  induction s with a s anins ih,
+    {intro k,
+      cases k with k,
+        {rewrite aux₀},
+      rewrite aux₁},
+  intro k,
+  cases k with k,
+    {rewrite [aux₀, choose_zero_right]},
+  rewrite [*(card_insert_of_not_mem anins), aux₄ anins, card_union_of_disjoint (aux₅ anins k),
+           aux₆ anins k, *ih]
+end
+
+end card_subsets
+
 end nat