diff options
Diffstat (limited to 'theories/Reals/Rtrigo_calc.v')
| -rw-r--r-- | theories/Reals/Rtrigo_calc.v | 578 |
1 files changed, 303 insertions, 275 deletions
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index f8c15667..baf0fa4b 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Rtrigo_calc.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Rtrigo_calc.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Rbase. Require Import Rfunctions. @@ -16,365 +16,388 @@ Require Import R_sqrt. Open Local Scope R_scope. Lemma tan_PI : tan PI = 0. -unfold tan in |- *; rewrite sin_PI; rewrite cos_PI; unfold Rdiv in |- *; - apply Rmult_0_l. +Proof. + unfold tan in |- *; rewrite sin_PI; rewrite cos_PI; unfold Rdiv in |- *; + apply Rmult_0_l. 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 PI at 1 in |- *; rewrite (double_var PI); ring. +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. Qed. Lemma tan_2PI : tan (2 * PI) = 0. -unfold tan in |- *; rewrite sin_2PI; unfold Rdiv in |- *; apply Rmult_0_l. +Proof. + unfold tan in |- *; rewrite sin_2PI; unfold Rdiv in |- *; apply Rmult_0_l. Qed. Lemma sin_cos_PI4 : sin (PI / 4) = cos (PI / 4). Proof with trivial. -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 PI at 2 3 in |- *; rewrite H; pattern PI at 2 3 in |- *; rewrite H... -assert (H0 : 2 <> 0); - [ discrR | unfold Rdiv in |- *; rewrite Rinv_mult_distr; try ring ]... + 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 PI at 2 3 in |- *; rewrite H; pattern PI at 2 3 in |- *; rewrite H... + assert (H0 : 2 <> 0); + [ discrR | unfold Rdiv in |- *; rewrite Rinv_mult_distr; try ring ]... Qed. Lemma sin_PI3_cos_PI6 : sin (PI / 3) = cos (PI / 6). Proof with trivial. -replace (PI / 6) with (PI / 2 - PI / 3)... -rewrite cos_shift... -assert (H0 : 6 <> 0); [ discrR | idtac ]... -assert (H1 : 3 <> 0); [ discrR | idtac ]... -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... -rewrite <- Rinv_l_sym... -rewrite (Rmult_comm (/ 3)); repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym... -pattern PI at 2 in |- *; rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r; - repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym... -ring... + replace (PI / 6) with (PI / 2 - PI / 3)... + rewrite cos_shift... + assert (H0 : 6 <> 0); [ discrR | idtac ]... + assert (H1 : 3 <> 0); [ discrR | idtac ]... + 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... + rewrite <- Rinv_l_sym... + rewrite (Rmult_comm (/ 3)); repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym... + pattern PI at 2 in |- *; rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r; + repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym... + ring... Qed. Lemma sin_PI6_cos_PI3 : cos (PI / 3) = sin (PI / 6). Proof with trivial. -replace (PI / 6) with (PI / 2 - PI / 3)... -rewrite sin_shift... -assert (H0 : 6 <> 0); [ discrR | idtac ]... -assert (H1 : 3 <> 0); [ discrR | idtac ]... -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... -rewrite <- Rinv_l_sym... -rewrite (Rmult_comm (/ 3)); repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym... -pattern PI at 2 in |- *; rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r; - repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym... -ring... + replace (PI / 6) with (PI / 2 - PI / 3)... + rewrite sin_shift... + assert (H0 : 6 <> 0); [ discrR | idtac ]... + assert (H1 : 3 <> 0); [ discrR | idtac ]... + 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... + rewrite <- Rinv_l_sym... + rewrite (Rmult_comm (/ 3)); repeat rewrite Rmult_assoc; rewrite <- Rinv_r_sym... + pattern PI at 2 in |- *; rewrite (Rmult_comm PI); repeat rewrite Rmult_1_r; + repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym... + ring... Qed. Lemma PI6_RGT_0 : 0 < PI / 6. -unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ]. +Proof. + unfold Rdiv in |- *; 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. -unfold Rdiv in |- *; apply Rmult_lt_compat_l. -apply PI_RGT_0. -apply Rinv_lt_contravar; prove_sup. +Proof. + unfold Rdiv in |- *; apply Rmult_lt_compat_l. + apply PI_RGT_0. + apply Rinv_lt_contravar; prove_sup. Qed. Lemma sin_PI6 : sin (PI / 6) = 1 / 2. Proof with trivial. -assert (H : 2 <> 0); [ discrR | idtac ]... -apply Rmult_eq_reg_l 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 in |- *; rewrite Rmult_1_l; rewrite Rmult_assoc; - pattern 2 at 2 in |- *; rewrite (Rmult_comm 2); rewrite Rmult_assoc; - rewrite <- Rinv_l_sym... -rewrite Rmult_1_r... -unfold Rdiv in |- *; rewrite Rinv_mult_distr... -rewrite (Rmult_comm (/ 2)); rewrite (Rmult_comm 2); - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... -rewrite Rmult_1_r... -discrR... -ring... -apply prod_neq_R0... -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 ] ]... + assert (H : 2 <> 0); [ discrR | idtac ]... + apply Rmult_eq_reg_l 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 in |- *; rewrite Rmult_1_l; rewrite Rmult_assoc; + pattern 2 at 2 in |- *; rewrite (Rmult_comm 2); rewrite Rmult_assoc; + rewrite <- Rinv_l_sym... + rewrite Rmult_1_r... + unfold Rdiv in |- *; rewrite Rinv_mult_distr... + rewrite (Rmult_comm (/ 2)); rewrite (Rmult_comm 2); + repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... + rewrite Rmult_1_r... + discrR... + ring... + apply prod_neq_R0... + 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. -assert (Hyp : 0 < 2); - [ prove_sup0 - | generalize (Rlt_le 0 2 Hyp); intro H1; red in |- *; intro H2; - generalize (sqrt_eq_0 2 H1 H2); intro H; absurd (2 = 0); - [ discrR | assumption ] ]. +Proof. + assert (Hyp : 0 < 2); + [ prove_sup0 + | generalize (Rlt_le 0 2 Hyp); intro H1; red in |- *; 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_0_compat (sqrt 2) sqrt2_neq_0); intro H; - generalize (prod_neq_R0 1 (/ sqrt 2) R1_neq_R0 H); - intro H0; assumption. +Proof. + generalize (Rinv_neq_0_compat (sqrt 2) sqrt2_neq_0); intro H; + generalize (prod_neq_R0 1 (/ sqrt 2) R1_neq_R0 H); + intro H0; assumption. Qed. Lemma sqrt3_2_neq_0 : 2 * sqrt 3 <> 0. -apply prod_neq_R0; - [ discrR - | assert (Hyp : 0 < 3); - [ prove_sup0 - | generalize (Rlt_le 0 3 Hyp); intro H1; red in |- *; intro H2; - generalize (sqrt_eq_0 3 H1 H2); intro H; absurd (3 = 0); - [ discrR | assumption ] ] ]. +Proof. + apply prod_neq_R0; + [ discrR + | assert (Hyp : 0 < 3); + [ prove_sup0 + | generalize (Rlt_le 0 3 Hyp); intro H1; red in |- *; intro H2; + generalize (sqrt_eq_0 3 H1 H2); intro H; absurd (3 = 0); + [ discrR | assumption ] ] ]. Qed. Lemma Rlt_sqrt2_0 : 0 < sqrt 2. -assert (Hyp : 0 < 2); - [ prove_sup0 - | generalize (sqrt_positivity 2 (Rlt_le 0 2 Hyp)); intro H1; elim H1; - intro H2; - [ assumption - | absurd (0 = sqrt 2); - [ apply (sym_not_eq (A:=R)); apply sqrt2_neq_0 | assumption ] ] ]. +Proof. + assert (Hyp : 0 < 2); + [ prove_sup0 + | generalize (sqrt_positivity 2 (Rlt_le 0 2 Hyp)); intro H1; elim H1; + intro H2; + [ assumption + | absurd (0 = sqrt 2); + [ apply (sym_not_eq (A:=R)); apply sqrt2_neq_0 | assumption ] ] ]. Qed. Lemma Rlt_sqrt3_0 : 0 < sqrt 3. -cut (0%nat <> 1%nat); - [ intro H0; assert (Hyp : 0 < 2); - [ prove_sup0 - | generalize (Rlt_le 0 2 Hyp); intro H1; assert (Hyp2 : 0 < 3); - [ 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; - 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; - apply (Rlt_trans 0 (sqrt 2) (sqrt 3) Rlt_sqrt2_0 H3) - | ring ] ] ] - | discriminate ]. +Proof. + cut (0%nat <> 1%nat); + [ intro H0; assert (Hyp : 0 < 2); + [ prove_sup0 + | generalize (Rlt_le 0 2 Hyp); intro H1; assert (Hyp2 : 0 < 3); + [ 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; + 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; + apply (Rlt_trans 0 (sqrt 2) (sqrt 3) Rlt_sqrt2_0 H3) + | ring ] ] ] + | discriminate ]. Qed. Lemma PI4_RGT_0 : 0 < PI / 4. -unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ]. +Proof. + unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ]. Qed. Lemma cos_PI4 : cos (PI / 4) = 1 / sqrt 2. Proof with trivial. -apply Rsqr_inj... -apply cos_ge_0... -left; apply (Rlt_trans (- (PI / 2)) 0 (PI / 4) _PI2_RLT_0 PI4_RGT_0)... -left; apply PI4_RLT_PI2... -left; apply (Rmult_lt_0_compat 1 (/ sqrt 2))... -prove_sup... -apply Rinv_0_lt_compat; apply Rlt_sqrt2_0... -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 |- *; - 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... -repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... -rewrite Rmult_1_r... -unfold Rdiv in |- *; rewrite Rmult_1_l; repeat rewrite <- Rmult_assoc... -rewrite <- Rinv_l_sym... -rewrite Rmult_1_l... -left; prove_sup... -apply sqrt2_neq_0... + apply Rsqr_inj... + apply cos_ge_0... + left; apply (Rlt_trans (- (PI / 2)) 0 (PI / 4) _PI2_RLT_0 PI4_RGT_0)... + left; apply PI4_RLT_PI2... + left; apply (Rmult_lt_0_compat 1 (/ sqrt 2))... + prove_sup... + apply Rinv_0_lt_compat; apply Rlt_sqrt2_0... + 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 |- *; + 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... + repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... + rewrite Rmult_1_r... + unfold Rdiv in |- *; rewrite Rmult_1_l; repeat rewrite <- Rmult_assoc... + rewrite <- Rinv_l_sym... + rewrite Rmult_1_l... + left; prove_sup... + apply sqrt2_neq_0... Qed. Lemma sin_PI4 : sin (PI / 4) = 1 / sqrt 2. -rewrite sin_cos_PI4; apply cos_PI4. +Proof. + rewrite sin_cos_PI4; apply cos_PI4. Qed. Lemma tan_PI4 : tan (PI / 4) = 1. -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. +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. 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; - repeat rewrite Rmult_assoc; rewrite <- Rinv_mult_distr; - [ ring | discrR | discrR ]... + 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; + repeat rewrite Rmult_assoc; rewrite <- Rinv_mult_distr; + [ ring | discrR | discrR ]... Qed. 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; - repeat rewrite Rmult_assoc; rewrite <- Rinv_mult_distr; - [ ring | discrR | discrR ]... + 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; + repeat rewrite Rmult_assoc; rewrite <- Rinv_mult_distr; + [ ring | discrR | discrR ]... Qed. Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2. Proof with trivial. -apply Rsqr_inj... -apply cos_ge_0... -left; apply (Rlt_trans (- (PI / 2)) 0 (PI / 6) _PI2_RLT_0 PI6_RGT_0)... -left; apply PI6_RLT_PI2... -left; apply (Rmult_lt_0_compat (sqrt 3) (/ 2))... -apply Rlt_sqrt3_0... -apply Rinv_0_lt_compat; prove_sup0... -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 Rmult_minus_distr_l; rewrite (Rmult_comm 3); - repeat rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym... -rewrite Rmult_1_l; rewrite Rmult_1_r... -rewrite <- (Rmult_comm (/ 2)); repeat rewrite <- Rmult_assoc... -rewrite <- Rinv_l_sym... -rewrite Rmult_1_l; rewrite <- Rinv_r_sym... -ring... -left; prove_sup0... + apply Rsqr_inj... + apply cos_ge_0... + left; apply (Rlt_trans (- (PI / 2)) 0 (PI / 6) _PI2_RLT_0 PI6_RGT_0)... + left; apply PI6_RLT_PI2... + left; apply (Rmult_lt_0_compat (sqrt 3) (/ 2))... + apply Rlt_sqrt3_0... + apply Rinv_0_lt_compat; prove_sup0... + 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 Rmult_minus_distr_l; rewrite (Rmult_comm 3); + repeat rewrite <- Rmult_assoc; rewrite <- Rinv_r_sym... + rewrite Rmult_1_l; rewrite Rmult_1_r... + rewrite <- (Rmult_comm (/ 2)); repeat rewrite <- Rmult_assoc... + rewrite <- Rinv_l_sym... + rewrite Rmult_1_l; rewrite <- Rinv_r_sym... + ring... + left; prove_sup0... Qed. Lemma tan_PI6 : tan (PI / 6) = 1 / sqrt 3. -unfold tan in |- *; rewrite sin_PI6; rewrite cos_PI6; unfold Rdiv in |- *; - 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; - elim (Rlt_irrefl 0 H1). -apply Rinv_neq_0_compat; discrR. +Proof. + unfold tan in |- *; rewrite sin_PI6; rewrite cos_PI6; unfold Rdiv in |- *; + 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; + elim (Rlt_irrefl 0 H1). + apply Rinv_neq_0_compat; discrR. Qed. Lemma sin_PI3 : sin (PI / 3) = sqrt 3 / 2. -rewrite sin_PI3_cos_PI6; apply cos_PI6. +Proof. + 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. +Proof. + rewrite sin_PI6_cos_PI3; apply sin_PI6. Qed. Lemma tan_PI3 : tan (PI / 3) = sqrt 3. -unfold tan in |- *; rewrite sin_PI3; rewrite cos_PI3; unfold Rdiv in |- *; - rewrite Rmult_1_l; rewrite Rinv_involutive. -rewrite Rmult_assoc; rewrite <- Rinv_l_sym. -apply Rmult_1_r. -discrR. -discrR. +Proof. + unfold tan in |- *; rewrite sin_PI3; rewrite cos_PI3; unfold Rdiv in |- *; + rewrite Rmult_1_l; rewrite Rinv_involutive. + rewrite Rmult_assoc; rewrite <- Rinv_l_sym. + apply Rmult_1_r. + discrR. + discrR. Qed. Lemma sin_2PI3 : sin (2 * (PI / 3)) = sqrt 3 / 2. -rewrite double; rewrite sin_plus; rewrite sin_PI3; rewrite cos_PI3; - unfold Rdiv in |- *; repeat rewrite Rmult_1_l; rewrite (Rmult_comm (/ 2)); - repeat rewrite <- Rmult_assoc; rewrite double_var; - reflexivity. +Proof. + rewrite double; rewrite sin_plus; rewrite sin_PI3; rewrite cos_PI3; + unfold Rdiv in |- *; repeat rewrite Rmult_1_l; rewrite (Rmult_comm (/ 2)); + repeat rewrite <- Rmult_assoc; rewrite double_var; + reflexivity. Qed. Lemma cos_2PI3 : cos (2 * (PI / 3)) = -1 / 2. 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... -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; - 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... -rewrite Rmult_1_r; rewrite (Rmult_comm 2); rewrite (Rmult_comm (/ 2))... -repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... -rewrite Rmult_1_r; rewrite sqrt_def... -ring... -left; prove_sup... + 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... + 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; + 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... + rewrite Rmult_1_r; rewrite (Rmult_comm 2); rewrite (Rmult_comm (/ 2))... + repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... + rewrite Rmult_1_r; rewrite sqrt_def... + ring... + left; prove_sup... 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 |- *; - rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l; - rewrite <- Ropp_inv_permute... -rewrite Rinv_involutive... -rewrite Rmult_assoc; rewrite Ropp_mult_distr_r_reverse; rewrite <- Rinv_l_sym... -ring... -apply Rinv_neq_0_compat... + assert (H : 2 <> 0); [ discrR | idtac ]... + unfold tan in |- *; rewrite sin_2PI3; rewrite cos_2PI3; unfold Rdiv in |- *; + rewrite Ropp_mult_distr_l_reverse; rewrite Rmult_1_l; + rewrite <- Ropp_inv_permute... + rewrite Rinv_involutive... + rewrite Rmult_assoc; rewrite Ropp_mult_distr_r_reverse; rewrite <- Rinv_l_sym... + ring... + apply Rinv_neq_0_compat... 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 Ropp_mult_distr_l_reverse... -pattern PI at 2 in |- *; rewrite double_var; pattern PI at 2 3 in |- *; - rewrite double_var; assert (H : 2 <> 0); - [ discrR | unfold Rdiv in |- *; repeat rewrite Rinv_mult_distr; try ring ]... + replace (5 * (PI / 4)) with (PI / 4 + PI)... + rewrite neg_cos; rewrite cos_PI4; unfold Rdiv in |- *; + rewrite Ropp_mult_distr_l_reverse... + pattern PI at 2 in |- *; rewrite double_var; pattern PI at 2 3 in |- *; + rewrite double_var; assert (H : 2 <> 0); + [ discrR | unfold Rdiv in |- *; 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 Ropp_mult_distr_l_reverse... -pattern PI at 2 in |- *; rewrite double_var; pattern PI at 2 3 in |- *; - rewrite double_var; assert (H : 2 <> 0); - [ discrR | unfold Rdiv in |- *; repeat rewrite Rinv_mult_distr; try ring ]... + replace (5 * (PI / 4)) with (PI / 4 + PI)... + rewrite neg_sin; rewrite sin_PI4; unfold Rdiv in |- *; + rewrite Ropp_mult_distr_l_reverse... + pattern PI at 2 in |- *; rewrite double_var; pattern PI at 2 3 in |- *; + rewrite double_var; assert (H : 2 <> 0); + [ discrR | unfold Rdiv in |- *; repeat rewrite Rinv_mult_distr; try ring ]... Qed. Lemma sin_cos5PI4 : cos (5 * (PI / 4)) = sin (5 * (PI / 4)). -rewrite cos_5PI4; rewrite sin_5PI4; reflexivity. +Proof. + rewrite cos_5PI4; rewrite sin_5PI4; reflexivity. Qed. Lemma Rgt_3PI2_0 : 0 < 3 * (PI / 2). -apply Rmult_lt_0_compat; - [ prove_sup0 - | unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ] ]. +Proof. + apply Rmult_lt_0_compat; + [ prove_sup0 + | unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup0 ] ]. Qed. Lemma Rgt_2PI_0 : 0 < 2 * PI. -apply Rmult_lt_0_compat; [ prove_sup0 | apply PI_RGT_0 ]. +Proof. + apply Rmult_lt_0_compat; [ prove_sup0 | apply PI_RGT_0 ]. Qed. Lemma Rlt_PI_3PI2 : PI < 3 * (PI / 2). -generalize PI2_RGT_0; intro H1; - 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. +Proof. + generalize PI2_RGT_0; intro H1; + 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. Qed. - + Lemma Rlt_3PI2_2PI : 3 * (PI / 2) < 2 * PI. -generalize PI2_RGT_0; intro H1; - 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. +Proof. + generalize PI2_RGT_0; intro H1; + 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. Qed. (***************************************************************) -(* Radian -> Degree | Degree -> Radian *) +(** Radian -> Degree | Degree -> Radian *) (***************************************************************) Definition plat : R := 180. @@ -382,27 +405,30 @@ Definition toRad (x:R) : R := x * PI * / plat. Definition toDeg (x:R) : R := x * plat * / PI. Lemma rad_deg : forall x:R, toRad (toDeg x) = x. -intro; unfold toRad, toDeg in |- *; - 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. +Proof. + intro; unfold toRad, toDeg in |- *; + 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. Qed. Lemma toRad_inj : forall x y:R, toRad x = toRad y -> x = y. -intros; unfold toRad in H; apply Rmult_eq_reg_l with PI. -rewrite <- (Rmult_comm x); rewrite <- (Rmult_comm y). -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 PI_neq0. +Proof. + intros; unfold toRad in H; apply Rmult_eq_reg_l with PI. + rewrite <- (Rmult_comm x); rewrite <- (Rmult_comm y). + 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 PI_neq0. Qed. Lemma deg_rad : forall x:R, toDeg (toRad x) = x. -intro x; apply toRad_inj; rewrite (rad_deg (toRad x)); reflexivity. +Proof. + intro x; apply toRad_inj; rewrite (rad_deg (toRad x)); reflexivity. Qed. Definition sind (x:R) : R := sin (toRad x). @@ -410,25 +436,27 @@ Definition cosd (x:R) : R := cos (toRad x). Definition tand (x:R) : R := tan (toRad x). Lemma Rsqr_sin_cos_d_one : forall x:R, Rsqr (sind x) + Rsqr (cosd x) = 1. -intro x; unfold sind in |- *; unfold cosd in |- *; apply sin2_cos2. +Proof. + intro x; unfold sind in |- *; unfold cosd in |- *; apply sin2_cos2. Qed. (***************************************************) -(* Other properties *) +(** Other properties *) (***************************************************) Lemma sin_lb_ge_0 : forall a:R, 0 <= a -> a <= PI / 2 -> 0 <= sin_lb a. -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 |- *; - repeat rewrite pow_ne_zero. -unfold Rdiv in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; - repeat rewrite Rplus_0_r; right; reflexivity. -discriminate. -discriminate. -discriminate. -discriminate. -elim (Rlt_irrefl 0 (Rle_lt_trans 0 a 0 H H2)). -Qed.
\ No newline at end of file +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 |- *; + repeat rewrite pow_ne_zero. + unfold Rdiv in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; + repeat rewrite Rplus_0_r; right; reflexivity. + discriminate. + discriminate. + discriminate. + discriminate. + elim (Rlt_irrefl 0 (Rle_lt_trans 0 a 0 H H2)). +Qed. |