Imported Upstream version 8.4dfsgupstream/8.4dfsg

1 files changed, 56 insertions, 56 deletions

diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index 587c2424..a1a3b007 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.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,13 +9,13 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
-Require Import Rtrigo.
+Require Import Rtrigo1.
 Require Import R_sqrt.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Lemma tan_PI : tan PI = 0.
 Proof.
-  unfold tan in |- *; rewrite sin_PI; rewrite cos_PI; unfold Rdiv in |- *;
+  unfold tan; rewrite sin_PI; rewrite cos_PI; unfold Rdiv;
     apply Rmult_0_l.
 Qed.
 
@@ -23,12 +23,12 @@ Lemma sin_3PI2 : sin (3 * (PI / 2)) = -1.
 Proof.
   replace (3 * (PI / 2)) with (PI + PI / 2).
   rewrite sin_plus; rewrite sin_PI; rewrite cos_PI; rewrite sin_PI2; ring.
-  pattern PI at 1 in |- *; rewrite (double_var PI); ring.
+  pattern PI at 1; rewrite (double_var PI); ring.
 Qed.
 
 Lemma tan_2PI : tan (2 * PI) = 0.
 Proof.
-  unfold tan in |- *; rewrite sin_2PI; unfold Rdiv in |- *; apply Rmult_0_l.
+  unfold tan; rewrite sin_2PI; unfold Rdiv; apply Rmult_0_l.
 Qed.
 
 Lemma sin_cos_PI4 : sin (PI / 4) = cos (PI / 4).
@@ -37,9 +37,9 @@ Proof with trivial.
   replace (PI / 2 + PI / 4) with (- (PI / 4) + PI)...
   rewrite neg_sin; rewrite sin_neg; ring...
   cut (PI = PI / 2 + PI / 2); [ intro | apply double_var ]...
-  pattern PI at 2 3 in |- *; rewrite H; pattern PI at 2 3 in |- *; rewrite H...
+  pattern PI at 2 3; rewrite H; pattern PI at 2 3; rewrite H...
   assert (H0 : 2 <> 0);
-    [ discrR | unfold Rdiv in |- *; rewrite Rinv_mult_distr; try ring ]...
+    [ discrR | unfold Rdiv; rewrite Rinv_mult_distr; try ring ]...
 Qed.
 
 Lemma sin_PI3_cos_PI6 : sin (PI / 3) = cos (PI / 6).
@@ -51,7 +51,7 @@ Proof with trivial.
   assert (H2 : 2 <> 0); [ discrR | idtac ]...
   apply Rmult_eq_reg_l with 6...
   rewrite Rmult_minus_distr_l; repeat rewrite (Rmult_comm 6)...
-  unfold Rdiv in |- *; repeat rewrite Rmult_assoc...
+  unfold Rdiv; repeat rewrite Rmult_assoc...
   rewrite <- Rinv_l_sym...
   rewrite (Rmult_comm (/ 3)); repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym...
   rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r;
@@ -68,7 +68,7 @@ Proof with trivial.
   assert (H2 : 2 <> 0); [ discrR | idtac ]...
   apply Rmult_eq_reg_l with 6...
   rewrite Rmult_minus_distr_l; repeat rewrite (Rmult_comm 6)...
-  unfold Rdiv in |- *; repeat rewrite Rmult_assoc...
+  unfold Rdiv; repeat rewrite Rmult_assoc...
   rewrite <- Rinv_l_sym...
   rewrite (Rmult_comm (/ 3)); repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym...
   rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r;
@@ -78,13 +78,13 @@ Qed.
 
 Lemma PI6_RGT_0 : 0 < PI / 6.
 Proof.
-  unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+  unfold Rdiv; apply Rmult_lt_0_compat;
     [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ].
 Qed.
 
 Lemma PI6_RLT_PI2 : PI / 6 < PI / 2.
 Proof.
-  unfold Rdiv in |- *; apply Rmult_lt_compat_l.
+  unfold Rdiv; apply Rmult_lt_compat_l.
   apply PI_RGT_0.
   apply Rinv_lt_contravar; prove_sup.
 Qed.
@@ -97,11 +97,11 @@ Proof with trivial.
   (2 * sin (PI / 6) * cos (PI / 6))...
   rewrite <- sin_2a; replace (2 * (PI / 6)) with (PI / 3)...
   rewrite sin_PI3_cos_PI6...
