*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2883 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 169 deletions

diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index f22ce994e..6ef075502 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -227,18 +227,6 @@ Assumption.
 Rewrite tan_neg; Unfold Rminus; Rewrite <- Ropp_mul1; Rewrite Ropp_mul2; Assumption.
 Qed.
 
-Lemma tan_PI : ``(tan PI)==0``.
-Unfold tan; Rewrite -> sin_PI; Rewrite -> cos_PI.
-Unfold Rdiv; Apply Rmult_Ol. 
-Qed.
-
-Lemma sin_3PI2 : ``(sin (3*(PI/2)))==(-1)``.
-Replace ``3*(PI/2)`` with ``PI+(PI/2)``.
-Rewrite -> sin_plus; Rewrite -> sin_PI; Rewrite -> cos_PI; Rewrite -> sin_PI2; Ring.
-Pattern 1 PI; Rewrite (double_var PI).
-Ring.
-Qed.
-
 Lemma cos_3PI2 : ``(cos (3*(PI/2)))==0``.
 Replace ``3*(PI/2)`` with ``PI+(PI/2)``.
 Rewrite -> cos_plus; Rewrite -> sin_PI; Rewrite -> cos_PI2; Ring.
@@ -254,10 +242,6 @@ Lemma cos_2PI : ``(cos (2*PI))==1``.
 Rewrite -> cos_2a; Rewrite -> sin_PI; Rewrite -> cos_PI; Ring.
 Qed.
 
-Lemma tan_2PI : ``(tan (2*PI))==0``.
-Unfold tan; Rewrite sin_2PI; Unfold Rdiv; Apply Rmult_Ol.
-Qed.
-
 Lemma neg_sin : (x:R) ``(sin (x+PI))==-(sin x)``.
 Intro x; Rewrite -> sin_plus; Rewrite -> sin_PI; Rewrite -> cos_PI; Ring.
 Qed.
@@ -916,112 +900,6 @@ Rewrite Rplus_Or; Intro H2; Assumption.
 Rewrite double; Pattern 1 2 PI; Rewrite double_var; Ring.
 Qed.
 
-Lemma sin_cos_PI4 : ``(sin (PI/4)) == (cos (PI/4))``.
-Rewrite cos_sin.
-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 2 3 PI; Rewrite H.
-Pattern 2 3 PI; Rewrite H.
-Unfold Rdiv; Cut ``2*2==4``.
-Intro; Rewrite Rmult_Rplus_distrl.
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult; [Rewrite H0; Ring | Apply aze | Apply aze].
-Ring.
-Qed.
-
-Lemma sin_PI3_cos_PI6 : ``(sin (PI/3))==(cos (PI/6))``.
-Replace ``PI/6`` with ``(PI/2)-(PI/3)``.
-Rewrite cos_shift; Reflexivity.
-Pattern 2 PI; Rewrite double_var.
-Cut ``PI == 3*(PI/3)``.
-Intro.
-Pattern 1 PI; Rewrite H.
-Unfold Rdiv.
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult.
-Unfold Rminus.
-Rewrite (Rmult_Rplus_distrl ``PI*/2`` ``PI*/2`` ``/3``).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult.
-Rewrite (Rmult_sym ``2``).
-Replace ``3*2`` with ``6``.
-Rewrite Ropp_distr1.
-Ring.
-Ring.
-Apply aze.
-DiscrR.
-DiscrR.
-Apply aze.
-Unfold Rdiv.
-Rewrite (Rmult_sym ``3``).
-Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Reflexivity.
-DiscrR.
-Qed.
-
-Lemma sin_PI6_cos_PI3 : ``(cos (PI/3))==(sin (PI/6))``.
-Replace ``PI/6`` with ``(PI/2)-(PI/3)``.
-Rewrite sin_shift; Reflexivity.
-Pattern 2 PI; Rewrite double_var.
-Cut ``PI == 3*(PI/3)``.
-Intro.
-Pattern 1 PI; Rewrite H.
-Unfold Rdiv.
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult.
-Unfold Rminus.
-Rewrite (Rmult_Rplus_distrl ``PI*/2`` ``PI*/2`` ``/3``).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_Rmult.
-Rewrite (Rmult_sym ``2``).
-Replace ``3*2`` with ``6``.
-Rewrite Ropp_distr1.
-Ring.
-Ring.
-Apply aze.
-DiscrR.
-DiscrR.
-DiscrR.
-Unfold Rdiv.
-Rewrite (Rmult_sym ``3``).
-Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Reflexivity.
-DiscrR.
-Qed.
-
-Lemma sin_PI6 : ``(sin (PI/6))==1/2``.
-Apply r_Rmult_mult with ``2*(cos (PI/6))``.
-Replace ``2*(cos (PI/6))*(sin (PI/6))`` with ``2*(sin (PI/6))*(cos (PI/6))``.
-Rewrite <- sin_2a; Replace ``2*(PI/6)`` with ``PI/3``.
-Rewrite sin_PI3_cos_PI6.
-Unfold Rdiv. 
-Rewrite Rmult_1l.
-Rewrite Rmult_assoc.
-Rewrite (Rmult_sym ``2``).
-Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r; Reflexivity.
-Apply aze.
-Replace ``6`` with ``2*3``.
-Unfold Rdiv.
-Rewrite Rinv_Rmult.
-Rewrite (Rmult_sym ``/2``).
-Rewrite (Rmult_sym ``2``).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r.
-Reflexivity.
-Apply aze.
-Apply aze.
-DiscrR.
-Ring.
-Ring.
-Apply prod_neq_R0; [DiscrR | Cut ``0<(cos (PI/6))``; [Intro H1; Auto with real | Apply cos_gt_0; [Apply (Rlt_trans ``-(PI/2)`` ``0`` ``PI/6`` _PI2_RLT_0 PI6_RGT_0) | Apply PI6_RLT_PI2]]].
-Qed.
-
 Lemma sin_eq_0_1 : (x:R) (EXT k:Z | x==(Rmult (IZR k) PI)) -> (sin x)==R0.
 Intros.
 Elim H; Intros.
