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 bin2_sum, Wilson and expnDn; 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 := ffact_rec.
Arguments falling_factorial : simpl never.

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 n m :=
  match n, m with
  | n'.+1, m'.+1 ⇒ binomial n' m + binomial n' m'
  | _, 0 ⇒ 1
  | 0, _.+1 ⇒ 0
  end.
Arguments binomial : simpl never.

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

Lemma binE n m : binomial n m =
  match n, m with
  | n'.+1, m'.+1 ⇒ binomial n' m + binomial n' m'
  | _, 0 ⇒ 1
  | 0, _.+1 ⇒ 0
  end.

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 bin2_sum n : \sum_(0 ≤ i < n) i = 'C(n, 2).

#[deprecated(since="mathcomp 2.3.0", note="Use bin2_sum instead.")]
Notation triangular_sum := bin2_sum (only parsing).

textbook proof of `bin2_sum`. Should be moved out of the main library, to a dedicated "showcase" library. Lemma textbook_triangular_sum n : \sum_(0 <= i < n) i = 'C(n, 2). Proof. rewrite bin2; apply: canRL half_double _. rewrite -addnn {1}big_nat_rev -big_split big_mkord /= ?add0n. rewrite (eq_bigr (fun _ => n.-1)); first by rewrite sum_nat_const card_ord. by case: n => [|n] [i le_i_n] //=; rewrite subSS subnK. Qed.

Theorem expnDn a b n :
  (a + b) ^ n = \sum_(i < n.+1) 'C(n, i) × (a ^ (n - i) × b ^ i).

#[deprecated(since="mathcomp 2.3.0", note="Use expnDn instead.")]
Definition Pascal := expnDn.

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.