Merge branch 'experimental/upstream' into upstream

1 files changed, 34 insertions, 36 deletions

diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v
index 55c30aec..ad076c48 100644
--- a/theories/Reals/Binomial.v
+++ b/theories/Reals/Binomial.v
@@ -1,24 +1,22 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <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        *)
 (************************************************************************)
 
-  (*i $Id: Binomial.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 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.
@@ -28,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.
@@ -48,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)));
@@ -70,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.
@@ -97,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).
@@ -127,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.
@@ -160,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).
@@ -168,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.