Library mathcomp.ssreflect.binomial
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ This files contains the definition of:
+ 'C(n, m) == the binomial coeficient n choose m.
+ n ^_ m == the falling (or lower) factorial of n with m terms, i.e.,
+ the product n * (n - 1) * ... * (n - m + 1).
+ Note that n ^_ m = 0 if m > n, and 'C(n, m) = n ^_ m %/ m/!.
+
+
+
+ In additions to the properties of these functions, we prove a few seminal
+ results such as triangular_sum, Wilson and Pascal; their proofs are good
+ examples of how to manipulate expressions with bigops.
+
+
+
+
+Set Implicit Arguments.
+ +
+
+
++Set Implicit Arguments.
+ +
+
+ More properties of the factorial *
+
+
+
+
+Lemma fact_smonotone m n : 0 < m → m < n → m`! < n`!.
+ +
+Lemma fact_prod n : n`! = \prod_(1 ≤ i < n.+1) i.
+ +
+Lemma logn_fact p n : prime p → logn p n`! = \sum_(1 ≤ k < n.+1) n %/ p ^ k.
+ +
+Theorem Wilson p : p > 1 → prime p = (p %| ((p.-1)`!).+1).
+ +
+
+
++Lemma fact_smonotone m n : 0 < m → m < n → m`! < n`!.
+ +
+Lemma fact_prod n : n`! = \prod_(1 ≤ i < n.+1) i.
+ +
+Lemma logn_fact p n : prime p → logn p n`! = \sum_(1 ≤ k < n.+1) n %/ p ^ k.
+ +
+Theorem Wilson p : p > 1 → prime p = (p %| ((p.-1)`!).+1).
+ +
+
+ The falling factorial
+
+
+
+
+Fixpoint ffact_rec n m := if m is m'.+1 then n × ffact_rec n.-1 m' else 1.
+ +
+Definition falling_factorial := nosimpl ffact_rec.
+ +
+Notation "n ^_ m" := (falling_factorial n m)
+ (at level 30, right associativity) : nat_scope.
+ +
+Lemma ffactE : falling_factorial = ffact_rec.
+ +
+Lemma ffactn0 n : n ^_ 0 = 1.
+ +
+Lemma ffact0n m : 0 ^_ m = (m == 0).
+ +
+Lemma ffactnS n m : n ^_ m.+1 = n × n.-1 ^_ m.
+ +
+Lemma ffactSS n m : n.+1 ^_ m.+1 = n.+1 × n ^_ m.
+ +
+Lemma ffactn1 n : n ^_ 1 = n.
+ +
+Lemma ffactnSr n m : n ^_ m.+1 = n ^_ m × (n - m).
+ +
+Lemma ffact_gt0 n m : (0 < n ^_ m) = (m ≤ n).
+ +
+Lemma ffact_small n m : n < m → n ^_ m = 0.
+ +
+Lemma ffactnn n : n ^_ n = n`!.
+ +
+Lemma ffact_fact n m : m ≤ n → n ^_ m × (n - m)`! = n`!.
+ +
+Lemma ffact_factd n m : m ≤ n → n ^_ m = n`! %/ (n - m)`!.
+ +
+
+
++Fixpoint ffact_rec n m := if m is m'.+1 then n × ffact_rec n.-1 m' else 1.
+ +
+Definition falling_factorial := nosimpl ffact_rec.
+ +
+Notation "n ^_ m" := (falling_factorial n m)
+ (at level 30, right associativity) : nat_scope.
+ +
+Lemma ffactE : falling_factorial = ffact_rec.
+ +
+Lemma ffactn0 n : n ^_ 0 = 1.
+ +
+Lemma ffact0n m : 0 ^_ m = (m == 0).
+ +
+Lemma ffactnS n m : n ^_ m.+1 = n × n.-1 ^_ m.
+ +
+Lemma ffactSS n m : n.+1 ^_ m.+1 = n.+1 × n ^_ m.
+ +
+Lemma ffactn1 n : n ^_ 1 = n.
+ +
+Lemma ffactnSr n m : n ^_ m.+1 = n ^_ m × (n - m).
+ +
+Lemma ffact_gt0 n m : (0 < n ^_ m) = (m ≤ n).
+ +
+Lemma ffact_small n m : n < m → n ^_ m = 0.
+ +
+Lemma ffactnn n : n ^_ n = n`!.
+ +
+Lemma ffact_fact n m : m ≤ n → n ^_ m × (n - m)`! = n`!.
+ +
+Lemma ffact_factd n m : m ≤ n → n ^_ m = n`! %/ (n - m)`!.
+ +
+
+ Binomial coefficients
+
+
+
+
+Fixpoint binomial_rec n m :=
+ match n, m with
+ | n'.+1, m'.+1 ⇒ binomial_rec n' m + binomial_rec n' m'
+ | _, 0 ⇒ 1
+ | 0, _.+1 ⇒ 0
+ end.
+ +
+Definition binomial := nosimpl binomial_rec.
+ +
+Notation "''C' ( n , m )" := (binomial n m)
+ (at level 8, format "''C' ( n , m )") : nat_scope.
+ +
+Lemma binE : binomial = binomial_rec.
+ +
+Lemma bin0 n : 'C(n, 0) = 1.
+ +
+Lemma bin0n m : 'C(0, m) = (m == 0).
+ +
+Lemma binS n m : 'C(n.+1, m.+1) = 'C(n, m.+1) + 'C(n, m).
+ +
+Lemma bin1 n : 'C(n, 1) = n.
+ +
+Lemma bin_gt0 n m : (0 < 'C(n, m)) = (m ≤ n).
+ +
+Lemma leq_bin2l n1 n2 m : n1 ≤ n2 → 'C(n1, m) ≤ 'C(n2, m).
+ +
+Lemma bin_small n m : n < m → 'C(n, m) = 0.
+ +
+Lemma binn n : 'C(n, n) = 1.
+ +
+
+
++Fixpoint binomial_rec n m :=
+ match n, m with
+ | n'.+1, m'.+1 ⇒ binomial_rec n' m + binomial_rec n' m'
+ | _, 0 ⇒ 1
+ | 0, _.+1 ⇒ 0
+ end.
+ +
+Definition binomial := nosimpl binomial_rec.
+ +
+Notation "''C' ( n , m )" := (binomial n m)
+ (at level 8, format "''C' ( n , m )") : nat_scope.
+ +
+Lemma binE : binomial = binomial_rec.
+ +
+Lemma bin0 n : 'C(n, 0) = 1.
+ +
+Lemma bin0n m : 'C(0, m) = (m == 0).
+ +
+Lemma binS n m : 'C(n.+1, m.+1) = 'C(n, m.+1) + 'C(n, m).
+ +
+Lemma bin1 n : 'C(n, 1) = n.
+ +
+Lemma bin_gt0 n m : (0 < 'C(n, m)) = (m ≤ n).
+ +
+Lemma leq_bin2l n1 n2 m : n1 ≤ n2 → 'C(n1, m) ≤ 'C(n2, m).
+ +
+Lemma bin_small n m : n < m → 'C(n, m) = 0.
+ +
+Lemma binn n : 'C(n, n) = 1.
+ +
+
+ Multiply to move diagonally down and right in the Pascal triangle.
+
+
+Lemma mul_bin_diag n m : n × 'C(n.-1, m) = m.+1 × 'C(n, m.+1).
+ +
+Lemma bin_fact n m : m ≤ n → 'C(n, m) × (m`! × (n - m)`!) = n`!.
+ +
+
+
++ +
+Lemma bin_fact n m : m ≤ n → 'C(n, m) × (m`! × (n - m)`!) = n`!.
+ +
+
+ In fact the only exception for bin_factd is n = 0 and m = 1
+
+
+Lemma bin_factd n m : 0 < n → 'C(n, m) = n`! %/ (m`! × (n - m)`!).
+ +
+Lemma bin_ffact n m : 'C(n, m) × m`! = n ^_ m.
+ +
+Lemma bin_ffactd n m : 'C(n, m) = n ^_ m %/ m`!.
+ +
+Lemma bin_sub n m : m ≤ n → 'C(n, n - m) = 'C(n, m).
+ +
+
+
++ +
+Lemma bin_ffact n m : 'C(n, m) × m`! = n ^_ m.
+ +
+Lemma bin_ffactd n m : 'C(n, m) = n ^_ m %/ m`!.
+ +
+Lemma bin_sub n m : m ≤ n → 'C(n, n - m) = 'C(n, m).
+ +
+
+ Multiply to move down in the Pascal triangle.
+
+
+
+
+ Multiply to move left in the Pascal triangle.
+
+
+Lemma mul_bin_left n m : m.+1 × 'C(n, m.+1) = (n - m) × 'C(n, m).
+ +
+Lemma binSn n : 'C(n.+1, n) = n.+1.
+ +
+Lemma bin2 n : 'C(n, 2) = (n × n.-1)./2.
+ +
+Lemma bin2odd n : odd n → 'C(n, 2) = n × n.-1./2.
+ +
+Lemma prime_dvd_bin k p : prime p → 0 < k < p → p %| 'C(p, k).
+ +
+Lemma triangular_sum n : \sum_(0 ≤ i < n) i = 'C(n, 2).
+ +
+Lemma textbook_triangular_sum n : \sum_(0 ≤ i < n) i = 'C(n, 2).
+ +
+Theorem Pascal a b n :
+ (a + b) ^ n = \sum_(i < n.+1) 'C(n, i) × (a ^ (n - i) × b ^ i).
+Definition expnDn := Pascal.
+ +
+Lemma Vandermonde k l i :
+ \sum_(j < i.+1) 'C(k, j) × 'C(l, i - j) = 'C(k + l , i).
+ +
+Lemma subn_exp m n k :
+ m ^ k - n ^ k = (m - n) × (\sum_(i < k) m ^ (k.-1 -i) × n ^ i).
+ +
+Lemma predn_exp m k : (m ^ k).-1 = m.-1 × (\sum_(i < k) m ^ i).
+ +
+Lemma dvdn_pred_predX n e : (n.-1 %| (n ^ e).-1)%N.
+ +
+Lemma modn_summ I r (P : pred I) F d :
+ \sum_(i <- r | P i) F i %% d = \sum_(i <- r | P i) F i %[mod d].
+ +
+
+
++ +
+Lemma binSn n : 'C(n.+1, n) = n.+1.
+ +
+Lemma bin2 n : 'C(n, 2) = (n × n.-1)./2.
+ +
+Lemma bin2odd n : odd n → 'C(n, 2) = n × n.-1./2.
+ +
+Lemma prime_dvd_bin k p : prime p → 0 < k < p → p %| 'C(p, k).
+ +
+Lemma triangular_sum n : \sum_(0 ≤ i < n) i = 'C(n, 2).
+ +
+Lemma textbook_triangular_sum n : \sum_(0 ≤ i < n) i = 'C(n, 2).
+ +
+Theorem Pascal a b n :
+ (a + b) ^ n = \sum_(i < n.+1) 'C(n, i) × (a ^ (n - i) × b ^ i).
+Definition expnDn := Pascal.
+ +
+Lemma Vandermonde k l i :
+ \sum_(j < i.+1) 'C(k, j) × 'C(l, i - j) = 'C(k + l , i).
+ +
+Lemma subn_exp m n k :
+ m ^ k - n ^ k = (m - n) × (\sum_(i < k) m ^ (k.-1 -i) × n ^ i).
+ +
+Lemma predn_exp m k : (m ^ k).-1 = m.-1 × (\sum_(i < k) m ^ i).
+ +
+Lemma dvdn_pred_predX n e : (n.-1 %| (n ^ e).-1)%N.
+ +
+Lemma modn_summ I r (P : pred I) F d :
+ \sum_(i <- r | P i) F i %% d = \sum_(i <- r | P i) F i %[mod d].
+ +
+
+ Combinatorial characterizations.
+
+
+
+
+Section Combinations.
+ +
+Implicit Types T D : finType.
+ +
+Lemma card_uniq_tuples T n (A : pred T) :
+ #|[set t : n.-tuple T | all A t & uniq t]| = #|A| ^_ n.
+ +
+Lemma card_inj_ffuns_on D T (R : pred T) :
+ #|[set f : {ffun D → T} in ffun_on R | injectiveb f]| = #|R| ^_ #|D|.
+ +
+Lemma card_inj_ffuns D T :
+ #|[set f : {ffun D → T} | injectiveb f]| = #|T| ^_ #|D|.
+ +
+Lemma cards_draws T (B : {set T}) k :
+ #|[set A : {set T} | A \subset B & #|A| == k]| = 'C(#|B|, k).
+ +
+Lemma card_draws T k : #|[set A : {set T} | #|A| == k]| = 'C(#|T|, k).
+ +
+Lemma card_ltn_sorted_tuples m n :
+ #|[set t : m.-tuple 'I_n | sorted ltn (map val t)]| = 'C(n, m).
+ +
+Lemma card_sorted_tuples m n :
+ #|[set t : m.-tuple 'I_n.+1 | sorted leq (map val t)]| = 'C(m + n, m).
+ +
+Lemma card_partial_ord_partitions m n :
+ #|[set t : m.-tuple 'I_n.+1 | \sum_(i <- t) i ≤ n]| = 'C(m + n, m).
+ +
+Lemma card_ord_partitions m n :
+ #|[set t : m.+1.-tuple 'I_n.+1 | \sum_(i <- t) i == n]| = 'C(m + n, m).
+ +
+End Combinations.
+ +
+
++Section Combinations.
+ +
+Implicit Types T D : finType.
+ +
+Lemma card_uniq_tuples T n (A : pred T) :
+ #|[set t : n.-tuple T | all A t & uniq t]| = #|A| ^_ n.
+ +
+Lemma card_inj_ffuns_on D T (R : pred T) :
+ #|[set f : {ffun D → T} in ffun_on R | injectiveb f]| = #|R| ^_ #|D|.
+ +
+Lemma card_inj_ffuns D T :
+ #|[set f : {ffun D → T} | injectiveb f]| = #|T| ^_ #|D|.
+ +
+Lemma cards_draws T (B : {set T}) k :
+ #|[set A : {set T} | A \subset B & #|A| == k]| = 'C(#|B|, k).
+ +
+Lemma card_draws T k : #|[set A : {set T} | #|A| == k]| = 'C(#|T|, k).
+ +
+Lemma card_ltn_sorted_tuples m n :
+ #|[set t : m.-tuple 'I_n | sorted ltn (map val t)]| = 'C(n, m).
+ +
+Lemma card_sorted_tuples m n :
+ #|[set t : m.-tuple 'I_n.+1 | sorted leq (map val t)]| = 'C(m + n, m).
+ +
+Lemma card_partial_ord_partitions m n :
+ #|[set t : m.-tuple 'I_n.+1 | \sum_(i <- t) i ≤ n]| = 'C(m + n, m).
+ +
+Lemma card_ord_partitions m n :
+ #|[set t : m.+1.-tuple 'I_n.+1 | \sum_(i <- t) i == n]| = 'C(m + n, m).
+ +
+End Combinations.
+ +
+