Merge tag 'upstream/8.4dfsg' into experimental/master

Upstream version 8.4dfsg

1 files changed, 57 insertions, 57 deletions

diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v
index 105d8347..e714f5f8 100644
--- a/theories/Reals/Rderiv.v
+++ b/theories/Reals/Rderiv.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        *)
@@ -16,7 +16,7 @@ Require Import Rfunctions.
 Require Import Rlimit.
 Require Import Fourier.
 Require Import Omega.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 (*********)
 Definition D_x (D:R -> Prop) (y x:R) : Prop := D x /\ y <> x.
@@ -34,18 +34,18 @@ Lemma cont_deriv :
   forall (f d:R -> R) (D:R -> Prop) (x0:R),
     D_in f d D x0 -> continue_in f D x0.
 Proof.
-  unfold continue_in in |- *; unfold D_in in |- *; unfold limit1_in in |- *;
-    unfold limit_in in |- *; unfold Rdiv in |- *; simpl in |- *;
+  unfold continue_in; unfold D_in; unfold limit1_in;
+    unfold limit_in; unfold Rdiv; simpl;
       intros; elim (H eps H0); clear H; intros; elim H;
         clear H; intros; elim (Req_dec (d x0) 0); intro.
   split with (Rmin 1 x); split.
   elim (Rmin_Rgt 1 x 0); intros a b; apply (b (conj Rlt_0_1 H)).
   intros; elim H3; clear H3; intros;
     generalize (let (H1, H2) := Rmin_Rgt 1 x (R_dist x1 x0) in H1);
-      unfold Rgt in |- *; intro; elim (H5 H4); clear H5;
+      unfold Rgt; intro; elim (H5 H4); clear H5;
         intros; generalize (H1 x1 (conj H3 H6)); clear H1;
           intro; unfold D_x in H3; elim H3; intros.
-  rewrite H2 in H1; unfold R_dist in |- *; unfold R_dist in H1;
+  rewrite H2 in H1; unfold R_dist; unfold R_dist in H1;
     cut (Rabs (f x1 - f x0) < eps * Rabs (x1 - x0)).
   intro; unfold R_dist in H5;
     generalize (Rmult_lt_compat_l eps (Rabs (x1 - x0)) 1 H0 H5);
@@ -68,7 +68,7 @@ Proof.
   intros; elim (Rmin_Rgt (Rmin (/ 2) x) (eps * / Rabs (2 * d x0)) 0);
     intros a b; apply (b (conj H4 H3)).
   apply Rmult_gt_0_compat; auto.
-  unfold Rgt in |- *; apply Rinv_0_lt_compat; apply Rabs_pos_lt;
+  unfold Rgt; apply Rinv_0_lt_compat; apply Rabs_pos_lt;
     apply Rmult_integral_contrapositive; split.
   discrR.
   assumption.
@@ -80,17 +80,17 @@ Proof.
     generalize
       (let (H1, H2) :=
         Rmin_Rgt (Rmin (/ 2) x) (eps * / Rabs (2 * d x0)) (R_dist x1 x0) in
-        H1); unfold Rgt in |- *; intro; elim (H5 H4); clear H5;
+        H1); unfold Rgt; intro; elim (H5 H4); clear H5;
       intros; generalize (let (H1, H2) := Rmin_Rgt (/ 2) x (R_dist x1 x0) in H1);
-        unfold Rgt in |- *; intro; elim (H7 H5); clear H7;
+        unfold Rgt; intro; elim (H7 H5); clear H7;
           intros; clear H4 H5; generalize (H1 x1 (conj H3 H8));
             clear H1; intro; unfold D_x in H3; elim H3; intros;
-              generalize (sym_not_eq H5); clear H5; intro H5;
+              generalize (not_eq_sym H5); clear H5; intro H5;
                 generalize (Rminus_eq_contra x1 x0 H5); intro; generalize H1;
-                  pattern (d x0) at 1 in |- *;
+                  pattern (d x0) at 1;
                     rewrite <- (let (H1, H2) := Rmult_ne (d x0) in H2);