-  unfold Rdiv in |- *; rewrite Rmult_1_l; rewrite Rmult_assoc;
-    pattern 2 at 2 in |- *; rewrite (Rmult_comm 2); rewrite Rmult_assoc;
+  unfold Rdiv; rewrite Rmult_1_l; rewrite Rmult_assoc;
+    pattern 2 at 2; rewrite (Rmult_comm 2); rewrite Rmult_assoc;
       rewrite <- Rinv_l_sym...
   rewrite Rmult_1_r...
-  unfold Rdiv in |- *; rewrite Rinv_mult_distr...
+  unfold Rdiv; rewrite Rinv_mult_distr...
   rewrite (Rmult_comm (/ 2)); rewrite (Rmult_comm 2);
     repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym...
   rewrite Rmult_1_r...
@@ -119,7 +119,7 @@ Lemma sqrt2_neq_0 : sqrt 2 <> 0.
 Proof.
   assert (Hyp : 0 < 2);
     [ prove_sup0
-      | generalize (Rlt_le 0 2 Hyp); intro H1; red in |- *; intro H2;
+      | generalize (Rlt_le 0 2 Hyp); intro H1; red; intro H2;
         generalize (sqrt_eq_0 2 H1 H2); intro H; absurd (2 = 0);
           [ discrR | assumption ] ].
 Qed.
@@ -137,7 +137,7 @@ Proof.
     [ discrR
       | assert (Hyp : 0 < 3);
         [ prove_sup0
-          | generalize (Rlt_le 0 3 Hyp); intro H1; red in |- *; intro H2;
+          | generalize (Rlt_le 0 3 Hyp); intro H1; red; intro H2;
             generalize (sqrt_eq_0 3 H1 H2); intro H; absurd (3 = 0);
               [ discrR | assumption ] ] ].
 Qed.
@@ -150,7 +150,7 @@ Proof.
         intro H2;
           [ assumption
             | absurd (0 = sqrt 2);
-              [ apply (sym_not_eq (A:=R)); apply sqrt2_neq_0 | assumption ] ] ].
+              [ apply (not_eq_sym (A:=R)); apply sqrt2_neq_0 | assumption ] ] ].
 Qed.
 
 Lemma Rlt_sqrt3_0 : 0 < sqrt 3.
@@ -162,7 +162,7 @@ Proof.
           [ prove_sup0
             | generalize (Rlt_le 0 3 Hyp2); intro H2;
               generalize (lt_INR_0 1 (neq_O_lt 1 H0));
-                unfold INR in |- *; intro H3;
+                unfold INR; intro H3;
                   generalize (Rplus_lt_compat_l 2 0 1 H3);
                     rewrite Rplus_comm; rewrite Rplus_0_l; replace (2 + 1) with 3;
                       [ intro H4; generalize (sqrt_lt_1 2 3 H1 H2 H4); clear H3; intro H3;
@@ -173,7 +173,7 @@ Qed.
 
 Lemma PI4_RGT_0 : 0 < PI / 4.
 Proof.
-  unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+  unfold Rdiv; apply Rmult_lt_0_compat;
     [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ].
 Qed.
 
@@ -189,17 +189,17 @@ Proof with trivial.
   rewrite Rsqr_div...
   rewrite Rsqr_1; rewrite Rsqr_sqrt...
   assert (H : 2 <> 0); [ discrR | idtac ]...
-  unfold Rsqr in |- *; pattern (cos (PI / 4)) at 1 in |- *;
+  unfold Rsqr; pattern (cos (PI / 4)) at 1;
     rewrite <- sin_cos_PI4;
       replace (sin (PI / 4) * cos (PI / 4)) with
       (1 / 2 * (2 * sin (PI / 4) * cos (PI / 4)))...
   rewrite <- sin_2a; replace (2 * (PI / 4)) with (PI / 2)...
   rewrite sin_PI2...
   apply Rmult_1_r...
-  unfold Rdiv in |- *; rewrite (Rmult_comm 2); rewrite Rinv_mult_distr...
+  unfold Rdiv; rewrite (Rmult_comm 2); rewrite Rinv_mult_distr...
   repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym...
   rewrite Rmult_1_r...
-  unfold Rdiv in |- *; rewrite Rmult_1_l; repeat rewrite <- Rmult_assoc...
+  unfold Rdiv; rewrite Rmult_1_l; repeat rewrite <- Rmult_assoc...
   rewrite <- Rinv_l_sym...
   rewrite Rmult_1_l...
   left; prove_sup...
@@ -213,18 +213,18 @@ Qed.
 
 Lemma tan_PI4 : tan (PI / 4) = 1.
 Proof.
-  unfold tan in |- *; rewrite sin_cos_PI4.
-  unfold Rdiv in |- *; apply Rinv_r.
-  change (cos (PI / 4) <> 0) in |- *; rewrite cos_PI4; apply R1_sqrt2_neq_0.
+  unfold tan; rewrite sin_cos_PI4.
+  unfold Rdiv; apply Rinv_r.
+  change (cos (PI / 4) <> 0); rewrite cos_PI4; apply R1_sqrt2_neq_0.
 Qed.
 
 Lemma cos3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2.
 Proof with trivial.
   replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4))...
   rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4...
