# Library RSA.Binomials

Require Import Arith.
Require Import Wf_nat.
Require Export MiscRsa.

Fixpoint sum_nm (n : nat) : nat → (natnat) → nat :=
fun (m : nat) (f : natnat) ⇒
match n with
| Of m
| S n'f m + sum_nm n' (S m) f
end.

Lemma sum_nm_i :
(m n : nat) (f : natnat),
sum_nm (S n) m f = f m + sum_nm n (S m) f.
auto.
Qed.

Lemma sum_nm_f :
(m n : nat) (f : natnat),
sum_nm (S n) m f = sum_nm n m f + f (m + S n).
intros m n f; generalize m; clear m; elim n; simpl in |- *; intros.
rewrite (plus_comm m); auto.
rewrite H; repeat (rewrite (plus_comm m); simpl in |- *); auto with arith.
Qed.

Lemma sum_nm_ext :
(m n : nat) (f g : natnat),
( x : nat, x nf (m + x) = g (m + x)) →
sum_nm n m f = sum_nm n m g.
Proof.
intros m n f g; generalize m; clear m; elim n; simpl in |- *; intros.
rewrite (plus_n_O m); auto.
rewrite H; auto.
rewrite (plus_n_O m); auto.
rewrite H0; auto with arith.
intros x H'; simpl in |- *; rewrite plus_n_Sm; auto with arith.
Qed.

(m n : nat) (f g : natnat),
sum_nm n m f + sum_nm n m g = sum_nm n m (fun i : natf i + g i).
Proof.
intros m n f g; generalize m; elim n; auto; intros; simpl in |- ×.
rewrite <- H.
repeat rewrite plus_assoc_reverse; apply (f_equal2 (A1:=nat) (A2:=nat)); auto.
repeat rewrite plus_assoc; apply (f_equal2 (A1:=nat) (A2:=nat)); auto.
apply plus_comm.
Qed.

Lemma sum_nm_times :
(m n x : nat) (f : natnat),
x × sum_nm n m f = sum_nm n m (fun i : natx × f i).
Proof.
intros m n x f; generalize m; elim n; auto; intros; simpl in |- ×.
rewrite <- H; auto with arith.
repeat rewrite (mult_comm x); auto.
rewrite mult_plus_distr_r; auto.
Qed.

Lemma inv_sum_nm :
(P : natProp) (i n : nat) (f : natnat),
( a b : nat, P aP bP (a + b)) →
( x : nat, x nP (f (i + x))) → P (sum_nm n i f).
Proof.
intros P i n f; generalize i; clear i; elim n; clear n; intros; simpl in |- ×.
rewrite (plus_n_O i); auto.
apply H0; auto.
rewrite (plus_n_O i); auto with arith.
apply H; auto.
intros x H'; simpl in |- *; rewrite plus_n_Sm; auto with arith.
Qed.

Lemma t_sum_Svars :
(n k : nat) (f : natnat),
sum_nm k n f = sum_nm k (S n) (fun i : natf (pred i)).
Proof.
intros n k f; generalize n; elim k; auto; intros; simpl in |- ×.
rewrite <- H; auto.
Qed.

Fixpoint binomial (a : nat) : natnat :=
fun b : nat
match a, b with
| _, O ⇒ 1
| O, S b' ⇒ 0
| S a', S b'binomial a' (S b') + binomial a' b'
end.

Lemma binomial_def1 : n : nat, binomial n 0 = 1.
Proof.
simple induction n; auto.
Qed.

Lemma binomial_def2 : n m : nat, n < mbinomial n m = 0.
simple induction n; simpl in |- *; auto.
intros m; case m; simpl in |- *; auto.
intros H'; inversion H'; auto.
intros n0 H' m; case m; simpl in |- *; auto.
intros H'0; inversion H'0; auto.
intros n1 H'0.
rewrite H'; auto with arith.
rewrite H'; auto with arith.
Qed.

Lemma binomial_def3 : n : nat, binomial n n = 1.
Proof.
simple induction n; intros; simpl in |- *; auto.
rewrite (binomial_def2 n0 (S n0)); auto.
Qed.

Lemma binomial_def4 :
n k : nat,
k < nbinomial (S n) (S k) = binomial n (S k) + binomial n k.
Proof.
simpl in |- *; auto.
Qed.

