diff options
author | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-16 09:03:02 +0000 |
---|---|---|
committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-16 09:03:02 +0000 |
commit | 7f8807d77df6d8e4605b26fbdb9075b5de5fc768 (patch) | |
tree | a3a962d6852eca10854d687bd3b248b9298c6ee0 /theories/Reals/Rtrigo.v | |
parent | 1e558a3ce46468154c719eba3f6812be23ab49d7 (diff) |
MAJ Rtrigo pour sqrt
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2880 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo.v')
-rw-r--r-- | theories/Reals/Rtrigo.v | 301 |
1 files changed, 0 insertions, 301 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 92accec1c..f22ce994e 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -419,26 +419,6 @@ Pattern 1 ``2``; Rewrite <- Rplus_Or. Replace ``6`` with ``2+4``; [Apply Rlt_compatibility; Sup0 | Ring]. Qed. -Lemma sqrt2_neq_0 : ~``(sqrt 2)==0``. -Generalize (Rlt_le ``0`` ``2`` Rgt_2_0); Intro H1; Red; Intro H2; Generalize (sqrt_eq_0 ``2`` H1 H2); Intro H; Absurd ``2==0``; [ DiscrR | Assumption]. -Qed. - -Lemma R1_sqrt2_neq_0 : ~``1/(sqrt 2)==0``. -Generalize (Rinv_neq_R0 ``(sqrt 2)`` sqrt2_neq_0); Intro H; Generalize (prod_neq_R0 ``1`` ``(Rinv (sqrt 2))`` R1_neq_R0 H); Intro H0; Assumption. -Qed. - -Lemma sqrt3_2_neq_0 : ~``2*(sqrt 3)==0``. -Apply prod_neq_R0; [DiscrR | Generalize (Rlt_le ``0`` ``3`` Rgt_3_0); Intro H1; Red; Intro H2; Generalize (sqrt_eq_0 ``3`` H1 H2); Intro H; Absurd ``3==0``; [ DiscrR | Assumption]]. -Qed. - -Lemma Rlt_sqrt2_0 : ``0<(sqrt 2)``. -Generalize (sqrt_positivity ``2`` (Rlt_le ``0`` ``2`` Rgt_2_0)); Intro H1; Elim H1; Intro H2; [Assumption | Absurd ``0 == (sqrt 2)``; [Apply not_sym; Apply sqrt2_neq_0 | Assumption]]. -Qed. - -Lemma Rlt_sqrt3_0 : ``0<(sqrt 3)``. -Cut ~(O=(1)); [Intro H0; Generalize (Rlt_le ``0`` ``2`` Rgt_2_0); Intro H1; Generalize (Rlt_le ``0`` ``3`` Rgt_3_0); Intro H2; Generalize (lt_INR_0 (1) (neq_O_lt (1) H0)); Unfold INR; Intro H3; Generalize (Rlt_compatibility ``2`` ``0`` ``1`` H3); Rewrite Rplus_sym; Rewrite Rplus_Ol; Replace ``2+1`` with ``3``; [Intro H4; Generalize (sqrt_lt_1 ``2`` ``3`` H1 H2 H4); Clear H3; Intro H3; Apply (Rlt_trans ``0`` ``(sqrt 2)`` ``(sqrt 3)`` Rlt_sqrt2_0 H3) | Ring] | Discriminate]. -Qed. - Lemma PI2_Rlt_PI : ``PI/2<PI``. Unfold Rdiv; Pattern 2 PI; Rewrite <- Rmult_1r. Apply Rlt_monotony. @@ -950,94 +930,6 @@ Rewrite <- Rinv_Rmult; [Rewrite H0; Ring | Apply aze | Apply aze]. Ring. Qed. -Lemma cos_PI4 : ``(cos (PI/4))==1/(sqrt 2)``. -Apply Rsqr_inj. -Apply cos_ge_0. -Left; Apply (Rlt_trans ``-(PI/2)`` R0 ``PI/4`` _PI2_RLT_0 PI4_RGT_0). -Left; Apply PI4_RLT_PI2. -Left; Apply (Rmult_lt_pos R1 ``(Rinv (sqrt 2))``). -Apply Rlt_R0_R1. -Apply Rlt_Rinv. -Apply Rlt_sqrt2_0. -Rewrite Rsqr_div. -Rewrite Rsqr_1; Rewrite Rsqr_sqrt. -Unfold Rsqr; Pattern 1 ``(cos (PI/4))``; 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_1r. -Unfold Rdiv. -Rewrite (Rmult_sym ``2``). -Replace ``4`` with ``2*2``. -Rewrite Rinv_Rmult. -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r. -Reflexivity. -Apply aze. -Apply aze. -Apply aze. -Ring. -Unfold Rdiv. -Rewrite Rmult_1l. -Repeat Rewrite <- Rmult_assoc. -Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l. -Reflexivity. -Apply aze. -Left; Apply Rgt_2_0. -Apply sqrt2_neq_0. -Qed. - -Lemma sin_PI4 : ``(sin (PI/4))==1/(sqrt 2)``. -Rewrite sin_cos_PI4; Apply cos_PI4. -Qed. - -Lemma cos3PI4 : ``(cos (3*(PI/4)))==-1/(sqrt 2)``. -Replace ``3*(PI/4)`` with ``(PI/2)-(-(PI/4))``. -Rewrite cos_shift; Rewrite sin_neg; Rewrite sin_PI4. -Unfold Rdiv. -Rewrite Ropp_mul1. -Reflexivity. -Unfold Rminus. -Rewrite Ropp_Ropp. -Pattern 1 PI; Rewrite double_var. -Unfold Rdiv. -Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_Rmult. -Replace ``2*2`` with ``4``. -Ring. -Ring. -Apply aze. -Apply aze. -Qed. - -Lemma sin3PI4 : ``(sin (3*(PI/4)))==1/(sqrt 2)``. -Replace ``3*(PI/4)`` with ``(PI/2)-(-(PI/4))``. -Rewrite sin_shift; Rewrite cos_neg; Rewrite cos_PI4; Reflexivity. -Unfold Rminus. -Rewrite Ropp_Ropp. -Pattern 1 PI; Rewrite double_var. -Unfold Rdiv. -Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_Rmult. -Replace ``2*2`` with ``4``. -Ring. -Ring. -Apply aze. -Apply aze. -Qed. - -Lemma tan_PI4 : ``(tan (PI/4))==1``. -Unfold tan; Rewrite sin_cos_PI4. -Unfold Rdiv. -Apply Rinv_r. -Replace ``PI*/4`` with ``PI/4``. -Rewrite cos_PI4; Apply R1_sqrt2_neq_0. -Unfold Rdiv; Reflexivity. -Qed. - Lemma sin_PI3_cos_PI6 : ``(sin (PI/3))==(cos (PI/6))``. Replace ``PI/6`` with ``(PI/2)-(PI/3)``. Rewrite cos_shift; Reflexivity. @@ -1130,199 +1022,6 @@ 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 cos_PI6 : ``(cos (PI/6))==(sqrt 3)/2``. -Apply Rsqr_inj. -Apply cos_ge_0. -Left; Apply (Rlt_trans ``-(PI/2)`` R0 ``PI/6`` _PI2_RLT_0 PI6_RGT_0). -Left; Apply PI6_RLT_PI2. -Left; Apply (Rmult_lt_pos ``(sqrt 3)`` ``(Rinv 2)``). -Apply Rlt_sqrt3_0. -Apply Rlt_Rinv; Apply Rgt_2_0. -Rewrite Rsqr_div. -Rewrite cos2; Unfold Rsqr; Rewrite sin_PI6; Rewrite sqrt_def. -Unfold Rdiv. -Rewrite Rmult_1l. -Rewrite <- Rinv_Rmult. -Replace ``2*2`` with ``4``. -Apply r_Rmult_mult with ``4``. -Unfold Rminus. -Rewrite Rmult_Rplus_distr. -Rewrite Rmult_1r. -Rewrite Ropp_mul3. -Rewrite <- Rinv_r_sym. -Rewrite (Rmult_sym ``3``). -Rewrite <- Rmult_assoc. -Rewrite <- Rinv_r_sym. -Rewrite Rmult_1l. -Ring. -DiscrR. -DiscrR. -DiscrR. -Ring. -Apply aze. -Apply aze. -Left; Apply Rgt_3_0. -Apply aze. -Qed. - -Lemma tan_PI6 : ``(tan (PI/6))==1/(sqrt 3)``. -Unfold tan; Rewrite sin_PI6; Rewrite cos_PI6. -Unfold Rdiv. -Repeat Rewrite Rmult_1l. -Rewrite Rinv_Rmult. -Rewrite Rinv_Rinv. -Rewrite (Rmult_sym ``/2``). -Rewrite Rmult_assoc. -Rewrite <- Rinv_r_sym. -Apply Rmult_1r. -Apply aze. -Apply aze. -Red; Intro. -Assert H1 := Rlt_sqrt3_0. -Rewrite H in H1; Elim (Rlt_antirefl ``0`` H1). -Apply Rinv_neq_R0. -Apply aze. -Qed. - -Lemma sin_PI3 : ``(sin (PI/3))==(sqrt 3)/2``. -Rewrite sin_PI3_cos_PI6; Apply cos_PI6. -Qed. - -Lemma cos_PI3 : ``(cos (PI/3))==1/2``. -Rewrite sin_PI6_cos_PI3; Apply sin_PI6. -Qed. - -Lemma tan_PI3 : ``(tan (PI/3))==(sqrt 3)``. -Unfold tan; Rewrite sin_PI3; Rewrite cos_PI3. -Unfold Rdiv. -Rewrite Rmult_1l. -Rewrite Rinv_Rinv. -Rewrite Rmult_assoc. -Rewrite <- Rinv_l_sym. -Apply Rmult_1r. -Apply aze. -Apply aze. -Qed. - -Lemma sin_2PI3 : ``(sin (2*(PI/3)))==(sqrt 3)/2``. -Rewrite double. -Rewrite sin_plus; Rewrite sin_PI3; Rewrite cos_PI3. -Unfold Rdiv. -Repeat Rewrite Rmult_1l. -Rewrite (Rmult_sym ``/2``). -Pattern 3 ``(sqrt 3)``; Rewrite double_var. -Rewrite Rmult_Rplus_distrl. -Unfold Rdiv. -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_Rmult. -Replace ``2*2`` with ``4``. -Reflexivity. -Ring. -Apply aze. -Apply aze. -Qed. - -Lemma cos_2PI3 : ``(cos (2*(PI/3)))==-1/2``. -Rewrite double. -Rewrite cos_plus; Rewrite sin_PI3; Rewrite cos_PI3. -Unfold Rdiv. -Rewrite Rmult_1l. -Apply r_Rmult_mult with ``2*2``. -Rewrite Rminus_distr. -Repeat Rewrite Rmult_assoc. -Rewrite (Rmult_sym ``2``). -Repeat Rewrite Rmult_assoc. -Rewrite <- (Rinv_l_sym). -Rewrite Rmult_1r. -Rewrite <- Rinv_r_sym. -Pattern 4 ``2``; Rewrite (Rmult_sym ``2``). -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r. -Rewrite Ropp_mul3. -Rewrite Rmult_1r. -Rewrite (Rmult_sym ``2``). -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r. -Rewrite (Rmult_sym ``2``). -Rewrite (Rmult_sym ``/2``). -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r. -Rewrite sqrt_def. -Ring. -Replace ``3`` with ``(INR (S (S (S O))))`` . -Apply pos_INR. -Rewrite INR_eq_INR2. -Reflexivity. -Apply aze. -Apply aze. -Apply aze. -Apply aze. -Apply aze. -Apply prod_neq_R0; Apply aze. -Qed. - -Lemma tan_2PI3 : ``(tan (2*(PI/3)))==-(sqrt 3)``. -Unfold tan; Rewrite sin_2PI3; Rewrite cos_2PI3. -Unfold Rdiv. -Rewrite Rinv_Rmult. -Rewrite Rinv_Rinv. -Repeat Rewrite Rmult_assoc. -Rewrite (Rmult_sym ``/2``). -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r. -Rewrite <- Ropp_Rinv. -Rewrite Ropp_mul3. -Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity. -DiscrR. -Apply aze. -Apply aze. -DiscrR. -Apply Rinv_neq_R0; Apply aze. -Qed. - -Lemma cos_5PI4 : ``(cos (5*(PI/4)))==-1/(sqrt 2)``. -Replace ``5*(PI/4)`` with ``(PI/4)+(PI)``. -Rewrite neg_cos; Rewrite cos_PI4. -Unfold Rdiv. -Symmetry; Apply Ropp_mul1. -Pattern 2 PI; Rewrite double_var. -Pattern 2 3 PI; Rewrite double_var. -Unfold Rdiv. -Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_Rmult. -Replace ``2*2`` with ``4``. -Ring. -Ring. -Apply aze. -Apply aze. -Qed. - -Lemma sin_5PI4 : ``(sin (5*(PI/4)))==-1/(sqrt 2)``. -Replace ``5*(PI/4)`` with ``(PI/4)+(PI)``. -Rewrite neg_sin; Rewrite sin_PI4. -Unfold Rdiv; Symmetry; Apply Ropp_mul1. -Pattern 2 PI; Rewrite double_var. -Pattern 2 3 PI; Rewrite double_var. -Unfold Rdiv. -Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_Rmult. -Replace ``2*2`` with ``4``. -Ring. -Ring. -Apply aze. -Apply aze. -Qed. - -Lemma sin_cos5PI4 : ``(cos (5*(PI/4)))==(sin (5*(PI/4)))``. -Rewrite cos_5PI4; Rewrite sin_5PI4; Reflexivity. -Qed. - Lemma sin_eq_0_1 : (x:R) (EXT k:Z | x==(Rmult (IZR k) PI)) -> (sin x)==R0. Intros. Elim H; Intros. |