-  unfold Rdiv in |- *; rewrite Ropp_mult_distr_l_reverse...
-  unfold Rminus in |- *; rewrite Ropp_involutive; pattern PI at 1 in |- *;
-    rewrite double_var; unfold Rdiv in |- *; rewrite Rmult_plus_distr_r;
+  unfold Rdiv; rewrite Ropp_mult_distr_l_reverse...
+  unfold Rminus; rewrite Ropp_involutive; pattern PI at 1;
+    rewrite double_var; unfold Rdiv; rewrite Rmult_plus_distr_r;
       repeat rewrite Rmult_assoc; rewrite <- Rinv_mult_distr;
         [ ring | discrR | discrR ]...
 Qed.
@@ -233,8 +233,8 @@ Lemma sin3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2.
 Proof with trivial.
   replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4))...
   rewrite sin_shift; rewrite cos_neg; rewrite cos_PI4...
-  unfold Rminus in |- *; rewrite Ropp_involutive; pattern PI at 1 in |- *;
-    rewrite double_var; unfold Rdiv in |- *; rewrite Rmult_plus_distr_r;
+  unfold Rminus; rewrite Ropp_involutive; pattern PI at 1;
+    rewrite double_var; unfold Rdiv; rewrite Rmult_plus_distr_r;
       repeat rewrite Rmult_assoc; rewrite <- Rinv_mult_distr;
         [ ring | discrR | discrR ]...
 Qed.
@@ -251,8 +251,8 @@ Proof with trivial.
   assert (H : 2 <> 0); [ discrR | idtac ]...
   assert (H1 : 4 <> 0); [ apply prod_neq_R0 | idtac ]...
   rewrite Rsqr_div...
-  rewrite cos2; unfold Rsqr in |- *; rewrite sin_PI6; rewrite sqrt_def...
-  unfold Rdiv in |- *; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 4...
+  rewrite cos2; unfold Rsqr; rewrite sin_PI6; rewrite sqrt_def...
+  unfold Rdiv; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 4...
   rewrite Rmult_minus_distr_l; rewrite (Rmult_comm 3);
     repeat rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym...
   rewrite Rmult_1_l; rewrite Rmult_1_r...
@@ -265,14 +265,14 @@ Qed.
 
 Lemma tan_PI6 : tan (PI / 6) = 1 / sqrt 3.
 Proof.
-  unfold tan in |- *; rewrite sin_PI6; rewrite cos_PI6; unfold Rdiv in |- *;
+  unfold tan; rewrite sin_PI6; rewrite cos_PI6; unfold Rdiv;
     repeat rewrite Rmult_1_l; rewrite Rinv_mult_distr.
   rewrite Rinv_involutive.
   rewrite (Rmult_comm (/ 2)); rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
   apply Rmult_1_r.
   discrR.
   discrR.
-  red in |- *; intro; assert (H1 := Rlt_sqrt3_0); rewrite H in H1;
+  red; intro; assert (H1 := Rlt_sqrt3_0); rewrite H in H1;
     elim (Rlt_irrefl 0 H1).
   apply Rinv_neq_0_compat; discrR.
 Qed.
