Library mathcomp.ssreflect.binomial

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
From mathcomp Require Import div fintype tuple finfun bigop prime finset.

This files contains the definition of: 'C(n, m) == the binomial coefficient 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.

More properties of the factorial *

Lemma fact_prod n : n `! = \prod_(1 ≤ i < n .+1 ) i.

Lemma fact_split n m : m ≤ n → n `! = m `! × \prod_(m .+1 ≤ k < n .+1 ) k.

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_prod n m : n ^_ m = \prod_(i < m ) (n - i ).

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.
Arguments binomial_rec : simpl nomatch.

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 `!.

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 ).

Multiply to move down in the Pascal triangle.

Lemma mul_bin_down n m : n × 'C (n .-1 , m ) = (n - m ) × 'C (n , m ).

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 prime_modn_expSn p n : prime p → n .+1 ^ p = (n ^ p ).+1 %[mod p ].

Lemma fermat_little a p : prime p → a ^ p = a %[mod p ].

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.