summaryrefslogtreecommitdiff
path: root/theories/Reals/Binomial.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/Binomial.v')
-rw-r--r--theories/Reals/Binomial.v68
1 files changed, 34 insertions, 34 deletions
diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v
index 412f6442..ad076c48 100644
--- a/theories/Reals/Binomial.v
+++ b/theories/Reals/Binomial.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -9,14 +9,14 @@
Require Import Rbase.
Require Import Rfunctions.
Require Import PartSum.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
Definition C (n p:nat) : R :=
INR (fact n) / (INR (fact p) * INR (fact (n - p))).
Lemma pascal_step1 : forall n i:nat, (i <= n)%nat -> C n i = C n (n - i).
Proof.
- intros; unfold C in |- *; replace (n - (n - i))%nat with i.
+ intros; unfold C; replace (n - (n - i))%nat with i.
rewrite Rmult_comm.
reflexivity.
apply plus_minus; rewrite plus_comm; apply le_plus_minus; assumption.
@@ -26,10 +26,10 @@ Lemma pascal_step2 :
forall n i:nat,
(i <= n)%nat -> C (S n) i = INR (S n) / INR (S n - i) * C n i.
Proof.
- intros; unfold C in |- *; replace (S n - i)%nat with (S (n - i)).
+ intros; unfold C; replace (S n - i)%nat with (S (n - i)).
cut (forall n:nat, fact (S n) = (S n * fact n)%nat).
intro; repeat rewrite H0.
- unfold Rdiv in |- *; repeat rewrite mult_INR; repeat rewrite Rinv_mult_distr.
+ unfold Rdiv; repeat rewrite mult_INR; repeat rewrite Rinv_mult_distr.
ring.
apply INR_fact_neq_0.
apply INR_fact_neq_0.
@@ -46,13 +46,13 @@ Qed.
Lemma pascal_step3 :
forall n i:nat, (i < n)%nat -> C n (S i) = INR (n - i) / INR (S i) * C n i.
Proof.
- intros; unfold C in |- *.
+ intros; unfold C.
cut (forall n:nat, fact (S n) = (S n * fact n)%nat).
intro.
cut ((n - i)%nat = S (n - S i)).
intro.
- pattern (n - i)%nat at 2 in |- *; rewrite H1.
- repeat rewrite H0; unfold Rdiv in |- *; repeat rewrite mult_INR;
+ pattern (n - i)%nat at 2; rewrite H1.
+ repeat rewrite H0; unfold Rdiv; repeat rewrite mult_INR;
repeat rewrite Rinv_mult_distr.
rewrite <- H1; rewrite (Rmult_comm (/ INR (n - i)));
repeat rewrite Rmult_assoc; rewrite (Rmult_comm (INR (n - i)));
@@ -68,7 +68,7 @@ Proof.
apply prod_neq_R0; [ apply not_O_INR; discriminate | apply INR_fact_neq_0 ].
apply INR_fact_neq_0.
rewrite minus_Sn_m.
- simpl in |- *; reflexivity.
+ simpl; reflexivity.
apply lt_le_S; assumption.
intro; reflexivity.
Qed.
@@ -95,13 +95,13 @@ Proof.
rewrite <- minus_Sn_m.
cut ((n - (n - i))%nat = i).
intro; rewrite H0; reflexivity.
- symmetry in |- *; apply plus_minus.
+ symmetry ; apply plus_minus.
rewrite plus_comm; 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 in |- *.
+ unfold Rdiv.
repeat rewrite S_INR.
rewrite minus_INR.
cut (INR i + 1 <> 0).
@@ -125,18 +125,18 @@ Lemma binomial :
(x + y) ^ n = sum_f_R0 (fun i:nat => C n i * x ^ i * y ^ (n - i)) n.
Proof.
intros; induction n as [| n Hrecn].
- unfold C in |- *; simpl in |- *; unfold Rdiv in |- *;
+ unfold C; simpl; unfold Rdiv;
repeat rewrite Rmult_1_r; rewrite Rinv_1; ring.
- pattern (S n) at 1 in |- *; replace (S n) with (n + 1)%nat; [ idtac | ring ].
+ pattern (S n) at 1; replace (S n) with (n + 1)%nat; [ idtac | ring ].
rewrite pow_add; rewrite Hrecn.
- replace ((x + y) ^ 1) with (x + y); [ idtac | simpl in |- *; ring ].
+ replace ((x + y) ^ 1) with (x + y); [ idtac | simpl; ring ].
rewrite tech5.
cut (forall p:nat, C p p = 1).
cut (forall p:nat, C p 0 = 1).
intros; rewrite H0; rewrite <- minus_n_n; rewrite Rmult_1_l.
- replace (y ^ 0) with 1; [ rewrite Rmult_1_r | simpl in |- *; reflexivity ].
+ replace (y ^ 0) with 1; [ rewrite Rmult_1_r | simpl; reflexivity ].
induction n as [| n Hrecn0].
- simpl in |- *; do 2 rewrite H; ring.
+ simpl; do 2 rewrite H; ring.
(* N >= 1 *)
set (N := S n).
rewrite Rmult_plus_distr_l.
@@ -158,7 +158,7 @@ Proof.
rewrite (Rplus_comm (sum_f_R0 An n)).
repeat rewrite Rplus_assoc.
rewrite <- tech5.
- fold N in |- *.
+ fold N.
set (Cn := fun i:nat => C N i * x ^ i * y ^ (S N - i)).
cut (forall i:nat, (i < N)%nat -> Cn (S i) = Bn i).
intro; replace (sum_f_R0 Bn n) with (sum_f_R0 (fun i:nat => Cn (S i)) n).
@@ -166,42 +166,42 @@ Proof.
rewrite <- Rplus_assoc; rewrite (decomp_sum Cn N).
replace (pred N) with n.
ring.
- unfold N in |- *; simpl in |- *; reflexivity.
- unfold N in |- *; apply lt_O_Sn.
- unfold Cn in |- *; rewrite H; simpl in |- *; 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 in |- *; apply le_lt_trans with n; [ assumption | apply lt_n_Sn ].
- intros; unfold Bn, Cn in |- *.
+ unfold N; apply le_lt_trans with n; [ assumption | apply lt_n_Sn ].
+ intros; unfold Bn, Cn.
replace (S N - S i)%nat with (N - i)%nat; reflexivity.
- unfold An in |- *; fold N in |- *; rewrite <- minus_n_n; rewrite H0;
- simpl in |- *; ring.
+ unfold An; fold N; rewrite <- minus_n_n; rewrite H0;
+ simpl; ring.
apply sum_eq.
- intros; unfold An, Bn in |- *; replace (S N - S i)%nat with (N - i)%nat;
+ intros; unfold An, Bn; replace (S N - S i)%nat with (N - i)%nat;
[ idtac | reflexivity ].
rewrite <- pascal;
[ ring
- | apply le_lt_trans with n; [ assumption | unfold N in |- *; apply lt_n_Sn ] ].
- unfold N in |- *; reflexivity.
- unfold N in |- *; apply lt_O_Sn.
+ | apply le_lt_trans with n; [ assumption | unfold N; apply lt_n_Sn ] ].
+ unfold N; reflexivity.
+ unfold N; apply lt_O_Sn.
rewrite <- (Rmult_comm y); rewrite scal_sum; apply sum_eq.
intros; replace (S N - i)%nat with (S (N - i)).
replace (S (N - i)) with (N - i + 1)%nat; [ idtac | ring ].
- rewrite pow_add; replace (y ^ 1) with y; [ idtac | simpl in |- *; ring ];
+ rewrite pow_add; replace (y ^ 1) with y; [ idtac | simpl; ring ];
ring.
apply minus_Sn_m; assumption.
rewrite <- (Rmult_comm x); rewrite scal_sum; apply sum_eq.
intros; replace (S i) with (i + 1)%nat; [ idtac | ring ]; rewrite pow_add;
- replace (x ^ 1) with x; [ idtac | simpl in |- *; ring ];
+ replace (x ^ 1) with x; [ idtac | simpl; ring ];
ring.
- intro; unfold C in |- *.
+ intro; unfold C.
replace (INR (fact 0)) with 1; [ idtac | reflexivity ].
replace (p - 0)%nat with p; [ idtac | apply minus_n_O ].
- rewrite Rmult_1_l; unfold Rdiv in |- *; rewrite <- Rinv_r_sym;
+ rewrite Rmult_1_l; unfold Rdiv; rewrite <- Rinv_r_sym;
[ reflexivity | apply INR_fact_neq_0 ].
- intro; unfold C in |- *.
+ intro; unfold C.
replace (p - p)%nat with 0%nat; [ idtac | apply minus_n_n ].
replace (INR (fact 0)) with 1; [ idtac | reflexivity ].
- rewrite Rmult_1_r; unfold Rdiv in |- *; rewrite <- Rinv_r_sym;
+ rewrite Rmult_1_r; unfold Rdiv; rewrite <- Rinv_r_sym;
[ reflexivity | apply INR_fact_neq_0 ].
Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 16:42:03 +0000