Library binomial

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq paths div.
Require Import choice fintype tuple finfun bigops prime finset.

This files contains the definition of:                                     
     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.                               
   'C(n, m) == the binomial coeficient n choose m                           
            := n ^_ m %/ fact m                                             


 

 In additions to the properties of these functions, triangular_sum, Wilson  
 and Pascal are examples of how to manipulate expressions with bigops.

Import Prenex Implicits.

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.

Theorem Wilson : forall 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 : forall n, n ^_ 0 = 1.

Lemma ffact0n : forall m, 0 ^_ m = (m == 0).

Lemma ffactnS : forall n m, n ^_ m.+1 = n * n.-1 ^_ m.

Lemma ffactSS : forall n m, n.+1 ^_ m.+1 = n.+1 * n ^_ m.

Lemma ffactn1 : forall n, n ^_ 1 = n.

Lemma ffactnSr : forall n m, n ^_ m.+1 = n ^_ m * (n - m).

Lemma ffact_gt0 : forall n m, (0 < n ^_ m) = (m <= n).

Lemma ffact_small : forall n m, n < m -> n ^_ m = 0.

Lemma ffactnn : forall n, n ^_ n = n`!.

Lemma ffact_fact : forall n m, m <= n -> n ^_ m * (n - m)`! = n`!.

Lemma ffact_factd : forall n m, m <= n -> n ^_ m = n`! %/ (n - m)`!.

Binomial coefficients

Fixpoint bin_rec n m :=
  match n, m with
  | n'.+1, m'.+1 => bin_rec n' m + bin_rec n' m'
  | _, 0 => 1
  | 0, _.+1 => 0
  end.

Definition binomial := nosimpl bin_rec.

Notation "''C' ( n , m )" := (binomial n m)
  (at level 8, format "''C' ( n , m )") : nat_scope.

Lemma binE : binomial = bin_rec.

Lemma bin0 : forall n, 'C(n, 0) = 1.

Lemma bin0n : forall m, 'C(0, m) = (m == 0).

Lemma binS : forall n m, 'C(n.+1, m.+1) = 'C(n, m.+1) + 'C(n, m).

Lemma bin1 : forall n, 'C(n, 1) = n.

Lemma bin_gt0 : forall m n, (0 < 'C(m, n)) = (n <= m).

Lemma bin_small : forall n m, n < m -> 'C(n, m) = 0.

Lemma binn : forall n, 'C(n, n) = 1.

Lemma mul_Sm_binm : forall m n, m.+1 * 'C(m, n) = n.+1 * 'C(m.+1, n.+1).

Lemma bin_fact : forall m n, n <= m -> 'C(m, n) * (n`! * (m - n)`!) = m`!.

In fact the only exception is n = 0 and m = 1

Lemma bin_factd : forall n m, 0 < n -> 'C(n, m) = n`! %/ (m`! * (n - m)`!).

Lemma bin_ffact : forall n m, 'C(n, m) * m`! = n ^_ m.

Lemma bin_ffactd : forall n m, 'C(n, m) = n ^_ m %/ m`!.

Lemma bin_sub : forall n m, m <= n -> 'C(n, n - m) = 'C(n, m).

Lemma binSn : forall n, 'C(n.+1, n) = n.+1.

Lemma bin2 : forall n, 'C(n, 2) = (n * n.-1)./2.

Lemma bin2odd : forall n, odd n -> 'C(n, 2) = n * n.-1./2.

Lemma prime_dvd_bin : forall k p, prime p -> 0 < k < p -> p %| 'C(p, k).

Lemma triangular_sum : forall n, \sum_(0 <= i < n) i = 'C(n, 2).

Lemma textbook_triangular_sum : forall n, \sum_(0 <= i < n) i = 'C(n, 2).

Theorem Pascal : forall a b n,
(a + b) ^ n = \sum_(i < n.+1) 'C(n, i) * (a ^ (n - i) * b ^ i).
Definition expn_addl := Pascal.

Lemma subn_exp : forall m n k,
m ^ k - n ^ k = (m - n) * (\sum_(i < k) m ^ (k.-1 -i) * n ^ i).

Lemma predn_exp : forall m k, (m ^ k).-1 = m.-1 * (\sum_(i < k) m ^ i).

Combinatorial characterizations.

Section Combinations.

Implicit Types T D : finType.

Lemma card_uniq_tuples : forall T n (A : pred T),
  #|[set t : n.-tuple T | all A t && uniq t]| = #|A| ^_ n.

Lemma card_inj_ffuns_on : forall D T (R : pred T),
  #|[set f : {ffun D -> T} | ffun_on R f && injectiveb f]| = #|R| ^_ #|D|.

Lemma card_inj_ffuns : forall D T,
  #|[set f : {ffun D -> T} | injectiveb f]| = #|T| ^_ #|D|.

Lemma card_draws : forall T k, #|[set A : {set T} | #|A| == k]| = 'C(#|T|, k).

Lemma card_ltn_sorted_tuples : forall m n,
  #|[set t : m.-tuple 'I_n | sorted ltn (map val t)]| = 'C(n, m).

Lemma card_sorted_tuples : forall m n,
  #|[set t : m.-tuple 'I_n.+1 | sorted leq (map val t)]| = 'C(m + n, m).

Lemma card_partial_ord_partitions : forall m n,
  #|[set t : m.-tuple 'I_n.+1 | \sum_(i <- t) i <= n]| = 'C(m + n, m).

Lemma card_ord_partitions : forall m n,
  #|[set t : m.+1.-tuple 'I_n.+1 | \sum_(i <- t) i == n]| = 'C(m + n, m).

End Combinations.