diff options
Diffstat (limited to 'theories/Reals/Rtrigo_calc.v')
| -rw-r--r-- | theories/Reals/Rtrigo_calc.v | 191 |
1 files changed, 56 insertions, 135 deletions
diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 9ba14ee7..7cbfc630 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Rbase. @@ -32,48 +34,22 @@ Proof. 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; rewrite H; pattern PI at 2 3; rewrite H... - assert (H0 : 2 <> 0); - [ discrR | unfold Rdiv; rewrite Rinv_mult_distr; try ring ]... +Proof. + rewrite cos_sin. + replace (PI / 2 + PI / 4) with (- (PI / 4) + PI) by field. + rewrite neg_sin, sin_neg; 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; 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; - repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym... - ring... +Proof. + replace (PI / 6) with (PI / 2 - PI / 3) by field. + now rewrite cos_shift. 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; 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; - repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym... - ring... +Proof. + replace (PI / 6) with (PI / 2 - PI / 3) by field. + now rewrite sin_shift. Qed. Lemma PI6_RGT_0 : 0 < PI / 6. @@ -90,29 +66,20 @@ Proof. 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))... +Proof. + 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; 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; 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... + (2 * sin (PI / 6) * cos (PI / 6)) by ring. + rewrite <- sin_2a; replace (2 * (PI / 6)) with (PI / 3) by field. + rewrite sin_PI3_cos_PI6. + field. + 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 ] ]... + | apply PI6_RLT_PI2 ] ]. Qed. Lemma sqrt2_neq_0 : sqrt 2 <> 0. @@ -188,20 +155,13 @@ Proof with trivial. 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; 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)... + (1 / 2 * (2 * sin (PI / 4) * cos (PI / 4))) by field. + rewrite <- sin_2a; replace (2 * (PI / 4)) with (PI / 2) by field. rewrite sin_PI2... - apply Rmult_1_r... - unfold Rdiv; rewrite (Rmult_comm 2); rewrite Rinv_mult_distr... - repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym... - rewrite Rmult_1_r... - unfold Rdiv; rewrite Rmult_1_l; repeat rewrite <- Rmult_assoc... - rewrite <- Rinv_l_sym... - rewrite Rmult_1_l... + field. left; prove_sup... apply sqrt2_neq_0... Qed. @@ -219,24 +179,17 @@ Proof. 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; 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 ]... +Proof. + replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. + rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4. + unfold Rdiv. + ring. 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; 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 ]... +Proof. + replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field. + now rewrite sin_shift, cos_neg, cos_PI4. Qed. Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2. @@ -248,19 +201,11 @@ Proof with trivial. 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; 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... - rewrite <- (Rmult_comm (/ 2)); repeat rewrite <- Rmult_assoc... - rewrite <- Rinv_l_sym... - rewrite Rmult_1_l; rewrite <- Rinv_r_sym... - ring... - left; prove_sup0... + field. + left ; prove_sup0. + discrR. Qed. Lemma tan_PI6 : tan (PI / 6) = 1 / sqrt 3. @@ -306,56 +251,32 @@ Proof. 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; 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; 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... +Proof. + rewrite cos_2a, sin_PI3, cos_PI3. + replace (sqrt 3 / 2 * (sqrt 3 / 2)) with ((sqrt 3 * sqrt 3) / 4) by field. + rewrite sqrt_sqrt. + field. + left ; prove_sup0. Qed. Lemma tan_2PI3 : tan (2 * (PI / 3)) = - sqrt 3. -Proof with trivial. - assert (H : 2 <> 0); [ discrR | idtac ]... - 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... - rewrite Rmult_assoc; rewrite Ropp_mult_distr_r_reverse; rewrite <- Rinv_l_sym... - ring... - apply Rinv_neq_0_compat... +Proof. + unfold tan; rewrite sin_2PI3, cos_2PI3. + field. 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; - rewrite Ropp_mult_distr_l_reverse... - pattern PI at 2; rewrite double_var; pattern PI at 2 3; - rewrite double_var; assert (H : 2 <> 0); - [ discrR | unfold Rdiv; repeat rewrite Rinv_mult_distr; try ring ]... +Proof. + replace (5 * (PI / 4)) with (PI / 4 + PI) by field. + rewrite neg_cos; rewrite cos_PI4; unfold Rdiv. + 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; - rewrite Ropp_mult_distr_l_reverse... - pattern PI at 2; rewrite double_var; pattern PI at 2 3; - rewrite double_var; assert (H : 2 <> 0); - [ discrR | unfold Rdiv; repeat rewrite Rinv_mult_distr; try ring ]... +Proof. + replace (5 * (PI / 4)) with (PI / 4 + PI) by field. + rewrite neg_sin; rewrite sin_PI4; unfold Rdiv. + ring. Qed. Lemma sin_cos5PI4 : cos (5 * (PI / 4)) = sin (5 * (PI / 4)). |