diff options
author | 2002-07-16 10:05:25 +0000 | |
---|---|---|
committer | 2002-07-16 10:05:25 +0000 | |
commit | bf014271e07872d855a6704f66981e108ae2e654 (patch) | |
tree | 0d09ba91742390a6e6385c428c019618c8510cf3 /theories/Reals | |
parent | 2b4201841c437ef86659eda7e1d1555eea39e626 (diff) |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2883 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals')
-rw-r--r-- | theories/Reals/Rtrigo.v | 169 | ||||
-rw-r--r-- | theories/Reals/Rtrigo_calc.v | 170 |
2 files changed, 170 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 *) (***************************************************) diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 0bcb76d1f..af6c6d59e 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -15,6 +15,129 @@ Require Rlimit. Require Rtrigo. Require R_sqrt. +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 tan_2PI : ``(tan (2*PI))==0``. +Unfold tan; Rewrite sin_2PI; Unfold Rdiv; Apply Rmult_Ol. +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 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. @@ -314,4 +437,51 @@ Qed. Lemma sin_cos5PI4 : ``(cos (5*(PI/4)))==(sin (5*(PI/4)))``. Rewrite cos_5PI4; Rewrite sin_5PI4; 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.
\ No newline at end of file |