diff options
Diffstat (limited to 'theories7/Reals/Binomial.v')
| -rw-r--r-- | theories7/Reals/Binomial.v | 181 |
1 files changed, 181 insertions, 0 deletions
diff --git a/theories7/Reals/Binomial.v b/theories7/Reals/Binomial.v new file mode 100644 index 00000000..1dfd2ec0 --- /dev/null +++ b/theories7/Reals/Binomial.v @@ -0,0 +1,181 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Binomial.v,v 1.1.2.1 2004/07/16 19:31:31 herbelin Exp $ i*) + +Require Rbase. +Require Rfunctions. +Require PartSum. +V7only [ Import nat_scope. Import Z_scope. Import R_scope. ]. +Open Local Scope R_scope. + +Definition C [n,p:nat] : R := ``(INR (fact n))/((INR (fact p))*(INR (fact (minus n p))))``. + +Lemma pascal_step1 : (n,i:nat) (le i n) -> (C n i) == (C n (minus n i)). +Intros; Unfold C; Replace (minus n (minus n i)) with i. +Rewrite Rmult_sym. +Reflexivity. +Apply plus_minus; Rewrite plus_sym; Apply le_plus_minus; Assumption. +Qed. + +Lemma pascal_step2 : (n,i:nat) (le i n) -> (C (S n) i) == ``(INR (S n))/(INR (minus (S n) i))*(C n i)``. +Intros; Unfold C; Replace (minus (S n) i) with (S (minus n i)). +Cut (n:nat) (fact (S n))=(mult (S n) (fact n)). +Intro; Repeat Rewrite H0. +Unfold Rdiv; Repeat Rewrite mult_INR; Repeat Rewrite Rinv_Rmult. +Ring. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Apply not_O_INR; Discriminate. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Apply prod_neq_R0. +Apply not_O_INR; Discriminate. +Apply INR_fact_neq_0. +Intro; Reflexivity. +Apply minus_Sn_m; Assumption. +Qed. + +Lemma pascal_step3 : (n,i:nat) (lt i n) -> (C n (S i)) == ``(INR (minus n i))/(INR (S i))*(C n i)``. +Intros; Unfold C. +Cut (n:nat) (fact (S n))=(mult (S n) (fact n)). +Intro. +Cut (minus n i) = (S (minus n (S i))). +Intro. +Pattern 2 (minus n i); Rewrite H1. +Repeat Rewrite H0; Unfold Rdiv; Repeat Rewrite mult_INR; Repeat Rewrite Rinv_Rmult. +Rewrite <- H1; Rewrite (Rmult_sym ``/(INR (minus n i))``); Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym (INR (minus n i))); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. +Ring. +Apply not_O_INR; Apply minus_neq_O; Assumption. +Apply not_O_INR; Discriminate. +Apply INR_fact_neq_0. +Apply INR_fact_neq_0. +Apply prod_neq_R0; [Apply not_O_INR; Discriminate | Apply INR_fact_neq_0]. +Apply not_O_INR; Discriminate. +Apply INR_fact_neq_0. +Apply prod_neq_R0; [Apply not_O_INR; Discriminate | Apply INR_fact_neq_0]. +Apply INR_fact_neq_0. +Rewrite minus_Sn_m. +Simpl; Reflexivity. +Apply lt_le_S; Assumption. +Intro; Reflexivity. +Qed. + +(**********) +Lemma pascal : (n,i:nat) (lt i n) -> ``(C n i)+(C n (S i))==(C (S n) (S i))``. +Intros. +Rewrite pascal_step3; [Idtac | Assumption]. +Replace ``(C n i)+(INR (minus n i))/(INR (S i))*(C n i)`` with ``(C n i)*(1+(INR (minus n i))/(INR (S i)))``; [Idtac | Ring]. +Replace ``1+(INR (minus n i))/(INR (S i))`` with ``(INR (S n))/(INR (S i))``. +Rewrite pascal_step1. +Rewrite Rmult_sym; Replace (S i) with (minus (S n) (minus n i)). +Rewrite <- pascal_step2. +Apply pascal_step1. +Apply le_trans with n. +Apply le_minusni_n. +Apply lt_le_weak; Assumption. +Apply le_n_Sn. +Apply le_minusni_n. +Apply lt_le_weak; Assumption. +Rewrite <- minus_Sn_m. +Cut (minus n (minus n i))=i. +Intro; Rewrite H0; Reflexivity. +Symmetry; Apply plus_minus. +Rewrite plus_sym; Rewrite le_plus_minus_r. +Reflexivity. +Apply lt_le_weak; Assumption. +Apply le_minusni_n; Apply lt_le_weak; Assumption. +Apply lt_le_weak; Assumption. +Unfold Rdiv. +Repeat Rewrite S_INR. +Rewrite minus_INR. +Cut ``((INR i)+1)<>0``. +Intro. +Apply r_Rmult_mult with ``(INR i)+1``; [Idtac | Assumption]. +Rewrite Rmult_Rplus_distr. +Rewrite Rmult_1r. +Do 2 Rewrite (Rmult_sym ``(INR i)+1``). +Repeat Rewrite Rmult_assoc. +Rewrite <- Rinv_l_sym; [Idtac | Assumption]. +Ring. +Rewrite <- S_INR. +Apply not_O_INR; Discriminate. +Apply lt_le_weak; Assumption. +Qed. + +(*********************) +(*********************) +Lemma binomial : (x,y:R;n:nat) ``(pow (x+y) n)``==(sum_f_R0 [i:nat]``(C n i)*(pow x i)*(pow y (minus n i))`` n). +Intros; Induction n. +Unfold C; Simpl; Unfold Rdiv; Repeat Rewrite Rmult_1r; Rewrite Rinv_R1; Ring. +Pattern 1 (S n); Replace (S n) with (plus n (1)); [Idtac | Ring]. +Rewrite pow_add; Rewrite Hrecn. +Replace ``(pow (x+y) (S O))`` with ``x+y``; [Idtac | Simpl; Ring]. +Rewrite tech5. +Cut (p:nat)(C p p)==R1. +Cut (p:nat)(C p O)==R1. +Intros; Rewrite H0; Rewrite <- minus_n_n; Rewrite Rmult_1l. +Replace (pow y O) with R1; [Rewrite Rmult_1r | Simpl; Reflexivity]. +Induction n. +Simpl; Do 2 Rewrite H; Ring. +(* N >= 1 *) +Pose N := (S n). +Rewrite Rmult_Rplus_distr. +Replace (Rmult (sum_f_R0 ([i:nat]``(C N i)*(pow x i)*(pow y (minus N i))``) N) x) with (sum_f_R0 [i:nat]``(C N i)*(pow x (S i))*(pow y (minus N i))`` N). +Replace (Rmult (sum_f_R0 ([i:nat]``(C N i)*(pow x i)*(pow y (minus N i))``) N) y) with (sum_f_R0 [i:nat]``(C N i)*(pow x i)*(pow y (minus (S N) i))`` N). +Rewrite (decomp_sum [i:nat]``(C (S N) i)*(pow x i)*(pow y (minus (S N) i))`` N). +Rewrite H; Replace (pow x O) with R1; [Idtac | Reflexivity]. +Do 2 Rewrite Rmult_1l. +Replace (minus (S N) O) with (S N); [Idtac | Reflexivity]. +Pose An := [i:nat]``(C N i)*(pow x (S i))*(pow y (minus N i))``. +Pose Bn := [i:nat]``(C N (S i))*(pow x (S i))*(pow y (minus N i))``. +Replace (pred N) with n. +Replace (sum_f_R0 ([i:nat]``(C (S N) (S i))*(pow x (S i))*(pow y (minus (S N) (S i)))``) n) with (sum_f_R0 [i:nat]``(An i)+(Bn i)`` n). +Rewrite plus_sum. +Replace (pow x (S N)) with (An (S n)). +Rewrite (Rplus_sym (sum_f_R0 An n)). +Repeat Rewrite Rplus_assoc. +Rewrite <- tech5. +Fold N. +Pose Cn := [i:nat]``(C N i)*(pow x i)*(pow y (minus (S N) i))``. +Cut (i:nat) (lt i N)-> (Cn (S i))==(Bn i). +Intro; Replace (sum_f_R0 Bn n) with (sum_f_R0 [i:nat](Cn (S i)) n). +Replace (pow y (S N)) with (Cn O). +Rewrite <- Rplus_assoc; Rewrite (decomp_sum Cn N). +Replace (pred N) with n. +Ring. +Unfold N; Simpl; Reflexivity. +Unfold N; Apply lt_O_Sn. +Unfold Cn; Rewrite H; Simpl; Ring. +Apply sum_eq. +Intros; Apply H1. +Unfold N; Apply le_lt_trans with n; [Assumption | Apply lt_n_Sn]. +Intros; Unfold Bn Cn. +Replace (minus (S N) (S i)) with (minus N i); Reflexivity. +Unfold An; Fold N; Rewrite <- minus_n_n; Rewrite H0; Simpl; Ring. +Apply sum_eq. +Intros; Unfold An Bn; Replace (minus (S N) (S i)) with (minus N i); [Idtac | Reflexivity]. +Rewrite <- pascal; [Ring | Apply le_lt_trans with n; [Assumption | Unfold N; Apply lt_n_Sn]]. +Unfold N; Reflexivity. +Unfold N; Apply lt_O_Sn. +Rewrite <- (Rmult_sym y); Rewrite scal_sum; Apply sum_eq. +Intros; Replace (minus (S N) i) with (S (minus N i)). +Replace (S (minus N i)) with (plus (minus N i) (1)); [Idtac | Ring]. +Rewrite pow_add; Replace (pow y (S O)) with y; [Idtac | Simpl; Ring]; Ring. +Apply minus_Sn_m; Assumption. +Rewrite <- (Rmult_sym x); Rewrite scal_sum; Apply sum_eq. +Intros; Replace (S i) with (plus i (1)); [Idtac | Ring]; Rewrite pow_add; Replace (pow x (S O)) with x; [Idtac | Simpl; Ring]; Ring. +Intro; Unfold C. +Replace (INR (fact O)) with R1; [Idtac | Reflexivity]. +Replace (minus p O) with p; [Idtac | Apply minus_n_O]. +Rewrite Rmult_1l; Unfold Rdiv; Rewrite <- Rinv_r_sym; [Reflexivity | Apply INR_fact_neq_0]. +Intro; Unfold C. +Replace (minus p p) with O; [Idtac | Apply minus_n_n]. +Replace (INR (fact O)) with R1; [Idtac | Reflexivity]. +Rewrite Rmult_1r; Unfold Rdiv; Rewrite <- Rinv_r_sym; [Reflexivity | Apply INR_fact_neq_0]. +Qed. |