@@ -1302,53 +1180,6 @@ Lemma  cos_eq_0_2PI_1 : (x:R) ``0<=x`` -> ``x<=2*PI`` -> ``x==PI/2``\/``x==3*(PI
 Intros x H1 H2 H3; Elim H3; Intro H4; [ Rewrite H4; Rewrite -> cos_PI2; Reflexivity | Rewrite H4; Rewrite -> cos_3PI2; Reflexivity ].
 Qed.
 
-(***************************************************************)
-(* Radian -> Degree | Degree -> Radian                         *)
-(***************************************************************)
-
-Definition plat : R := (IZR `180`).
-Definition toRad [x:R] : R := ``x*PI*/plat``.
-Definition toDeg [x:R] : R := ``x*plat*/PI``.
-
-Lemma rad_deg : (x:R) (toRad (toDeg x))==x.
-Intro x; Unfold toRad toDeg.
-Rewrite <- (Rmult_sym plat).
-Repeat Rewrite Rmult_assoc.
-Rewrite (Rmult_sym plat).
-Repeat Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym. 
-Rewrite Rmult_1r; Rewrite <- Rinv_l_sym. 
-Apply Rmult_1r.
-Apply PI_neq0.
-Unfold plat.
-Apply not_O_IZR.
-Discriminate.
-Qed.
-
-Lemma toRad_inj : (x,y:R) (toRad x)==(toRad y) -> x==y.
-Intros; Unfold toRad in H; Apply r_Rmult_mult with PI.
-Rewrite <- (Rmult_sym x); Rewrite <- (Rmult_sym y).
-Apply r_Rmult_mult with ``/plat``.
-Rewrite <- (Rmult_sym ``x*PI``); Rewrite <- (Rmult_sym ``y*PI``); Assumption.
-Apply Rinv_neq_R0.
-Unfold plat.
-Apply not_O_IZR.
-Discriminate.
-Apply PI_neq0.
-Qed.
-
-Lemma deg_rad : (x:R) (toDeg (toRad x))==x.
-Intro x; Apply toRad_inj; Rewrite -> (rad_deg (toRad x)); Reflexivity.
-Qed.
-
-Definition sind [x:R] : R := (sin (toRad x)).
-Definition cosd [x:R] : R := (cos (toRad x)).
-Definition tand [x:R] : R := (tan (toRad x)).
-
-Lemma Rsqr_sin_cos_d_one : (x:R) ``(Rsqr (sind x))+(Rsqr (cosd x))==1``.
-Intro x; Unfold sind; Unfold cosd; Apply sin2_cos2.
-Qed.
-
 (***************************************************)
 (*                Other properties                 *)
 (***************************************************)