From 0940f426ed4ab1753ce3fc0876fb651fb465a682 Mon Sep 17 00:00:00 2001 From: desmettr Date: Tue, 21 Jan 2003 16:09:42 +0000 Subject: Binome.v -> Binomial.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3560 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/Binome.v | 180 ---------------------------------------------- theories/Reals/Binomial.v | 180 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 180 insertions(+), 180 deletions(-) delete mode 100644 theories/Reals/Binome.v create mode 100644 theories/Reals/Binomial.v diff --git a/theories/Reals/Binome.v b/theories/Reals/Binome.v deleted file mode 100644 index 8b5406ee78..0000000000 --- a/theories/Reals/Binome.v +++ /dev/null @@ -1,180 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (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. - -(*********************) -(* Formule du binôme *) -(*********************) -Lemma binome : (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. diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v new file mode 100644 index 0000000000..8b5406ee78 --- /dev/null +++ b/theories/Reals/Binomial.v @@ -0,0 +1,180 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (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. + +(*********************) +(* Formule du binôme *) +(*********************) +Lemma binome : (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. -- cgit v1.2.3