-                      rewrite <- (Rinv_l (x1 - x0) H9); unfold R_dist in |- *;
-                        unfold Rminus at 1 in |- *; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0)));
+                      rewrite <- (Rinv_l (x1 - x0) H9); unfold R_dist;
+                        unfold Rminus at 1; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0)));
                           rewrite (Rmult_comm (/ (x1 - x0) * (x1 - x0)) (d x0));
                             rewrite <- (Ropp_mult_distr_l_reverse (d x0) (/ (x1 - x0) * (x1 - x0)));
                               rewrite (Rmult_comm (- d x0) (/ (x1 - x0) * (x1 - x0)));
@@ -113,7 +113,7 @@ Proof.
                                                   ; generalize (Rabs_triang_inv (f x1 - f x0) ((x1 - x0) * d x0));
                                                     intro; rewrite (Rmult_comm (x1 - x0) (- d x0));
                                                       rewrite (Ropp_mult_distr_l_reverse (d x0) (x1 - x0));
-                                                        fold (f x1 - f x0 - d x0 * (x1 - x0)) in |- *;
+                                                        fold (f x1 - f x0 - d x0 * (x1 - x0));
                                                           rewrite (Rmult_comm (x1 - x0) (d x0)) in H10; clear H1;
                                                             intro;
                                                               generalize
@@ -123,7 +123,7 @@ Proof.
                                                                   generalize
                                                                     (Rplus_lt_compat_l (Rabs (d x0 * (x1 - x0)))
                                                                       (Rabs (f x1 - f x0) - Rabs (d x0 * (x1 - x0))) (
-                                                                        Rabs (x1 - x0) * eps) H1); unfold Rminus at 2 in |- *;
+                                                                        Rabs (x1 - x0) * eps) H1); unfold Rminus at 2;
                                                                     rewrite (Rplus_comm (Rabs (f x1 - f x0)) (- Rabs (d x0 * (x1 - x0))));
                                                                       rewrite <-
                                                                         (Rplus_assoc (Rabs (d x0 * (x1 - x0))) (- Rabs (d x0 * (x1 - x0)))
@@ -162,7 +162,7 @@ Proof.
       (Rplus_lt_compat (Rabs (d x0 * (x1 - x0))) (eps * / 2)
         (Rabs (x1 - x0) * eps) (eps * / 2) H5 H3); intro;
       rewrite eps2 in H10; assumption.
-  unfold Rabs in |- *; case (Rcase_abs 2); auto.
+  unfold Rabs; case (Rcase_abs 2); auto.
   intro; cut (0 < 2).
   intro ; elim (Rlt_asym 0 2 H7 r).
   fourier.
@@ -174,14 +174,14 @@ Qed.
 Lemma Dconst :
   forall (D:R -> Prop) (y x0:R), D_in (fun x:R => y) (fun x:R => 0) D x0.
 Proof.
-  unfold D_in in |- *; intros; unfold limit1_in in |- *;
-    unfold limit_in in |- *; unfold Rdiv in |- *; intros;
-      simpl in |- *; split with eps; split; auto.
-  intros; rewrite (Rminus_diag_eq y y (refl_equal y)); rewrite Rmult_0_l;
-    unfold R_dist in |- *; rewrite (Rminus_diag_eq 0 0 (refl_equal 0));
-      unfold Rabs in |- *; case (Rcase_abs 0); intro.
+  unfold D_in; intros; unfold limit1_in;
+    unfold limit_in; unfold Rdiv; intros;
+      simpl; split with eps; split; auto.
+  intros; rewrite (Rminus_diag_eq y y (eq_refl y)); rewrite Rmult_0_l;
+    unfold R_dist; rewrite (Rminus_diag_eq 0 0 (eq_refl 0));
+      unfold Rabs; case (Rcase_abs 0); intro.
   absurd (0 < 0); auto.
-  red in |- *; intro; apply (Rlt_irrefl 0 H1).
+  red; intro; apply (Rlt_irrefl 0 H1).
   unfold Rgt in H0; assumption.
 Qed.
 
@@ -189,15 +189,15 @@ Qed.
 Lemma Dx :
   forall (D:R -> Prop) (x0:R), D_in (fun x:R => x) (fun x:R => 1) D x0.
 Proof.
-  unfold D_in in |- *; unfold Rdiv in |- *; intros; unfold limit1_in in |- *;
-    unfold limit_in in |- *; intros; simpl in |- *; split with eps;
+  unfold D_in; unfold Rdiv; intros; unfold limit1_in;
+    unfold limit_in; intros; simpl; split with eps;
       split; auto.
   intros; elim H0; clear H0; intros; unfold D_x in H0; elim H0; intros;
-    rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (sym_not_eq H3)));
-      unfold R_dist in |- *; rewrite (Rminus_diag_eq 1 1 (refl_equal 1));
-        unfold Rabs in |- *; case (Rcase_abs 0); intro.
+    rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (not_eq_sym H3)));
+      unfold R_dist; rewrite (Rminus_diag_eq 1 1 (eq_refl 1));
+        unfold Rabs; case (Rcase_abs 0); intro.
   absurd (0 < 0); auto.
