diff options
Diffstat (limited to 'theories/Reals/Rtrigo_calc.v')
| -rw-r--r-- | theories/Reals/Rtrigo_calc.v | 112 |
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. |