@@ -289,7 +289,7 @@ Qed.
 
 Lemma tan_PI3 : tan (PI / 3) = sqrt 3.
 Proof.
-  unfold tan in |- *; rewrite sin_PI3; rewrite cos_PI3; unfold Rdiv in |- *;
+  unfold tan; rewrite sin_PI3; rewrite cos_PI3; unfold Rdiv;
     rewrite Rmult_1_l; rewrite Rinv_involutive.
   rewrite Rmult_assoc; rewrite <- Rinv_l_sym.
   apply Rmult_1_r.
@@ -300,7 +300,7 @@ Qed.
 Lemma sin_2PI3 : sin (2 * (PI / 3)) = sqrt 3 / 2.
 Proof.
   rewrite double; rewrite sin_plus; rewrite sin_PI3; rewrite cos_PI3;
-    unfold Rdiv in |- *; repeat rewrite Rmult_1_l; rewrite (Rmult_comm (/ 2));
+    unfold Rdiv; repeat rewrite Rmult_1_l; rewrite (Rmult_comm (/ 2));
       repeat rewrite <- Rmult_assoc; rewrite double_var;
         reflexivity.
 Qed.
@@ -310,12 +310,12 @@ Proof with trivial.
   assert (H : 2 <> 0); [ discrR | idtac ]...
   assert (H0 : 4 <> 0); [ apply prod_neq_R0 | idtac ]...
   rewrite double; rewrite cos_plus; rewrite sin_PI3; rewrite cos_PI3;
-    unfold Rdiv in |- *; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 4...
+    unfold Rdiv; rewrite Rmult_1_l; apply Rmult_eq_reg_l with 4...
   rewrite Rmult_minus_distr_l; repeat rewrite Rmult_assoc;
     rewrite (Rmult_comm 2)...
   repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym...
   rewrite Rmult_1_r; rewrite <- Rinv_r_sym...
-  pattern 2 at 4 in |- *; rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc;
+  pattern 2 at 4; rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc;
     rewrite <- Rinv_l_sym...
   rewrite Rmult_1_r; rewrite Ropp_mult_distr_r_reverse; rewrite Rmult_1_r...
   rewrite (Rmult_comm 2); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym...
@@ -329,7 +329,7 @@ Qed.
 Lemma tan_2PI3 : tan (2 * (PI / 3)) = - sqrt 3.
 Proof with trivial.
   assert (H : 2 <> 0); [ discrR | idtac ]...
-  unfold tan in |- *; rewrite sin_2PI3; rewrite cos_2PI3; unfold Rdiv in |- *;
+  unfold tan; rewrite sin_2PI3; rewrite cos_2PI3; unfold Rdiv;
     rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l;
       rewrite <- Ropp_inv_permute...
   rewrite Rinv_involutive...
@@ -341,21 +341,21 @@ Qed.
 Lemma cos_5PI4 : cos (5 * (PI / 4)) = -1 / sqrt 2.
 Proof with trivial.
   replace (5 * (PI / 4)) with (PI / 4 + PI)...
-  rewrite neg_cos; rewrite cos_PI4; unfold Rdiv in |- *;
+  rewrite neg_cos; rewrite cos_PI4; unfold Rdiv;
     rewrite Ropp_mult_distr_l_reverse...
-  pattern PI at 2 in |- *; rewrite double_var; pattern PI at 2 3 in |- *;
+  pattern PI at 2; rewrite double_var; pattern PI at 2 3;
     rewrite double_var; assert (H : 2 <> 0);
-      [ discrR | unfold Rdiv in |- *; repeat rewrite Rinv_mult_distr; try ring ]...
+      [ discrR | unfold Rdiv; repeat rewrite Rinv_mult_distr; try ring ]...
 Qed.
 
 Lemma sin_5PI4 : sin (5 * (PI / 4)) = -1 / sqrt 2.
 Proof with trivial.
   replace (5 * (PI / 4)) with (PI / 4 + PI)...
-  rewrite neg_sin; rewrite sin_PI4; unfold Rdiv in |- *;
+  rewrite neg_sin; rewrite sin_PI4; unfold Rdiv;
     rewrite Ropp_mult_distr_l_reverse...