-  red in |- *; intro; apply (Rlt_irrefl 0 r).
+  red; intro; apply (Rlt_irrefl 0 r).
   unfold Rgt in H; assumption.
 Qed.
 
@@ -208,12 +208,12 @@ Lemma Dadd :
     D_in g dg D x0 ->
     D_in (fun x:R => f x + g x) (fun x:R => df x + dg x) D x0.
 Proof.
-  unfold D_in in |- *; intros;
+  unfold D_in; intros;
     generalize
       (limit_plus (fun x:R => (f x - f x0) * / (x - x0))
         (fun x:R => (g x - g x0) * / (x - x0)) (D_x D x0) (
-          df x0) (dg x0) x0 H H0); clear H H0; unfold limit1_in in |- *;
-      unfold limit_in in |- *; simpl in |- *; intros; elim (H eps H0);
+          df x0) (dg x0) x0 H H0); clear H H0; unfold limit1_in;
+      unfold limit_in; simpl; intros; elim (H eps H0);
         clear H; intros; elim H; clear H; intros; split with x;
           split; auto; intros; generalize (H1 x1 H2); clear H1;
             intro; rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0))) in H1;
@@ -233,8 +233,8 @@ Lemma Dmult :
     D_in g dg D x0 ->
     D_in (fun x:R => f x * g x) (fun x:R => df x * g x + f x * dg x) D x0.
 Proof.
