Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids
  Basics.Decidable Spaces.Nat.Core Spaces.Nat.Division Tactics.EvalIn.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Set Universe Minimization ToSet.

Local Open Scope nat_scope.

(** * Factorials *)

(** ** Definition *)

Fixpoint factorial n := 
  match n with
  | 0 => 1
  | S n => S n * factorial n
  end.

(** ** Properties *)

(** The factorial of [0] is [1]. *)
Definition nat_factorial_zero : factorial 0 = 1 := idpath.

(** The factorial of [n + 1] is [n + 1] times the factorial of [n]. *)
Definition nat_factorial_succ n : factorial n.+1 = n.+1 * factorial n
  := idpath.

(** A variant of [nat_factorial_succ]. *)
Definition nat_factorial_pred n
  : 0 < n -> factorial n = n * factorial (nat_pred n).
n: nat
0 < n -> factorial n = n * factorial (nat_pred n)
Proof.
n: nat
0 < n -> factorial n = n * factorial (nat_pred n)
  intros []; reflexivity.
Defined.

(** Every factorial is positive. *)
Instance lt_zero_factorial n : 0 < factorial n.
n: nat
0 < factorial n
Proof.
n: nat
0 < factorial n
  induction n; exact _.
Defined.

(** Except for [factorial 0 = factorial 1], the [factorial] function is strictly monotone.  We separate out the successor case since it is used twice in the proof of the general result. *)
Definition nat_factorial_strictly_monotone_succ n
  : 0 < n -> factorial n < factorial n.+1.
n: nat
0 < n -> factorial n < factorial n.+1
Proof.
n: nat
0 < n -> factorial n < factorial n.+1
  intro H.
n: nat
H: 0 < n
factorial n < factorial n.+1
  rewrite <- (nat_mul_one_l (factorial n)).
n: nat
H: 0 < n
1 * factorial n < factorial n.+1
  rapply (nat_mul_r_strictly_monotone _).
Defined.

Instance nat_factorial_strictly_monotone n m
  : 0 < n -> n < m -> factorial n < factorial m.
n, m: nat
0 < n -> n < m -> factorial n < factorial m
Proof.
n, m: nat
0 < n -> n < m -> factorial n < factorial m
  intros H1 H2; induction H2.
n: nat
H1: 0 < n
factorial n < factorial n.+1
n: nat
H1: 0 < n
m: nat
H2: n.+1 <= m
IHleq: factorial n < factorial m
factorial n < factorial m.+1
  -
n: nat
H1: 0 < n
factorial n < factorial n.+1 rapply nat_factorial_strictly_monotone_succ.
  -
n: nat
H1: 0 < n
m: nat
H2: n.+1 <= m
IHleq: factorial n < factorial m
factorial n < factorial m.+1 apply (lt_trans IHleq).
n: nat
H1: 0 < n
m: nat
H2: n.+1 <= m
IHleq: factorial n < factorial m
factorial m < factorial m.+1
    rapply nat_factorial_strictly_monotone_succ.
Defined.

(** ** Divisibility *)

(** Any number less than or equal to [n] divides [factorial n]. *)
Instance nat_divides_factorial_factor n m
  : 0 < n -> n <= m -> (n | factorial m).
n, m: nat
0 < n -> n <= m -> (n | factorial m)
Proof.
n, m: nat
0 < n -> n <= m -> (n | factorial m)
  intros [] H2.
n, m: nat
H2: 1 <= m
(1 | factorial m)
n, m, m0: nat
l: 1 <= m0
H2: m0.+1 <= m
(m0.+1 | factorial m)
  1: exact _.
n, m, m0: nat
l: 1 <= m0
H2: m0.+1 <= m
(m0.+1 | factorial m)
  induction H2; exact _.
Defined.

(** [factorial] is a monotone function from [nat] to [nat] with respect to [<=] and divides. *)
Instance nat_divides_factorial_lt n m
  : n <= m -> (factorial n | factorial m).
n, m: nat
n <= m -> (factorial n | factorial m)
Proof.
n, m: nat
n <= m -> (factorial n | factorial m)
  intros H; induction H; exact _.
Defined.

(** A product of factorials divides the factorial of the sum. *)
Instance nat_divides_factorial_mul_factorial_add n m
  : (factorial n * factorial m | factorial (n + m)).
n, m: nat
(factorial n * factorial m | factorial (n + m))
Proof.
n, m: nat
(factorial n * factorial m | factorial (n + m))
  remember (n + m) as k eqn:p.
n, m, k: nat
p: n + m = k
(factorial n * factorial m | factorial k)
  revert k n m p; snapply nat_ind_strong; hnf; intros k IH n m p.
k: nat
IH: forall m : nat,
m < k ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k
(factorial n * factorial m | factorial k)
  destruct k.
