feat(library/theories/combinatorics/choose): begin theory of binomial coefficients

library/data/nat/fact.lean

@@ -21,19 +21,11 @@ rfl
 lemma fact_succ (n) : fact (succ n) = succ n * fact n :=
 rfl
 
-lemma fact_ne_zero : ∀ n, fact n ≠ 0
-| 0        := by contradiction
-| (succ n) :=
-  begin
-    intro h,
-    rewrite [fact_succ at h],
-    cases (eq_zero_or_eq_zero_of_mul_eq_zero h) with h₁ h₂,
-      contradiction,
-      exact fact_ne_zero n h₂
-  end
+lemma fact_pos : ∀ n, fact n > 0
+| 0        := zero_lt_one
+| (succ n) := mul_pos !succ_pos (fact_pos n)
 
-lemma fact_gt_0 (n) : fact n > 0 :=
-pos_of_ne_zero (fact_ne_zero n)
+lemma fact_ne_zero (n : ℕ) : fact n ≠ 0 := ne_of_gt !fact_pos
 
 lemma dvd_fact : ∀ {m n}, m > 0 → m ≤ n → m ∣ fact n
 | m 0        h₁ h₂ := absurd h₁ (not_lt_of_ge h₂)

library/theories/combinatorics/choose.lean

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+
+Binomial coefficients, "n choose k".
+-/
+import data.nat.div data.nat.fact
+open decidable
+
+namespace nat
+
+/- choose -/
+
+definition choose : ℕ → ℕ → ℕ
+| 0 0               := 1
+| 0 (succ k)        := 0
+| (succ n) 0        := 1
+| (succ n) (succ k) := choose n (succ k) + choose n k
+
+theorem choose_zero_right (n : ℕ) : choose n 0 = 1 :=
+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_eq_zero_of_lt {n : ℕ} : ∀{k : ℕ}, n < k → choose n k = 0 :=
+nat.induction_on n
+  (take k, assume H : 0 < k,
+    obtain k' (H : k = succ k'), from exists_eq_succ_of_pos H,
+    by rewrite H)
+  (take n',
+    assume IH: ∀ k, n' < k → choose n' k = 0,
+    take k,
+    assume H : succ n' < k,
+    obtain k' (keq : k = succ k'), from exists_eq_succ_of_lt H,
+    assert H' : n' < k', by rewrite keq at H; apply lt_of_succ_lt_succ H,
+    by rewrite [keq, choose_succ_succ, IH _ H', IH _ (lt.trans H' !lt_succ_self)])
+
+theorem choose_self (n : ℕ) : choose n n = 1 :=
+begin
+  induction n with [n, ih],
+    {apply rfl},
+  rewrite [choose_succ_succ, ih, choose_eq_zero_of_lt !lt_succ_self]
+end
+
+theorem choose_succ_self (n : ℕ) : choose (succ n) n = succ n :=
+begin
+  induction n with [n, ih],
+    {apply rfl},
+  rewrite [choose_succ_succ, ih, choose_self, add.comm]
+end
+
+theorem choose_one_right (n : ℕ) : choose n 1 = n :=
+begin
+  induction n with [n, ih],
+    {apply rfl},
+  rewrite [choose_succ_succ, ih, choose_zero_right]
+end
+
+theorem choose_pos {n : ℕ} : ∀ {k : ℕ}, k ≤ n → choose n k > 0 :=
+begin
+  induction n with [n, ih],
+    {intros [k, H],
+      have kz : k = 0, from eq_of_le_of_ge H !zero_le,
+      rewrite [kz, choose_zero_right]; apply zero_lt_one},
+  intro k,
+  cases k with k,
+    {intro H, rewrite [choose_zero_right], apply zero_lt_one},
+  assume H : succ k ≤ succ n,
+  assert H' : k ≤ n, from le_of_succ_le_succ H,
+  by rewrite [choose_succ_succ]; apply add_pos_right (ih H')
+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 :=
+begin
+  induction n with [n, ih],
+    {intro k,
+      cases k with k',
+        {rewrite [*choose_self, one_mul, mul_one]},
+        {have H : 1 < succ (succ k'), from succ_lt_succ !zero_lt_succ,
+          rewrite [one_mul, choose_zero_succ, choose_eq_zero_of_lt H, zero_mul]}},
+  intro k,
+  cases k with k',
+    {rewrite [choose_zero_right, choose_one_right]},
+  rewrite [choose_succ_succ (succ n), mul.right_distrib, -ih (succ k')],
+  rewrite [choose_succ_succ at {1}, mul.left_distrib, *succ_mul (succ n), mul_succ, -ih k'],
+  rewrite [*add.assoc, add.left_comm (choose n _)]
+end
+
+theorem choose_mul_fact_mul_fact {n : ℕ} :
+  ∀ {k : ℕ}, k ≤ n → choose n k * fact k * fact (n - k) = fact n :=
+begin
+  induction n using nat.strong_induction_on with [n, ih],
+  cases n with n,
+    {intro k H, have kz : k = 0, from eq_zero_of_le_zero H, rewrite [kz]},
+  intro k,
+  intro H,  -- k ≤ n,
+  cases k with k,
+    {rewrite [choose_zero_right, fact_zero, *one_mul]},
+  have kle : k ≤ n, from le_of_succ_le_succ H,
+  show choose (succ n) (succ k) * fact (succ k) * fact (succ n - succ k) = fact (succ n), from
+  begin
+    rewrite [succ_sub_succ, fact_succ, -mul.assoc, -succ_mul_choose_eq],
+    rewrite [fact_succ n, -ih n !lt_succ_self kle, *mul.assoc]
+  end
+end
+
+theorem choose_def_alt {n k : ℕ} (H : k ≤ n) : choose n k = fact n div (fact k * fact (n -k)) :=
+eq.symm (div_eq_of_eq_mul_left (mul_pos !fact_pos !fact_pos)
+    (by rewrite [-mul.assoc, choose_mul_fact_mul_fact H]))
+
+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
+
+end nat

library/theories/combinatorics/combinatorics.md

@@ -0,0 +1,4 @@
+theories.combinatorics
+======================
+
+* [choose](choose.lean)

library/theories/number_theory/primes.lean

@@ -113,7 +113,7 @@ open eq.ops
 theorem infinite_primes (n : nat) : ∃ p, p ≥ n ∧ prime p :=
 let m := fact (n + 1) in
 have Hn1 : n + 1 ≥ 1, from succ_le_succ (zero_le _),
-have m_ge_1 : m ≥ 1,  from le_of_lt_succ (succ_lt_succ (fact_gt_0 _)),
+have m_ge_1 : m ≥ 1,  from le_of_lt_succ (succ_lt_succ (fact_pos _)),
 have m1_ge_2 : m + 1 ≥ 2, from succ_le_succ m_ge_1,
 obtain p (prime_p : prime p) (p_dvd_m1 : p ∣ m + 1), from ex_prime_and_dvd m1_ge_2,
 have p_ge_2 : p ≥ 2, from ge_two_of_prime prime_p,

library/theories/theories.md

@@ -2,3 +2,4 @@ theories
 ========
 
 * [number_theory](number_theory.md)
+* [combinatorics](combinatorics.md)