-  intros; unfold D_in in |- *; generalize H H0; intros; unfold D_in in H, H0;
-    generalize (cont_deriv f df D x0 H1); unfold continue_in in |- *;
+  intros; unfold D_in; generalize H H0; intros; unfold D_in in H, H0;
+    generalize (cont_deriv f df D x0 H1); unfold continue_in;
       intro;
         generalize
           (limit_mul (fun x:R => (g x - g x0) * / (x - x0)) (
@@ -250,8 +250,8 @@ Proof.
             (fun x:R => (g x - g x0) * / (x - x0) * f x) (
               D_x D x0) (df x0 * g x0) (dg x0 * f x0) x0 H H4);
           clear H4 H; intro; unfold limit1_in in H; unfold limit_in in H;
-            simpl in H; unfold limit1_in in |- *; unfold limit_in in |- *;
-              simpl in |- *; intros; elim (H eps H0); clear H; intros;
+            simpl in H; unfold limit1_in; unfold limit_in;
+              simpl; intros; elim (H eps H0); clear H; intros;
                 elim H; clear H; intros; split with x; split; auto;
                   intros; generalize (H1 x1 H2); clear H1; intro;
                     rewrite (Rmult_comm (f x1 - f x0) (/ (x1 - x0))) in H1;
@@ -268,9 +268,9 @@ Proof.
                                     ((f x1 - f x0) * g x0 + (g x1 - g x0) * f x1 = f x1 * g x1 - f x0 * g x0).
   intro; rewrite H3 in H1; assumption.
   ring.
-  unfold limit1_in in |- *; unfold limit_in in |- *; simpl in |- *; intros;
+  unfold limit1_in; unfold limit_in; simpl; intros;
     split with eps; split; auto; intros; elim (R_dist_refl (g x0) (g x0));
-      intros a b; rewrite (b (refl_equal (g x0))); unfold Rgt in H;
+      intros a b; rewrite (b (eq_refl (g x0))); unfold Rgt in H;
         assumption.
 Qed.
 
@@ -281,7 +281,7 @@ Lemma Dmult_const :
 Proof.
   intros;
     generalize (Dmult D (fun _:R => 0) df (fun _:R => a) f x0 (Dconst D a x0) H);
-      unfold D_in in |- *; intros; rewrite (Rmult_0_l (f x0)) in H0;
+      unfold D_in; intros; rewrite (Rmult_0_l (f x0)) in H0;
         rewrite (let (H1, H2) := Rplus_ne (a * df x0) in H2) in H0;
           assumption.
 Qed.
@@ -291,10 +291,10 @@ Lemma Dopp :
   forall (D:R -> Prop) (f df:R -> R) (x0:R),
     D_in f df D x0 -> D_in (fun x:R => - f x) (fun x:R => - df x) D x0.
 Proof.
-  intros; generalize (Dmult_const D f df x0 (-1) H); unfold D_in in |- *;
-    unfold limit1_in in |- *; unfold limit_in in |- *;
+  intros; generalize (Dmult_const D f df x0 (-1) H); unfold D_in;
+    unfold limit1_in; unfold limit_in;
       intros; generalize (H0 eps H1); clear H0; intro; elim H0;
-        clear H0; intros; elim H0; clear H0; simpl in |- *;
+        clear H0; intros; elim H0; clear H0; simpl;
           intros; split with x; split; auto.
   intros; generalize (H2 x1 H3); clear H2; intro;
     rewrite Ropp_mult_distr_l_reverse in H2;
@@ -313,7 +313,7 @@ Lemma Dminus :
     D_in g dg D x0 ->
     D_in (fun x:R => f x - g x) (fun x:R => df x - dg x) D x0.
 Proof.
-  unfold Rminus in |- *; intros; generalize (Dopp D g dg x0 H0); intro;
+  unfold Rminus; intros; generalize (Dopp D g dg x0 H0); intro;
     apply (Dadd D df (fun x:R => - dg x) f (fun x:R => - g x) x0);
       assumption.
 Qed.
@@ -324,14 +324,14 @@ Lemma Dx_pow_n :
     D_in (fun x:R => x ^ n) (fun x:R => INR n * x ^ (n - 1)) D x0.
 Proof.
   simple induction n; intros.
-  simpl in |- *; rewrite Rmult_0_l; apply Dconst.
+  simpl; rewrite Rmult_0_l; apply Dconst.
   intros; cut (n0 = (S n0 - 1)%nat);
-    [ intro a; rewrite <- a; clear a | simpl in |- *; apply minus_n_O ].
+    [ intro a; rewrite <- a; clear a | simpl; apply minus_n_O ].
   generalize
     (Dmult D (fun _:R => 1) (fun x:R => INR n0 * x ^ (n0 - 1)) (
       fun x:R => x) (fun x:R => x ^ n0) x0 (Dx D x0) (
-        H D x0)); unfold D_in in |- *; unfold limit1_in in |- *;
-    unfold limit_in in |- *; simpl in |- *; intros; elim (H0 eps H1);
+        H D x0)); unfold D_in; unfold limit1_in;
+    unfold limit_in; simpl; intros; elim (H0 eps H1);
       clear H0; intros; elim H0; clear H0; intros; split with x;
         split; auto.
   intros; generalize (H2 x1 H3); clear H2 H3; intro;
@@ -340,7 +340,7 @@ Proof.
         rewrite (Rmult_comm (INR n0) (x0 ^ (n0 - 1))) in H2;
           rewrite <- (Rmult_assoc x0 (x0 ^ (n0 - 1)) (INR n0)) in H2;
             rewrite (tech_pow_Rmult x0 (n0 - 1)) in H2; elim (Peano_dec.eq_nat_dec n0 0) ; intros cond.
-  rewrite cond in H2; rewrite cond; simpl in H2; simpl in |- *;
+  rewrite cond in H2; rewrite cond; simpl in H2; simpl;
     cut (1 + x0 * 1 * 0 = 1 * 1);
       [ intro A; rewrite A in H2; assumption | ring ].
   cut (n0 <> 0%nat -> S (n0 - 1) = n0); [ intro | omega ];