IH: forall m : nat,
m < 0 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = 0
(factorial n * factorial m | factorial 0)
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
(factorial n * factorial m | factorial k.+1)
  {
IH: forall m : nat,
m < 0 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = 0
(factorial n * factorial m | factorial 0) apply equiv_nat_add_zero in p.
IH: forall m : nat,
m < 0 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: ((n = 0) * (m = 0))%type
(factorial n * factorial m | factorial 0)
    destruct p as [p q].
IH: forall m : nat,
m < 0 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n = 0
q: m = 0
(factorial n * factorial m | factorial 0)
    destruct p^, q^.
IH: forall m : nat,
m < 0 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
p, q: 0 = 0
(factorial 0 * factorial 0 | factorial 0)
    exact _. }
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
(factorial n * factorial m | factorial k.+1)
  rewrite_refl nat_factorial_succ.
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
(factorial n * factorial m | k.+1 * factorial k)
  rewrite <- p.
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
(factorial n * factorial m | (n + m) * factorial k)
  rewrite nat_dist_r.
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
(factorial n * factorial m
| n * factorial k + m * factorial k)
  assert (helper : forall n' m' (p' : n' + m' = k.+1), (factorial n' * factorial m' | n' * factorial k)).
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
forall n' m' : nat,
n' + m' = k.+1 ->
(factorial n' * factorial m' | n' * factorial k)
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
helper: forall n' m' : nat,
n' + m' = k.+1 ->
(factorial n' * factorial m'
| n' * factorial k)
(factorial n * factorial m
| n * factorial k + m * factorial k)
  -
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
forall n' m' : nat,
n' + m' = k.+1 ->
(factorial n' * factorial m' | n' * factorial k) intros n' m' p'.
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
n', m': nat
p': n' + m' = k.+1
(factorial n' * factorial m' | n' * factorial k)
    destruct n'; only 1: exact _.
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
n', m': nat
p': n'.+1 + m' = k.+1
(factorial n'.+1 * factorial m' | n'.+1 * factorial k)
    rewrite nat_factorial_succ.
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
n', m': nat
p': n'.+1 + m' = k.+1
(n'.+1 * factorial n' * factorial m'
| n'.+1 * factorial k)
    rewrite <- nat_mul_assoc.
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
n', m': nat
p': n'.+1 + m' = k.+1
(n'.+1 * (factorial n' * factorial m')
| n'.+1 * factorial k)
    rapply nat_divides_mul_monotone.
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
n', m': nat
p': n'.+1 + m' = k.+1
(factorial n' * factorial m' | factorial k)
    rapply IH.
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
n', m': nat
p': n'.+1 + m' = k.+1
n' + m' = k
    exact (ap nat_pred p').
  -
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
helper: forall n' m' : nat,
n' + m' = k.+1 ->
(factorial n' * factorial m'
| n' * factorial k)
(factorial n * factorial m
| n * factorial k + m * factorial k) napply nat_divides_add.
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
helper: forall n' m' : nat,
n' + m' = k.+1 ->
(factorial n' * factorial m'
| n' * factorial k)
(factorial n * factorial m | n * factorial k)
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
helper: forall n' m' : nat,
n' + m' = k.+1 ->
(factorial n' * factorial m'
| n' * factorial k)
(factorial n * factorial m | m * factorial k)
    +
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
helper: forall n' m' : nat,
n' + m' = k.+1 ->
(factorial n' * factorial m'
| n' * factorial k)
(factorial n * factorial m | n * factorial k) apply helper, p.
    +
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
helper: forall n' m' : nat,
n' + m' = k.+1 ->
(factorial n' * factorial m'
| n' * factorial k)
(factorial n * factorial m | m * factorial k) rewrite nat_mul_comm.
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
helper: forall n' m' : nat,
n' + m' = k.+1 ->
(factorial n' * factorial m'
| n' * factorial k)
(factorial m * factorial n | m * factorial k)
      apply helper.
k: nat
IH: forall m : nat,
m < k.+1 ->
forall n m0 : nat,
n + m0 = m ->
(factorial n * factorial m0 | factorial m)
n, m: nat
p: n + m = k.+1
helper: forall n' m' : nat,
n' + m' = k.+1 ->
(factorial n' * factorial m'
| n' * factorial k)
m + n = k.+1
      lhs napply nat_add_comm; exact p.
Defined.

(** Here is a variant of [nat_divides_factorial_mul_factorial_add] that is more suitable for binomial coefficients. *)
Instance nat_divides_factorial_mul_factorial_add' n m
  : m <= n -> (factorial m * factorial (n - m) | factorial n).
n, m: nat
m <= n ->
(factorial m * factorial (n - m) | factorial n)
Proof.
n, m: nat
m <= n ->
(factorial m * factorial (n - m) | factorial n)
  intros H.
n, m: nat
H: m <= n
(factorial m * factorial (n - m) | factorial n)
  rewrite <- (ap factorial (nat_add_sub_r_cancel H)).
n, m: nat
H: m <= n
(factorial m * factorial (n - m)
| factorial (m + (n - m)))
  apply nat_divides_factorial_mul_factorial_add.
Defined.