-  pattern PI at 2 in |- *; rewrite double_var; pattern PI at 2 3 in |- *;
+  pattern PI at 2; rewrite double_var; pattern PI at 2 3;
     rewrite double_var; assert (H : 2 <> 0);
-      [ discrR | unfold Rdiv in |- *; repeat rewrite Rinv_mult_distr; try ring ]...
+      [ discrR | unfold Rdiv; repeat rewrite Rinv_mult_distr; try ring ]...
 Qed.
 
 Lemma sin_cos5PI4 : cos (5 * (PI / 4)) = sin (5 * (PI / 4)).
@@ -367,7 +367,7 @@ Lemma Rgt_3PI2_0 : 0 < 3 * (PI / 2).
 Proof.
   apply Rmult_lt_0_compat;
     [ prove_sup0
-      | unfold Rdiv in |- *; apply Rmult_lt_0_compat;
+      | unfold Rdiv; apply Rmult_lt_0_compat;
         [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ] ].
 Qed.
 
@@ -382,7 +382,7 @@ Proof.
     generalize (Rplus_lt_compat_l PI 0 (PI / 2) H1);
       replace (PI + PI / 2) with (3 * (PI / 2)).
   rewrite Rplus_0_r; intro H2; assumption.
-  pattern PI at 2 in |- *; rewrite double_var; ring.
+  pattern PI at 2; rewrite double_var; ring.
 Qed.
 
 Lemma Rlt_3PI2_2PI : 3 * (PI / 2) < 2 * PI.
@@ -391,7 +391,7 @@ Proof.
     generalize (Rplus_lt_compat_l (3 * (PI / 2)) 0 (PI / 2) H1);
       replace (3 * (PI / 2) + PI / 2) with (2 * PI).
   rewrite Rplus_0_r; intro H2; assumption.
-  rewrite double; pattern PI at 1 2 in |- *; rewrite double_var; ring.
+  rewrite double; pattern PI at 1 2; rewrite double_var; ring.
 Qed.
 
 (***************************************************************)
@@ -404,13 +404,13 @@ Definition toDeg (x:R) : R := x * plat * / PI.
 
 Lemma rad_deg : forall x:R, toRad (toDeg x) = x.
 Proof.
-  intro; unfold toRad, toDeg in |- *;
+  intro; unfold toRad, toDeg;
     replace (x * plat * / PI * PI * / plat) with
     (x * (plat * / plat) * (PI * / PI)); [ idtac | ring ].
   repeat rewrite <- Rinv_r_sym.
   ring.
   apply PI_neq0.
-  unfold plat in |- *; discrR.
+  unfold plat; discrR.
 Qed.
 
 Lemma toRad_inj : forall x y:R, toRad x = toRad y -> x = y.
@@ -420,7 +420,7 @@ Proof.
   apply Rmult_eq_reg_l with (/ plat).
   rewrite <- (Rmult_comm (x * PI)); rewrite <- (Rmult_comm (y * PI));
     assumption.
-  apply Rinv_neq_0_compat; unfold plat in |- *; discrR.
+  apply Rinv_neq_0_compat; unfold plat; discrR.
   apply PI_neq0.
 Qed.
 
@@ -435,7 +435,7 @@ Definition tand (x:R) : R := tan (toRad x).
 
 Lemma Rsqr_sin_cos_d_one : forall x:R, Rsqr (sind x) + Rsqr (cosd x) = 1.
 Proof.
-  intro x; unfold sind in |- *; unfold cosd in |- *; apply sin2_cos2.
+  intro x; unfold sind; unfold cosd; apply sin2_cos2.
 Qed.
 
 (***************************************************)
@@ -447,10 +447,10 @@ Proof.
   intros; case (Rtotal_order 0 a); intro.
   left; apply sin_lb_gt_0; assumption.
   elim H1; intro.
-  rewrite <- H2; unfold sin_lb in |- *; unfold sin_approx in |- *;
-    unfold sum_f_R0 in |- *; unfold sin_term in |- *;
+  rewrite <- H2; unfold sin_lb; unfold sin_approx;
+    unfold sum_f_R0; unfold sin_term;
       repeat rewrite pow_ne_zero.
-  unfold Rdiv in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r;
+  unfold Rdiv; repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r;
     repeat rewrite Rplus_0_r; right; reflexivity.
   discriminate.
   discriminate.