@@ -355,8 +355,8 @@ Lemma Dcomp :
     D_in g dg Dg (f x0) ->
     D_in (fun x:R => g (f x)) (fun x:R => df x * dg (f x)) (Dgf Df Dg f) x0.
 Proof.
-  intros Df Dg df dg f g x0 H H0; generalize H H0; unfold D_in in |- *;
-    unfold Rdiv in |- *; intros;
+  intros Df Dg df dg f g x0 H H0; generalize H H0; unfold D_in;
+    unfold Rdiv; intros;
       generalize
         (limit_comp f (fun x:R => (g x - g (f x0)) * / (x - f x0)) (
           D_x Df x0) (D_x Dg (f x0)) (f x0) (dg (f x0)) x0);
@@ -376,8 +376,8 @@ Proof.
       (limit_mul (fun x:R => (f x - f x0) * / (x - x0)) (
         fun x:R => dg (f x0)) (D_x Df x0) (df x0) (dg (f x0)) x0 H1
       (limit_free (fun x:R => dg (f x0)) (D_x Df x0) x0 x0));
-      intro; unfold limit1_in in |- *; unfold limit_in in |- *;
-        simpl in |- *; unfold limit1_in in H5, H7; unfold limit_in in H5, H7;
+      intro; unfold limit1_in; unfold limit_in;
+        simpl; unfold limit1_in in H5, H7; unfold limit_in in H5, H7;
           simpl in H5, H7; intros; elim (H5 eps H8); elim (H7 eps H8);
             clear H5 H7; intros; elim H5; elim H7; clear H5 H7;
               intros; split with (Rmin x x1); split.
@@ -391,7 +391,7 @@ Proof.
       rewrite (Rminus_diag_eq (f x2) (f x0) H12) in H16;
         rewrite (Rmult_0_l (/ (x2 - x0))) in H16;
           rewrite (Rmult_0_l (dg (f x0))) in H16; rewrite H12;
-            rewrite (Rminus_diag_eq (g (f x0)) (g (f x0)) (refl_equal (g (f x0))));
+            rewrite (Rminus_diag_eq (g (f x0)) (g (f x0)) (eq_refl (g (f x0))));
               rewrite (Rmult_0_l (/ (x2 - x0))); assumption.
   clear H10 H5; elim H11; clear H11; intros; elim H5; clear H5; intros;
     cut
@@ -405,8 +405,8 @@ Proof.
               in H15; rewrite (Rinv_l (f x2 - f x0) H16) in H15;
                 rewrite (let (H1, H2) := Rmult_ne (/ (x2 - x0)) in H2) in H15;
                   rewrite (Rmult_comm (df x0) (dg (f x0))); assumption.
-  clear H5 H3 H4 H2; unfold limit1_in in |- *; unfold limit_in in |- *;
-    simpl in |- *; unfold limit1_in in H1; unfold limit_in in H1;
+  clear H5 H3 H4 H2; unfold limit1_in; unfold limit_in;
+    simpl; unfold limit1_in in H1; unfold limit_in in H1;
       simpl in H1; intros; elim (H1 eps H2); clear H1; intros;
         elim H1; clear H1; intros; split with x; split; auto;
           intros; unfold D_x, Dgf in H4, H3; elim H4; clear H4;
@@ -425,8 +425,8 @@ Proof.
     generalize
       (Dcomp D D dexpr (fun x:R => INR n * x ^ (n - 1)) expr (
         fun x:R => x ^ n) x0 H (Dx_pow_n n D (expr x0)));
-      intro; unfold D_in in |- *; unfold limit1_in in |- *;
-        unfold limit_in in |- *; simpl in |- *; intros; unfold D_in in H0;
+      intro; unfold D_in; unfold limit1_in;
+        unfold limit_in; simpl; intros; unfold D_in in H0;
           unfold limit1_in in H0; unfold limit_in in H0; simpl in H0;
             elim (H0 eps H1); clear H0; intros; elim H0; clear H0;
               intros; split with x; split; intros; auto.