Lemma binomial_fact :
m n : nat,
binomial (n + m) n × (factorial n × factorial m) = factorial (n + m).
Proof.
intros m; elim m; clear m.
intros n; rewrite plus_comm; simpl in |- *; rewrite binomial_def3;
simpl in |- *; rewrite mult_comm; simpl in |- *; rewrite plus_comm;
simpl in |- *; auto.
intros m H' n; elim n; clear n.
simpl in |- *; rewrite plus_comm; simpl in |- *; rewrite plus_comm;
simpl in |- *; auto.
intros n H'0.
replace (S n + S m) with (S (S n + m)); [ idtac | simpl in |- × ]; auto.
rewrite binomial_def4;
[ idtac | rewrite plus_comm; simpl in |- *; rewrite plus_comm ];
auto with arith.
rewrite mult_plus_distr_r.
apply
(trans_equal (A:=nat))
with (y := factorial (S n + m) × S m + factorial (n + S m) × S n).
apply f_equal2 with (A1 := nat) (A2 := nat); auto.
rewrite <- H'.
repeat rewrite mult_assoc_reverse; rewrite (mult_comm (factorial m));
simpl in |- *; auto.
rewrite <- H'0.
rewrite <- plus_n_Sm; auto.
rewrite mult_assoc_reverse; rewrite mult_comm with (m := S n);
rewrite (mult_assoc (S n)); simpl in |- *; auto.
apply (trans_equal (A:=nat)) with (y := (S m + S n) × factorial (S n + m)).
rewrite mult_plus_distr_r; apply f_equal2 with (A1 := nat) (A2 := nat).
rewrite (mult_comm (S m)); auto.
rewrite (mult_comm (S n)); rewrite <- plus_n_Sm; auto.
rewrite (plus_comm (S m)); rewrite <- plus_n_Sm; auto.
Qed.

Theorem exp_Pascal :
a b n : nat,
power (a + b) n =
sum_nm n 0 (fun k : natbinomial n k × (power a (n - k) × power b k)).
Proof.
simple induction n; auto.
intros n0; case n0.
simpl in |- *; repeat rewrite mult_comm with (m := 1); simpl in |- *;
repeat rewrite <- plus_n_O; auto.
intros n1 H'.
apply trans_equal with (y := (a + b) × power (a + b) (S n1)).
simpl in |- *; auto.
rewrite H'; rewrite mult_plus_distr_r; repeat rewrite sum_nm_times.
rewrite sum_nm_i; rewrite binomial_def1.
replace (1 × (power a (S n1 - 0) × power b 0)) with (power a (S n1));
[ idtac
| rewrite mult_comm with (m := 1); simpl in |- *;
repeat rewrite plus_comm with (m := 0) ]; auto.
rewrite sum_nm_f; rewrite binomial_def3.
replace (S n1 - (0 + S n1)) with 0;
[ idtac | simpl in |- *; apply minus_n_n ]; auto.
replace (power a 0) with 1; auto.
replace (b × (1 × (1 × power b (0 + S n1)))) with (b × power b (S n1));
[ idtac | simpl in |- *; repeat rewrite <- plus_n_O ];
auto.
rewrite (t_sum_Svars 0 n1).
replace
(a × power a (S n1) +
sum_nm n1 1
(fun z : nat
a × (binomial (S n1) z × (power a (S n1 - z) × power b z))) +
(sum_nm n1 1
(fun x : nat
b ×
(binomial (S n1) (pred x) ×
(power a (S n1 - pred x) × power b (pred x)))) +
b × power b (S n1))) with
(power a (S (S n1)) +
(sum_nm n1 1
(fun x : nat
binomial (S (S n1)) x × (power a (S (S n1) - x) × power b x)) +
power b (S (S n1)))).
rewrite (sum_nm_i 0); rewrite (sum_nm_f 1).
rewrite binomial_def1; rewrite binomial_def3.
replace (S (S n1) - 0) with (S (S n1)); auto.
replace (S (S n1) - (1 + S n1)) with 0; auto with arith.
replace (power a 0) with 1; auto.
replace (power b 0) with 1; auto.
replace (1 × (power a (S (S n1)) × 1)) with (power a (S (S n1)));
[ idtac
| repeat rewrite mult_comm with (m := 1); simpl in |- *;
repeat rewrite plus_comm with (m := 0); simpl in |- × ];
auto.
replace (1 + S n1) with (S (S n1)); auto.
replace (1 × (1 × power b (S (S n1)))) with (power b (S (S n1)));
[ idtac
| repeat rewrite mult_comm with (m := 1); simpl in |- *;
rewrite plus_comm with (m := 0); simpl in |- × ];
auto.
repeat rewrite plus_assoc_reverse; apply plus_eq; auto.
repeat rewrite plus_assoc; apply plus_eq; auto.
apply sum_nm_ext.
intros x H'0.
replace (pred (1 + x)) with x; [ idtac | auto ].
replace (S (S n1) - (1 + x)) with (S n1 - x); [ idtac | auto ].
replace (S n1 - (1 + x)) with (n1 - x); [ idtac | auto ].
replace (1 + x) with (S x); [ idtac | auto ].
rewrite (binomial_def4 (S n1)); auto with arith.
rewrite mult_plus_distr_r.
apply plus_eq.
repeat rewrite mult_assoc; apply mult_eq; auto.
rewrite (mult_comm a); repeat rewrite mult_assoc_reverse; apply mult_eq; auto.
rewrite <- minus_Sn_m; simpl in |- *; auto.
rewrite (mult_comm b); repeat rewrite mult_assoc_reverse; apply mult_eq; auto.
apply mult_eq; auto.
simpl in |- *; apply mult_comm.
Qed.