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 *
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'.+1binomial_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.
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.
Multiply to move left in the Pascal triangle.
Combinatorial characterizations.