diff options
author | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-16 09:00:58 +0000 |
---|---|---|
committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-07-16 09:00:58 +0000 |
commit | 6526cd438bf12926805ffcb6415154082bae61d9 (patch) | |
tree | 40233fdfe3c53c362a5dfdbd2a1c9164afca9980 /theories/Reals/Rtrigo_calc.v | |
parent | a30878bdb78071ce183d90bb16e37fa68e0122bd (diff) |
Proprietes (calculatoires) des fonctions trigonometriques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2875 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_calc.v')
-rw-r--r-- | theories/Reals/Rtrigo_calc.v | 317 |
1 files changed, 317 insertions, 0 deletions
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v new file mode 100644 index 000000000..0bcb76d1f --- /dev/null +++ b/theories/Reals/Rtrigo_calc.v @@ -0,0 +1,317 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +Require Rbase. +Require DiscrR. +Require R_sqr. +Require Rlimit. +Require Rtrigo. +Require R_sqrt. + +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 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. +DiscrR. +DiscrR. +DiscrR. +Ring. +Unfold Rdiv. +Rewrite Rmult_1l. +Repeat Rewrite <- Rmult_assoc. +Rewrite <- Rinv_l_sym. +Rewrite Rmult_1l. +Reflexivity. +DiscrR. +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 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 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 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.
\ No newline at end of file |