diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-11 15:32:59 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-11 15:32:59 +0000 |
| commit | 4dab5938805ec41237b1bdce5efa308e37932cd0 (patch) | |
| tree | 617c1bfabe41e2e99d0dbefe305b170745edf811 /theories/Reals/Rtrigo.v | |
| parent | a5c2bbab10ba5f26ad289e1b911db69294946c55 (diff) | |
finish the rearrangement for removing the sin_PI2 axiom. This new version
- provides the atan function
- shows that this function is equal between -1 and 1 to a function defined
with power series
- establishes the equality with the PI value as given by the alternated
series constructed with PI_tg
- provides a smarter theorem to compute approximations of PI, based on a
formula in the same family as the one used by John Machin in 1706
Dependencies between files have been rearranged so that the new theorems
are loaded with the library Reals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15429 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo.v')
| -rw-r--r-- | theories/Reals/Rtrigo.v | 2049 |
1 files changed, 3 insertions, 2046 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 88bf0e084..8f936b37b 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -21,2049 +21,6 @@ Require Import Fourier. Require Import Ranalysis1. Require Import Rsqrt_def. Require Import PSeries_reg. - -Local Open Scope nat_scope. -Local Open Scope R_scope. - -Lemma CVN_R_cos : - forall fn:nat -> R -> R, - fn = (fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)) -> - CVN_R fn. -Proof. - unfold CVN_R in |- *; intros. - cut ((r:R) <> 0). - intro hyp_r; unfold CVN_r in |- *. - exists (fun n:nat => / INR (fact (2 * n)) * r ^ (2 * n)). - cut - { l:R | - Un_cv - (fun n:nat => - sum_f_R0 (fun k:nat => Rabs (/ INR (fact (2 * k)) * r ^ (2 * k))) - n) l }. - intro X; elim X; intros. - exists x. - split. - apply p. - intros; rewrite H; unfold Rdiv in |- *; do 2 rewrite Rabs_mult. - rewrite pow_1_abs; rewrite Rmult_1_l. - cut (0 < / INR (fact (2 * n))). - intro; rewrite (Rabs_right _ (Rle_ge _ _ (Rlt_le _ _ H1))). - apply Rmult_le_compat_l. - left; apply H1. - rewrite <- RPow_abs; apply pow_maj_Rabs. - rewrite Rabs_Rabsolu. - unfold Boule in H0; rewrite Rminus_0_r in H0. - left; apply H0. - apply Rinv_0_lt_compat; apply INR_fact_lt_0. - apply Alembert_C2. - intro; apply Rabs_no_R0. - apply prod_neq_R0. - apply Rinv_neq_0_compat. - apply INR_fact_neq_0. - apply pow_nonzero; assumption. - assert (H0 := Alembert_cos). - unfold cos_n in H0; unfold Un_cv in H0; unfold Un_cv in |- *; intros. - cut (0 < eps / Rsqr r). - intro; elim (H0 _ H2); intros N0 H3. - exists N0; intros. - unfold R_dist in |- *; assert (H5 := H3 _ H4). - unfold R_dist in H5; - replace - (Rabs - (Rabs (/ INR (fact (2 * S n)) * r ^ (2 * S n)) / - Rabs (/ INR (fact (2 * n)) * r ^ (2 * n)))) with - (Rsqr r * - Rabs ((-1) ^ S n / INR (fact (2 * S n)) / ((-1) ^ n / INR (fact (2 * n))))). - apply Rmult_lt_reg_l with (/ Rsqr r). - apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption. - pattern (/ Rsqr r) at 1 in |- *; replace (/ Rsqr r) with (Rabs (/ Rsqr r)). - rewrite <- Rabs_mult; rewrite Rmult_minus_distr_l; rewrite Rmult_0_r; - rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); apply H5. - unfold Rsqr in |- *; apply prod_neq_R0; assumption. - rewrite Rabs_Rinv. - rewrite Rabs_right. - reflexivity. - apply Rle_ge; apply Rle_0_sqr. - unfold Rsqr in |- *; apply prod_neq_R0; assumption. - rewrite (Rmult_comm (Rsqr r)); unfold Rdiv in |- *; repeat rewrite Rabs_mult; - rewrite Rabs_Rabsolu; rewrite pow_1_abs; rewrite Rmult_1_l; - repeat rewrite Rmult_assoc; apply Rmult_eq_compat_l. - rewrite Rabs_Rinv. - rewrite Rabs_mult; rewrite (pow_1_abs n); rewrite Rmult_1_l; - rewrite <- Rabs_Rinv. - rewrite Rinv_involutive. - rewrite Rinv_mult_distr. - rewrite Rabs_Rinv. - rewrite Rinv_involutive. - rewrite (Rmult_comm (Rabs (Rabs (r ^ (2 * S n))))); rewrite Rabs_mult; - rewrite Rabs_Rabsolu; rewrite Rmult_assoc; apply Rmult_eq_compat_l. - rewrite Rabs_Rinv. - do 2 rewrite Rabs_Rabsolu; repeat rewrite Rabs_right. - replace (r ^ (2 * S n)) with (r ^ (2 * n) * r * r). - repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. - unfold Rsqr in |- *; ring. - apply pow_nonzero; assumption. - replace (2 * S n)%nat with (S (S (2 * n))). - simpl in |- *; ring. - ring. - apply Rle_ge; apply pow_le; left; apply (cond_pos r). - apply Rle_ge; apply pow_le; left; apply (cond_pos r). - apply Rabs_no_R0; apply pow_nonzero; assumption. - apply Rabs_no_R0; apply INR_fact_neq_0. - apply INR_fact_neq_0. - apply Rabs_no_R0; apply Rinv_neq_0_compat; apply INR_fact_neq_0. - apply Rabs_no_R0; apply pow_nonzero; assumption. - apply INR_fact_neq_0. - apply Rinv_neq_0_compat; apply INR_fact_neq_0. - apply prod_neq_R0. - apply pow_nonzero; discrR. - apply Rinv_neq_0_compat; apply INR_fact_neq_0. - unfold Rdiv in |- *; apply Rmult_lt_0_compat. - apply H1. - apply Rinv_0_lt_compat; apply Rsqr_pos_lt; assumption. - assert (H0 := cond_pos r); red in |- *; intro; rewrite H1 in H0; - elim (Rlt_irrefl _ H0). -Qed. - -(**********) -Lemma continuity_cos : continuity cos. -Proof. - set (fn := fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N)) * x ^ (2 * N)). - cut (CVN_R fn). - intro; cut (forall x:R, { l:R | Un_cv (fun N:nat => SP fn N x) l }). - intro cv; cut (forall n:nat, continuity (fn n)). - intro; cut (forall x:R, cos x = SFL fn cv x). - intro; cut (continuity (SFL fn cv) -> continuity cos). - intro; apply H1. - apply SFL_continuity; assumption. - unfold continuity in |- *; unfold continuity_pt in |- *; - unfold continue_in in |- *; unfold limit1_in in |- *; - unfold limit_in in |- *; simpl in |- *; unfold R_dist in |- *; - intros. - elim (H1 x _ H2); intros. - exists x0; intros. - elim H3; intros. - split. - apply H4. - intros; rewrite (H0 x); rewrite (H0 x1); apply H5; apply H6. - intro; unfold cos, SFL in |- *. - case (cv x); case (exist_cos (Rsqr x)); intros. - symmetry in |- *; eapply UL_sequence. - apply u. - unfold cos_in in c; unfold infinite_sum in c; unfold Un_cv in |- *; intros. - elim (c _ H0); intros N0 H1. - exists N0; intros. - unfold R_dist in H1; unfold R_dist, SP in |- *. - replace (sum_f_R0 (fun k:nat => fn k x) n) with - (sum_f_R0 (fun i:nat => cos_n i * Rsqr x ^ i) n). - apply H1; assumption. - apply sum_eq; intros. - unfold cos_n, fn in |- *; apply Rmult_eq_compat_l. - unfold Rsqr in |- *; rewrite pow_sqr; reflexivity. - intro; unfold fn in |- *; - replace (fun x:R => (-1) ^ n / INR (fact (2 * n)) * x ^ (2 * n)) with - (fct_cte ((-1) ^ n / INR (fact (2 * n))) * pow_fct (2 * n))%F; - [ idtac | reflexivity ]. - apply continuity_mult. - apply derivable_continuous; apply derivable_const. - apply derivable_continuous; apply (derivable_pow (2 * n)). - apply CVN_R_CVS; apply X. - apply CVN_R_cos; unfold fn in |- *; reflexivity. -Qed. - -Lemma sin_gt_cos_7_8 : sin (7 / 8) > cos (7 / 8). -Proof. -assert (lo1 : 0 <= 7/8) by fourier. -assert (up1 : 7/8 <= 4) by fourier. -assert (lo : -2 <= 7/8) by fourier. -assert (up : 7/8 <= 2) by fourier. -destruct (pre_sin_bound _ 0 lo1 up1) as [lower _ ]. -destruct (pre_cos_bound _ 0 lo up) as [_ upper]. -apply Rle_lt_trans with (1 := upper). -apply Rlt_le_trans with (2 := lower). -unfold cos_approx, sin_approx. -simpl sum_f_R0; replace 7 with (IZR 7) by (simpl; field). -replace 8 with (IZR 8) by (simpl; field). -unfold cos_term, sin_term; simpl fact; rewrite !INR_IZR_INZ. -simpl plus; simpl mult. -field_simplify; - try (repeat apply conj; apply not_eq_sym, Rlt_not_eq, (IZR_lt 0); reflexivity). -unfold Rminus; rewrite !pow_IZR, <- !mult_IZR, <- !opp_IZR, <- ?plus_IZR. -match goal with - |- IZR ?a / ?b < ?c / ?d => - apply Rmult_lt_reg_r with d;[apply (IZR_lt 0); reflexivity | - unfold Rdiv at 2; rewrite Rmult_assoc, Rinv_l, Rmult_1_r, Rmult_comm; - [ |apply not_eq_sym, Rlt_not_eq, (IZR_lt 0); reflexivity ]]; - apply Rmult_lt_reg_r with b;[apply (IZR_lt 0); reflexivity | ] -end. -unfold Rdiv; rewrite !Rmult_assoc, Rinv_l, Rmult_1_r; - [ | apply not_eq_sym, Rlt_not_eq, (IZR_lt 0); reflexivity]. -repeat (rewrite <- !plus_IZR || rewrite <- !mult_IZR). -apply IZR_lt; reflexivity. -Qed. - -Definition PI_2_aux : {z | 7/8 <= z <= 7/4 /\ -cos z = 0}. -assert (cc : continuity (fun r =>- cos r)). - apply continuity_opp, continuity_cos. -assert (cvp : 0 < cos (7/8)). - assert (int78 : -2 <= 7/8 <= 2) by (split; fourier). - destruct int78 as [lower upper]. - case (pre_cos_bound _ 0 lower upper). - unfold cos_approx; simpl sum_f_R0; unfold cos_term. - intros cl _; apply Rlt_le_trans with (2 := cl); simpl. - fourier. -assert (cun : cos (7/4) < 0). - replace (7/4) with (7/8 + 7/8) by field. - rewrite cos_plus. - apply Rlt_minus; apply Rsqr_incrst_1. - exact sin_gt_cos_7_8. - apply Rlt_le; assumption. - apply Rlt_le; apply Rlt_trans with (1 := cvp); exact sin_gt_cos_7_8. -apply IVT; auto; fourier. -Qed. - -Definition PI2 := proj1_sig PI_2_aux. - -Definition PI := 2 * PI2. - -Lemma cos_pi2 : cos PI2 = 0. -unfold PI2; case PI_2_aux; simpl. -intros x [_ q]; rewrite <- (Ropp_involutive (cos x)), q; apply Ropp_0. -Qed. - -Lemma pi2_int : 7/8 <= PI2 <= 7/4. -unfold PI2; case PI_2_aux; simpl; tauto. -Qed. - -(**********) -Lemma cos_minus : forall x y:R, cos (x - y) = cos x * cos y + sin x * sin y. -Proof. - intros; unfold Rminus in |- *; rewrite cos_plus. - rewrite <- cos_sym; rewrite sin_antisym; ring. -Qed. - -(**********) -Lemma sin2_cos2 : forall x:R, Rsqr (sin x) + Rsqr (cos x) = 1. -Proof. - intro; unfold Rsqr in |- *; rewrite Rplus_comm; rewrite <- (cos_minus x x); - unfold Rminus in |- *; rewrite Rplus_opp_r; apply cos_0. -Qed. - -Lemma cos2 : forall x:R, Rsqr (cos x) = 1 - Rsqr (sin x). -Proof. - intros x; rewrite <- (sin2_cos2 x); ring. -Qed. - -Lemma sin2 : forall x:R, Rsqr (sin x) = 1 - Rsqr (cos x). -Proof. - intro x; generalize (cos2 x); intro H1; rewrite H1. - unfold Rminus in |- *; rewrite Ropp_plus_distr; rewrite <- Rplus_assoc; - rewrite Rplus_opp_r; rewrite Rplus_0_l; symmetry in |- *; - apply Ropp_involutive. -Qed. - -(**********) -Lemma cos_PI2 : cos (PI / 2) = 0. -Proof. - unfold PI; generalize cos_pi2; replace ((2 * PI2)/2) with PI2 by field; tauto. -Qed. - -Lemma sin_pos_tech : forall x, 0 < x < 2 -> 0 < sin x. -intros x [int1 int2]. -assert (lo : 0 <= x) by (apply Rlt_le; assumption). -assert (up : x <= 4) by (apply Rlt_le, Rlt_trans with (1:=int2); fourier). -destruct (pre_sin_bound _ 0 lo up) as [t _]; clear lo up. -apply Rlt_le_trans with (2:= t); clear t. -unfold sin_approx; simpl sum_f_R0; unfold sin_term; simpl. -match goal with |- _ < ?a => - replace a with (x * (1 - x^2/6)) by (simpl; field) -end. -assert (t' : x ^ 2 <= 4). - replace 4 with (2 ^ 2) by field. - apply (pow_incr x 2); split; apply Rlt_le; assumption. -apply Rmult_lt_0_compat;[assumption | fourier ]. -Qed. - -Lemma sin_PI2 : sin (PI / 2) = 1. -replace (PI / 2) with PI2 by (unfold PI; field). -assert (int' : 0 < PI2 < 2). - destruct pi2_int; split; fourier. -assert (lo2 := sin_pos_tech PI2 int'). -assert (t2 : Rabs (sin PI2) = 1). - rewrite <- Rabs_R1; apply Rsqr_eq_abs_0. - rewrite Rsqr_1, sin2, cos_pi2, Rsqr_0, Rminus_0_r; reflexivity. -revert t2; rewrite Rabs_pos_eq;[| apply Rlt_le]; tauto. -Qed. - -Lemma PI_RGT_0 : PI > 0. -Proof. unfold PI; destruct pi2_int; fourier. Qed. - -Lemma PI_4 : PI <= 4. -Proof. unfold PI; destruct pi2_int; fourier. Qed. - -(**********) -Lemma PI_neq0 : PI <> 0. -Proof. - red in |- *; intro; assert (H0 := PI_RGT_0); rewrite H in H0; - elim (Rlt_irrefl _ H0). -Qed. - - -(**********) -Lemma cos_PI : cos PI = -1. -Proof. - replace PI with (PI / 2 + PI / 2). - rewrite cos_plus. - rewrite sin_PI2; rewrite cos_PI2. - ring. - symmetry in |- *; apply double_var. -Qed. - -Lemma sin_PI : sin PI = 0. -Proof. - assert (H := sin2_cos2 PI). - rewrite cos_PI in H. - rewrite <- Rsqr_neg in H. - rewrite Rsqr_1 in H. - cut (Rsqr (sin PI) = 0). - intro; apply (Rsqr_eq_0 _ H0). - apply Rplus_eq_reg_l with 1. - rewrite Rplus_0_r; rewrite Rplus_comm; exact H. -Qed. - -Lemma sin_bound : forall (a : R) (n : nat), 0 <= a -> a <= PI -> - sin_approx a (2 * n + 1) <= sin a <= sin_approx a (2 * (n + 1)). -Proof. -intros a n a0 api; apply pre_sin_bound. - assumption. -apply Rle_trans with (1:= api) (2 := PI_4). -Qed. - -Lemma cos_bound : forall (a : R) (n : nat), - PI / 2 <= a -> a <= PI / 2 -> - cos_approx a (2 * n + 1) <= cos a <= cos_approx a (2 * (n + 1)). -Proof. -intros a n lower upper; apply pre_cos_bound. - apply Rle_trans with (2 := lower). - apply Rmult_le_reg_r with 2; [fourier |]. - replace ((-PI/2) * 2) with (-PI) by field. - assert (t := PI_4); fourier. -apply Rle_trans with (1 := upper). -apply Rmult_le_reg_r with 2; [fourier | ]. -replace ((PI/2) * 2) with PI by field. -generalize PI_4; intros; fourier. -Qed. -(**********) -Lemma neg_cos : forall x:R, cos (x + PI) = - cos x. -Proof. - intro x; rewrite cos_plus; rewrite sin_PI; rewrite cos_PI; ring. -Qed. - -(**********) -Lemma sin_cos : forall x:R, sin x = - cos (PI / 2 + x). -Proof. - intro x; rewrite cos_plus; rewrite sin_PI2; rewrite cos_PI2; ring. -Qed. - -(**********) -Lemma sin_plus : forall x y:R, sin (x + y) = sin x * cos y + cos x * sin y. -Proof. - intros. - rewrite (sin_cos (x + y)). - replace (PI / 2 + (x + y)) with (PI / 2 + x + y); [ rewrite cos_plus | ring ]. - rewrite (sin_cos (PI / 2 + x)). - replace (PI / 2 + (PI / 2 + x)) with (x + PI). - rewrite neg_cos. - replace (cos (PI / 2 + x)) with (- sin x). - ring. - rewrite sin_cos; rewrite Ropp_involutive; reflexivity. - pattern PI at 1 in |- *; rewrite (double_var PI); ring. -Qed. - -Lemma sin_minus : forall x y:R, sin (x - y) = sin x * cos y - cos x * sin y. -Proof. - intros; unfold Rminus in |- *; rewrite sin_plus. - rewrite <- cos_sym; rewrite sin_antisym; ring. -Qed. - -(**********) -Definition tan (x:R) : R := sin x / cos x. - -Lemma tan_plus : - forall x y:R, - cos x <> 0 -> - cos y <> 0 -> - cos (x + y) <> 0 -> - 1 - tan x * tan y <> 0 -> - tan (x + y) = (tan x + tan y) / (1 - tan x * tan y). -Proof. - intros; unfold tan in |- *; rewrite sin_plus; rewrite cos_plus; - unfold Rdiv in |- *; - replace (cos x * cos y - sin x * sin y) with - (cos x * cos y * (1 - sin x * / cos x * (sin y * / cos y))). - rewrite Rinv_mult_distr. - repeat rewrite <- Rmult_assoc; - replace ((sin x * cos y + cos x * sin y) * / (cos x * cos y)) with - (sin x * / cos x + sin y * / cos y). - reflexivity. - rewrite Rmult_plus_distr_r; rewrite Rinv_mult_distr. - repeat rewrite Rmult_assoc; repeat rewrite (Rmult_comm (sin x)); - repeat rewrite <- Rmult_assoc. - repeat rewrite Rinv_r_simpl_m; [ reflexivity | assumption | assumption ]. - assumption. - assumption. - apply prod_neq_R0; assumption. - assumption. - unfold Rminus in |- *; rewrite Rmult_plus_distr_l; rewrite Rmult_1_r; - apply Rplus_eq_compat_l; repeat rewrite Rmult_assoc; - rewrite (Rmult_comm (sin x)); rewrite (Rmult_comm (cos y)); - rewrite <- Ropp_mult_distr_r_reverse; repeat rewrite <- Rmult_assoc; - rewrite <- Rinv_r_sym. - rewrite Rmult_1_l; rewrite (Rmult_comm (sin x)); - rewrite <- Ropp_mult_distr_r_reverse; repeat rewrite Rmult_assoc; - apply Rmult_eq_compat_l; rewrite (Rmult_comm (/ cos y)); - rewrite Rmult_assoc; rewrite <- Rinv_r_sym. - apply Rmult_1_r. - assumption. - assumption. -Qed. - -(*******************************************************) -(** * Some properties of cos, sin and tan *) -(*******************************************************) - -Lemma sin_2a : forall x:R, sin (2 * x) = 2 * sin x * cos x. -Proof. - intro x; rewrite double; rewrite sin_plus. - rewrite <- (Rmult_comm (sin x)); symmetry in |- *; rewrite Rmult_assoc; - apply double. -Qed. - -Lemma cos_2a : forall x:R, cos (2 * x) = cos x * cos x - sin x * sin x. -Proof. - intro x; rewrite double; apply cos_plus. -Qed. - -Lemma cos_2a_cos : forall x:R, cos (2 * x) = 2 * cos x * cos x - 1. -Proof. - intro x; rewrite double; unfold Rminus in |- *; rewrite Rmult_assoc; - rewrite cos_plus; generalize (sin2_cos2 x); rewrite double; - intro H1; rewrite <- H1; ring_Rsqr. -Qed. - -Lemma cos_2a_sin : forall x:R, cos (2 * x) = 1 - 2 * sin x * sin x. -Proof. - intro x; rewrite Rmult_assoc; unfold Rminus in |- *; repeat rewrite double. - generalize (sin2_cos2 x); intro H1; rewrite <- H1; rewrite cos_plus; - ring_Rsqr. -Qed. - -Lemma tan_2a : - forall x:R, - cos x <> 0 -> - cos (2 * x) <> 0 -> - 1 - tan x * tan x <> 0 -> tan (2 * x) = 2 * tan x / (1 - tan x * tan x). -Proof. - repeat rewrite double; intros; repeat rewrite double; rewrite double in H0; - apply tan_plus; assumption. -Qed. - -Lemma sin_neg : forall x:R, sin (- x) = - sin x. -Proof. - apply sin_antisym. -Qed. - -Lemma cos_neg : forall x:R, cos (- x) = cos x. -Proof. - intro; symmetry in |- *; apply cos_sym. -Qed. - -Lemma tan_0 : tan 0 = 0. -Proof. - unfold tan in |- *; rewrite sin_0; rewrite cos_0. - unfold Rdiv in |- *; apply Rmult_0_l. -Qed. - -Lemma tan_neg : forall x:R, tan (- x) = - tan x. -Proof. - intros x; unfold tan in |- *; rewrite sin_neg; rewrite cos_neg; - unfold Rdiv in |- *. - apply Ropp_mult_distr_l_reverse. -Qed. - -Lemma tan_minus : - forall x y:R, - cos x <> 0 -> - cos y <> 0 -> - cos (x - y) <> 0 -> - 1 + tan x * tan y <> 0 -> - tan (x - y) = (tan x - tan y) / (1 + tan x * tan y). -Proof. - intros; unfold Rminus in |- *; rewrite tan_plus. - rewrite tan_neg; unfold Rminus in |- *; rewrite <- Ropp_mult_distr_l_reverse; - rewrite Rmult_opp_opp; reflexivity. - assumption. - rewrite cos_neg; assumption. - assumption. - rewrite tan_neg; unfold Rminus in |- *; rewrite <- Ropp_mult_distr_l_reverse; - rewrite Rmult_opp_opp; assumption. -Qed. - -Lemma cos_3PI2 : cos (3 * (PI / 2)) = 0. -Proof. - replace (3 * (PI / 2)) with (PI + PI / 2). - rewrite cos_plus; rewrite sin_PI; rewrite cos_PI2; ring. - pattern PI at 1 in |- *; rewrite (double_var PI). - ring. -Qed. - -Lemma sin_2PI : sin (2 * PI) = 0. -Proof. - rewrite sin_2a; rewrite sin_PI; ring. -Qed. - -Lemma cos_2PI : cos (2 * PI) = 1. -Proof. - rewrite cos_2a; rewrite sin_PI; rewrite cos_PI; ring. -Qed. - -Lemma neg_sin : forall x:R, sin (x + PI) = - sin x. -Proof. - intro x; rewrite sin_plus; rewrite sin_PI; rewrite cos_PI; ring. -Qed. - -Lemma sin_PI_x : forall x:R, sin (PI - x) = sin x. -Proof. - intro x; rewrite sin_minus; rewrite sin_PI; rewrite cos_PI; rewrite Rmult_0_l; - unfold Rminus in |- *; rewrite Rplus_0_l; rewrite Ropp_mult_distr_l_reverse; - rewrite Ropp_involutive; apply Rmult_1_l. -Qed. - -Lemma sin_period : forall (x:R) (k:nat), sin (x + 2 * INR k * PI) = sin x. -Proof. - intros x k; induction k as [| k Hreck]. - simpl in |- *; ring_simplify (x + 2 * 0 * PI). - trivial. - - replace (x + 2 * INR (S k) * PI) with (x + 2 * INR k * PI + 2 * PI). - rewrite sin_plus in |- *; rewrite sin_2PI in |- *; rewrite cos_2PI in |- *. - ring_simplify; trivial. - rewrite S_INR in |- *; ring. -Qed. - -Lemma cos_period : forall (x:R) (k:nat), cos (x + 2 * INR k * PI) = cos x. -Proof. - intros x k; induction k as [| k Hreck]. - simpl in |- *; ring_simplify (x + 2 * 0 * PI). - trivial. - - replace (x + 2 * INR (S k) * PI) with (x + 2 * INR k * PI + 2 * PI). - rewrite cos_plus in |- *; rewrite sin_2PI in |- *; rewrite cos_2PI in |- *. - ring_simplify; trivial. - rewrite S_INR in |- *; ring. -Qed. - -Lemma sin_shift : forall x:R, sin (PI / 2 - x) = cos x. -Proof. - intro x; rewrite sin_minus; rewrite sin_PI2; rewrite cos_PI2; ring. -Qed. - -Lemma cos_shift : forall x:R, cos (PI / 2 - x) = sin x. -Proof. - intro x; rewrite cos_minus; rewrite sin_PI2; rewrite cos_PI2; ring. -Qed. - -Lemma cos_sin : forall x:R, cos x = sin (PI / 2 + x). -Proof. - intro x; rewrite sin_plus; rewrite sin_PI2; rewrite cos_PI2; ring. -Qed. - -Lemma PI2_RGT_0 : 0 < PI / 2. -Proof. - unfold Rdiv in |- *; apply Rmult_lt_0_compat; - [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup ]. -Qed. - -Lemma SIN_bound : forall x:R, -1 <= sin x <= 1. -Proof. - intro; case (Rle_dec (-1) (sin x)); intro. - case (Rle_dec (sin x) 1); intro. - split; assumption. - cut (1 < sin x). - intro; - generalize - (Rsqr_incrst_1 1 (sin x) H (Rlt_le 0 1 Rlt_0_1) - (Rlt_le 0 (sin x) (Rlt_trans 0 1 (sin x) Rlt_0_1 H))); - rewrite Rsqr_1; intro; rewrite sin2 in H0; unfold Rminus in H0; - generalize (Rplus_lt_compat_l (-1) 1 (1 + - Rsqr (cos x)) H0); - repeat rewrite <- Rplus_assoc; repeat rewrite Rplus_opp_l; - rewrite Rplus_0_l; intro; rewrite <- Ropp_0 in H1; - generalize (Ropp_lt_gt_contravar (-0) (- Rsqr (cos x)) H1); - repeat rewrite Ropp_involutive; intro; generalize (Rle_0_sqr (cos x)); - intro; elim (Rlt_irrefl 0 (Rle_lt_trans 0 (Rsqr (cos x)) 0 H3 H2)). - auto with real. - cut (sin x < -1). - intro; generalize (Ropp_lt_gt_contravar (sin x) (-1) H); - rewrite Ropp_involutive; clear H; intro; - generalize - (Rsqr_incrst_1 1 (- sin x) H (Rlt_le 0 1 Rlt_0_1) - (Rlt_le 0 (- sin x) (Rlt_trans 0 1 (- sin x) Rlt_0_1 H))); - rewrite Rsqr_1; intro; rewrite <- Rsqr_neg in H0; - rewrite sin2 in H0; unfold Rminus in H0; - generalize (Rplus_lt_compat_l (-1) 1 (1 + - Rsqr (cos x)) H0); - repeat rewrite <- Rplus_assoc; repeat rewrite Rplus_opp_l; - rewrite Rplus_0_l; intro; rewrite <- Ropp_0 in H1; - generalize (Ropp_lt_gt_contravar (-0) (- Rsqr (cos x)) H1); - repeat rewrite Ropp_involutive; intro; generalize (Rle_0_sqr (cos x)); - intro; elim (Rlt_irrefl 0 (Rle_lt_trans 0 (Rsqr (cos x)) 0 H3 H2)). - auto with real. -Qed. - -Lemma COS_bound : forall x:R, -1 <= cos x <= 1. -Proof. - intro; rewrite <- sin_shift; apply SIN_bound. -Qed. - -Lemma cos_sin_0 : forall x:R, ~ (cos x = 0 /\ sin x = 0). -Proof. - intro; red in |- *; intro; elim H; intros; generalize (sin2_cos2 x); intro; - rewrite H0 in H2; rewrite H1 in H2; repeat rewrite Rsqr_0 in H2; - rewrite Rplus_0_r in H2; generalize Rlt_0_1; intro; - rewrite <- H2 in H3; elim (Rlt_irrefl 0 H3). -Qed. - -Lemma cos_sin_0_var : forall x:R, cos x <> 0 \/ sin x <> 0. -Proof. - intros x. - destruct (Req_dec (cos x) 0). 2: now left. - right. intros H'. - apply (cos_sin_0 x). - now split. -Qed. - -(*****************************************************************) -(** * Using series definitions of cos and sin *) -(*****************************************************************) - -Definition sin_lb (a:R) : R := sin_approx a 3. -Definition sin_ub (a:R) : R := sin_approx a 4. -Definition cos_lb (a:R) : R := cos_approx a 3. -Definition cos_ub (a:R) : R := cos_approx a 4. - -Lemma sin_lb_gt_0 : forall a:R, 0 < a -> a <= PI / 2 -> 0 < sin_lb a. -Proof. - intros. - unfold sin_lb in |- *; unfold sin_approx in |- *; unfold sin_term in |- *. - set (Un := fun i:nat => a ^ (2 * i + 1) / INR (fact (2 * i + 1))). - replace - (sum_f_R0 - (fun i:nat => (-1) ^ i * (a ^ (2 * i + 1) / INR (fact (2 * i + 1)))) 3) - with (sum_f_R0 (fun i:nat => (-1) ^ i * Un i) 3); - [ idtac | apply sum_eq; intros; unfold Un in |- *; reflexivity ]. - cut (forall n:nat, Un (S n) < Un n). - intro; simpl in |- *. - repeat rewrite Rmult_1_l; repeat rewrite Rmult_1_r; - replace (-1 * Un 1%nat) with (- Un 1%nat); [ idtac | ring ]; - replace (-1 * -1 * Un 2%nat) with (Un 2%nat); [ idtac | ring ]; - replace (-1 * (-1 * -1) * Un 3%nat) with (- Un 3%nat); - [ idtac | ring ]; - replace (Un 0%nat + - Un 1%nat + Un 2%nat + - Un 3%nat) with - (Un 0%nat - Un 1%nat + (Un 2%nat - Un 3%nat)); [ idtac | ring ]. - apply Rplus_lt_0_compat. - unfold Rminus in |- *; apply Rplus_lt_reg_r with (Un 1%nat); - rewrite Rplus_0_r; rewrite (Rplus_comm (Un 1%nat)); - rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; - apply H1. - unfold Rminus in |- *; apply Rplus_lt_reg_r with (Un 3%nat); - rewrite Rplus_0_r; rewrite (Rplus_comm (Un 3%nat)); - rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; - apply H1. - intro; unfold Un in |- *. - cut ((2 * S n + 1)%nat = (2 * n + 1 + 2)%nat). - intro; rewrite H1. - rewrite pow_add; unfold Rdiv in |- *; rewrite Rmult_assoc; - apply Rmult_lt_compat_l. - apply pow_lt; assumption. - rewrite <- H1; apply Rmult_lt_reg_l with (INR (fact (2 * n + 1))). - apply lt_INR_0; apply neq_O_lt. - assert (H2 := fact_neq_0 (2 * n + 1)). - red in |- *; intro; elim H2; symmetry in |- *; assumption. - rewrite <- Rinv_r_sym. - apply Rmult_lt_reg_l with (INR (fact (2 * S n + 1))). - apply lt_INR_0; apply neq_O_lt. - assert (H2 := fact_neq_0 (2 * S n + 1)). - red in |- *; intro; elim H2; symmetry in |- *; assumption. - rewrite (Rmult_comm (INR (fact (2 * S n + 1)))); repeat rewrite Rmult_assoc; - rewrite <- Rinv_l_sym. - do 2 rewrite Rmult_1_r; apply Rle_lt_trans with (INR (fact (2 * n + 1)) * 4). - apply Rmult_le_compat_l. - replace 0 with (INR 0); [ idtac | reflexivity ]; apply le_INR; apply le_O_n. - simpl in |- *; rewrite Rmult_1_r; replace 4 with (Rsqr 2); - [ idtac | ring_Rsqr ]; replace (a * a) with (Rsqr a); - [ idtac | reflexivity ]; apply Rsqr_incr_1. - apply Rle_trans with (PI / 2); - [ assumption - | unfold Rdiv in |- *; apply Rmult_le_reg_l with 2; - [ prove_sup0 - | rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m; - [ replace 4 with 4; [ apply PI_4 | ring ] | discrR ] ] ]. - left; assumption. - left; prove_sup0. - rewrite H1; replace (2 * n + 1 + 2)%nat with (S (S (2 * n + 1))). - do 2 rewrite fact_simpl; do 2 rewrite mult_INR. - repeat rewrite <- Rmult_assoc. - rewrite <- (Rmult_comm (INR (fact (2 * n + 1)))). - rewrite Rmult_assoc. - apply Rmult_lt_compat_l. - apply lt_INR_0; apply neq_O_lt. - assert (H2 := fact_neq_0 (2 * n + 1)). - red in |- *; intro; elim H2; symmetry in |- *; assumption. - do 2 rewrite S_INR; rewrite plus_INR; rewrite mult_INR; set (x := INR n); - unfold INR in |- *. - replace ((2 * x + 1 + 1 + 1) * (2 * x + 1 + 1)) with (4 * x * x + 10 * x + 6); - [ idtac | ring ]. - apply Rplus_lt_reg_r with (-4); rewrite Rplus_opp_l; - replace (-4 + (4 * x * x + 10 * x + 6)) with (4 * x * x + 10 * x + 2); - [ idtac | ring ]. - apply Rplus_le_lt_0_compat. - cut (0 <= x). - intro; apply Rplus_le_le_0_compat; repeat apply Rmult_le_pos; - assumption || left; prove_sup. - unfold x in |- *; replace 0 with (INR 0); - [ apply le_INR; apply le_O_n | reflexivity ]. - prove_sup0. - ring. - apply INR_fact_neq_0. - apply INR_fact_neq_0. - ring. -Qed. - -Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a. - intros; unfold sin_lb, sin_ub in |- *; apply (sin_bound a 1 H H0). -Qed. - -Lemma COS : - forall a:R, - PI / 2 <= a -> a <= PI / 2 -> cos_lb a <= cos a <= cos_ub a. - intros; unfold cos_lb, cos_ub in |- *; apply (cos_bound a 1 H H0). -Qed. - -(**********) -Lemma _PI2_RLT_0 : - (PI / 2) < 0. -Proof. - rewrite <- Ropp_0; apply Ropp_lt_contravar; apply PI2_RGT_0. -Qed. - -Lemma PI4_RLT_PI2 : PI / 4 < PI / 2. -Proof. - unfold Rdiv in |- *; apply Rmult_lt_compat_l. - apply PI_RGT_0. - apply Rinv_lt_contravar. - apply Rmult_lt_0_compat; prove_sup0. - pattern 2 at 1 in |- *; rewrite <- Rplus_0_r. - replace 4 with (2 + 2); [ apply Rplus_lt_compat_l; prove_sup0 | ring ]. -Qed. - -Lemma PI2_Rlt_PI : PI / 2 < PI. -Proof. - unfold Rdiv in |- *; pattern PI at 2 in |- *; rewrite <- Rmult_1_r. - apply Rmult_lt_compat_l. - apply PI_RGT_0. - pattern 1 at 3 in |- *; rewrite <- Rinv_1; apply Rinv_lt_contravar. - rewrite Rmult_1_l; prove_sup0. - pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; - apply Rlt_0_1. -Qed. - -(***************************************************) -(** * Increasing and decreasing of [cos] and [sin] *) -(***************************************************) -Theorem sin_gt_0 : forall x:R, 0 < x -> x < PI -> 0 < sin x. -Proof. - intros; elim (SIN x (Rlt_le 0 x H) (Rlt_le x PI H0)); intros H1 _; - case (Rtotal_order x (PI / 2)); intro H2. - apply Rlt_le_trans with (sin_lb x). - apply sin_lb_gt_0; [ assumption | left; assumption ]. - assumption. - elim H2; intro H3. - rewrite H3; rewrite sin_PI2; apply Rlt_0_1. - rewrite <- sin_PI_x; generalize (Ropp_gt_lt_contravar x (PI / 2) H3); - intro H4; generalize (Rplus_lt_compat_l PI (- x) (- (PI / 2)) H4). - replace (PI + - x) with (PI - x). - replace (PI + - (PI / 2)) with (PI / 2). - intro H5; generalize (Ropp_lt_gt_contravar x PI H0); intro H6; - change (- PI < - x) in H6; generalize (Rplus_lt_compat_l PI (- PI) (- x) H6). - rewrite Rplus_opp_r. - replace (PI + - x) with (PI - x). - intro H7; - elim - (SIN (PI - x) (Rlt_le 0 (PI - x) H7) - (Rlt_le (PI - x) PI (Rlt_trans (PI - x) (PI / 2) PI H5 PI2_Rlt_PI))); - intros H8 _; - generalize (sin_lb_gt_0 (PI - x) H7 (Rlt_le (PI - x) (PI / 2) H5)); - intro H9; apply (Rlt_le_trans 0 (sin_lb (PI - x)) (sin (PI - x)) H9 H8). - reflexivity. - pattern PI at 2 in |- *; rewrite double_var; ring. - reflexivity. -Qed. - -Theorem cos_gt_0 : forall x:R, - (PI / 2) < x -> x < PI / 2 -> 0 < cos x. -Proof. - intros; rewrite cos_sin; - generalize (Rplus_lt_compat_l (PI / 2) (- (PI / 2)) x H). - rewrite Rplus_opp_r; intro H1; - generalize (Rplus_lt_compat_l (PI / 2) x (PI / 2) H0); - rewrite <- double_var; intro H2; apply (sin_gt_0 (PI / 2 + x) H1 H2). -Qed. - -Lemma sin_ge_0 : forall x:R, 0 <= x -> x <= PI -> 0 <= sin x. -Proof. - intros x H1 H2; elim H1; intro H3; - [ elim H2; intro H4; - [ left; apply (sin_gt_0 x H3 H4) - | rewrite H4; right; symmetry in |- *; apply sin_PI ] - | rewrite <- H3; right; symmetry in |- *; apply sin_0 ]. -Qed. - -Lemma cos_ge_0 : forall x:R, - (PI / 2) <= x -> x <= PI / 2 -> 0 <= cos x. -Proof. - intros x H1 H2; elim H1; intro H3; - [ elim H2; intro H4; - [ left; apply (cos_gt_0 x H3 H4) - | rewrite H4; right; symmetry in |- *; apply cos_PI2 ] - | rewrite <- H3; rewrite cos_neg; right; symmetry in |- *; apply cos_PI2 ]. -Qed. - -Lemma sin_le_0 : forall x:R, PI <= x -> x <= 2 * PI -> sin x <= 0. -Proof. - intros x H1 H2; apply Rge_le; rewrite <- Ropp_0; - rewrite <- (Ropp_involutive (sin x)); apply Ropp_le_ge_contravar; - rewrite <- neg_sin; replace (x + PI) with (x - PI + 2 * INR 1 * PI); - [ rewrite (sin_period (x - PI) 1); apply sin_ge_0; - [ replace (x - PI) with (x + - PI); - [ rewrite Rplus_comm; replace 0 with (- PI + PI); - [ apply Rplus_le_compat_l; assumption | ring ] - | ring ] - | replace (x - PI) with (x + - PI); rewrite Rplus_comm; - [ pattern PI at 2 in |- *; replace PI with (- PI + 2 * PI); - [ apply Rplus_le_compat_l; assumption | ring ] - | ring ] ] - | unfold INR in |- *; ring ]. -Qed. - -Lemma cos_le_0 : forall x:R, PI / 2 <= x -> x <= 3 * (PI / 2) -> cos x <= 0. -Proof. - intros x H1 H2; apply Rge_le; rewrite <- Ropp_0; - rewrite <- (Ropp_involutive (cos x)); apply Ropp_le_ge_contravar; - rewrite <- neg_cos; replace (x + PI) with (x - PI + 2 * INR 1 * PI). - rewrite cos_period; apply cos_ge_0. - replace (- (PI / 2)) with (- PI + PI / 2). - unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_le_compat_l; - assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. - unfold Rminus in |- *; rewrite Rplus_comm; - replace (PI / 2) with (- PI + 3 * (PI / 2)). - apply Rplus_le_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. - unfold INR in |- *; ring. -Qed. - -Lemma sin_lt_0 : forall x:R, PI < x -> x < 2 * PI -> sin x < 0. -Proof. - intros x H1 H2; rewrite <- Ropp_0; rewrite <- (Ropp_involutive (sin x)); - apply Ropp_lt_gt_contravar; rewrite <- neg_sin; - replace (x + PI) with (x - PI + 2 * INR 1 * PI); - [ rewrite (sin_period (x - PI) 1); apply sin_gt_0; - [ replace (x - PI) with (x + - PI); - [ rewrite Rplus_comm; replace 0 with (- PI + PI); - [ apply Rplus_lt_compat_l; assumption | ring ] - | ring ] - | replace (x - PI) with (x + - PI); rewrite Rplus_comm; - [ pattern PI at 2 in |- *; replace PI with (- PI + 2 * PI); - [ apply Rplus_lt_compat_l; assumption | ring ] - | ring ] ] - | unfold INR in |- *; ring ]. -Qed. - -Lemma sin_lt_0_var : forall x:R, - PI < x -> x < 0 -> sin x < 0. -Proof. - intros; generalize (Rplus_lt_compat_l (2 * PI) (- PI) x H); - replace (2 * PI + - PI) with PI; - [ intro H1; rewrite Rplus_comm in H1; - generalize (Rplus_lt_compat_l (2 * PI) x 0 H0); - intro H2; rewrite (Rplus_comm (2 * PI)) in H2; - rewrite <- (Rplus_comm 0) in H2; rewrite Rplus_0_l in H2; - rewrite <- (sin_period x 1); unfold INR in |- *; - replace (2 * 1 * PI) with (2 * PI); - [ apply (sin_lt_0 (x + 2 * PI) H1 H2) | ring ] - | ring ]. -Qed. - -Lemma cos_lt_0 : forall x:R, PI / 2 < x -> x < 3 * (PI / 2) -> cos x < 0. -Proof. - intros x H1 H2; rewrite <- Ropp_0; rewrite <- (Ropp_involutive (cos x)); - apply Ropp_lt_gt_contravar; rewrite <- neg_cos; - replace (x + PI) with (x - PI + 2 * INR 1 * PI). - rewrite cos_period; apply cos_gt_0. - replace (- (PI / 2)) with (- PI + PI / 2). - unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_lt_compat_l; - assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. - unfold Rminus in |- *; rewrite Rplus_comm; - replace (PI / 2) with (- PI + 3 * (PI / 2)). - apply Rplus_lt_compat_l; assumption. - pattern PI at 1 in |- *; rewrite (double_var PI); rewrite Ropp_plus_distr; - ring. - unfold INR in |- *; ring. -Qed. - -Lemma tan_gt_0 : forall x:R, 0 < x -> x < PI / 2 -> 0 < tan x. -Proof. - intros x H1 H2; unfold tan in |- *; generalize _PI2_RLT_0; - generalize (Rlt_trans 0 x (PI / 2) H1 H2); intros; - generalize (Rlt_trans (- (PI / 2)) 0 x H0 H1); intro H5; - generalize (Rlt_trans x (PI / 2) PI H2 PI2_Rlt_PI); - intro H7; unfold Rdiv in |- *; apply Rmult_lt_0_compat. - apply sin_gt_0; assumption. - apply Rinv_0_lt_compat; apply cos_gt_0; assumption. -Qed. - -Lemma tan_lt_0 : forall x:R, - (PI / 2) < x -> x < 0 -> tan x < 0. -Proof. - intros x H1 H2; unfold tan in |- *; - generalize (cos_gt_0 x H1 (Rlt_trans x 0 (PI / 2) H2 PI2_RGT_0)); - intro H3; rewrite <- Ropp_0; - replace (sin x / cos x) with (- (- sin x / cos x)). - rewrite <- sin_neg; apply Ropp_gt_lt_contravar; - change (0 < sin (- x) / cos x) in |- *; unfold Rdiv in |- *; - apply Rmult_lt_0_compat. - apply sin_gt_0. - rewrite <- Ropp_0; apply Ropp_gt_lt_contravar; assumption. - apply Rlt_trans with (PI / 2). - rewrite <- (Ropp_involutive (PI / 2)); apply Ropp_gt_lt_contravar; assumption. - apply PI2_Rlt_PI. - apply Rinv_0_lt_compat; assumption. - unfold Rdiv in |- *; ring. -Qed. - -Lemma cos_ge_0_3PI2 : - forall x:R, 3 * (PI / 2) <= x -> x <= 2 * PI -> 0 <= cos x. -Proof. - intros; rewrite <- cos_neg; rewrite <- (cos_period (- x) 1); - unfold INR in |- *; replace (- x + 2 * 1 * PI) with (2 * PI - x). - generalize (Ropp_le_ge_contravar x (2 * PI) H0); intro H1; - generalize (Rge_le (- x) (- (2 * PI)) H1); clear H1; - intro H1; generalize (Rplus_le_compat_l (2 * PI) (- (2 * PI)) (- x) H1). - rewrite Rplus_opp_r. - intro H2; generalize (Ropp_le_ge_contravar (3 * (PI / 2)) x H); intro H3; - generalize (Rge_le (- (3 * (PI / 2))) (- x) H3); clear H3; - intro H3; - generalize (Rplus_le_compat_l (2 * PI) (- x) (- (3 * (PI / 2))) H3). - replace (2 * PI + - (3 * (PI / 2))) with (PI / 2). - intro H4; - apply - (cos_ge_0 (2 * PI - x) - (Rlt_le (- (PI / 2)) (2 * PI - x) - (Rlt_le_trans (- (PI / 2)) 0 (2 * PI - x) _PI2_RLT_0 H2)) H4). - rewrite double; pattern PI at 2 3 in |- *; rewrite double_var; ring. - ring. -Qed. - -Lemma form1 : - forall p q:R, cos p + cos q = 2 * cos ((p - q) / 2) * cos ((p + q) / 2). -Proof. - intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2). - rewrite cos_plus; rewrite cos_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. -Qed. - -Lemma form2 : - forall p q:R, cos p - cos q = -2 * sin ((p - q) / 2) * sin ((p + q) / 2). -Proof. - intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2). - rewrite cos_plus; rewrite cos_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. -Qed. - -Lemma form3 : - forall p q:R, sin p + sin q = 2 * cos ((p - q) / 2) * sin ((p + q) / 2). -Proof. - intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2). - rewrite sin_plus; rewrite sin_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. -Qed. - -Lemma form4 : - forall p q:R, sin p - sin q = 2 * cos ((p + q) / 2) * sin ((p - q) / 2). -Proof. - intros p q; pattern p at 1 in |- *; - replace p with ((p - q) / 2 + (p + q) / 2). - pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2). - rewrite sin_plus; rewrite sin_minus; ring. - pattern q at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - pattern p at 3 in |- *; rewrite double_var; unfold Rdiv in |- *; ring. - -Qed. - -Lemma sin_increasing_0 : - forall x y:R, - - (PI / 2) <= x -> - x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> sin x < sin y -> x < y. -Proof. - intros; cut (sin ((x - y) / 2) < 0). - intro H4; case (Rtotal_order ((x - y) / 2) 0); intro H5. - assert (Hyp : 0 < 2). - prove_sup0. - generalize (Rmult_lt_compat_l 2 ((x - y) / 2) 0 Hyp H5). - unfold Rdiv in |- *. - rewrite <- Rmult_assoc. - rewrite Rinv_r_simpl_m. - rewrite Rmult_0_r. - clear H5; intro H5; apply Rminus_lt; assumption. - discrR. - elim H5; intro H6. - rewrite H6 in H4; rewrite sin_0 in H4; elim (Rlt_irrefl 0 H4). - change (0 < (x - y) / 2) in H6; - generalize (Ropp_le_ge_contravar (- (PI / 2)) y H1). - rewrite Ropp_involutive. - intro H7; generalize (Rge_le (PI / 2) (- y) H7); clear H7; intro H7; - generalize (Rplus_le_compat x (PI / 2) (- y) (PI / 2) H0 H7). - rewrite <- double_var. - intro H8. - assert (Hyp : 0 < 2). - prove_sup0. - generalize - (Rmult_le_compat_l (/ 2) (x - y) PI - (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H8). - repeat rewrite (Rmult_comm (/ 2)). - intro H9; - generalize - (sin_gt_0 ((x - y) / 2) H6 - (Rle_lt_trans ((x - y) / 2) (PI / 2) PI H9 PI2_Rlt_PI)); - intro H10; - elim - (Rlt_irrefl (sin ((x - y) / 2)) - (Rlt_trans (sin ((x - y) / 2)) 0 (sin ((x - y) / 2)) H4 H10)). - generalize (Rlt_minus (sin x) (sin y) H3); clear H3; intro H3; - rewrite form4 in H3; - generalize (Rplus_le_compat x (PI / 2) y (PI / 2) H0 H2). - rewrite <- double_var. - assert (Hyp : 0 < 2). - prove_sup0. - intro H4; - generalize - (Rmult_le_compat_l (/ 2) (x + y) PI - (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H4). - repeat rewrite (Rmult_comm (/ 2)). - clear H4; intro H4; - generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) y H H1); - replace (- (PI / 2) + - (PI / 2)) with (- PI). - intro H5; - generalize - (Rmult_le_compat_l (/ 2) (- PI) (x + y) - (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H5). - replace (/ 2 * (x + y)) with ((x + y) / 2). - replace (/ 2 * - PI) with (- (PI / 2)). - clear H5; intro H5; elim H4; intro H40. - elim H5; intro H50. - generalize (cos_gt_0 ((x + y) / 2) H50 H40); intro H6; - generalize (Rmult_lt_compat_l 2 0 (cos ((x + y) / 2)) Hyp H6). - rewrite Rmult_0_r. - clear H6; intro H6; case (Rcase_abs (sin ((x - y) / 2))); intro H7. - assumption. - generalize (Rge_le (sin ((x - y) / 2)) 0 H7); clear H7; intro H7; - generalize - (Rmult_le_pos (2 * cos ((x + y) / 2)) (sin ((x - y) / 2)) - (Rlt_le 0 (2 * cos ((x + y) / 2)) H6) H7); intro H8; - generalize - (Rle_lt_trans 0 (2 * cos ((x + y) / 2) * sin ((x - y) / 2)) 0 H8 H3); - intro H9; elim (Rlt_irrefl 0 H9). - rewrite <- H50 in H3; rewrite cos_neg in H3; rewrite cos_PI2 in H3; - rewrite Rmult_0_r in H3; rewrite Rmult_0_l in H3; - elim (Rlt_irrefl 0 H3). - unfold Rdiv in H3. - rewrite H40 in H3; assert (H50 := cos_PI2); unfold Rdiv in H50; - rewrite H50 in H3; rewrite Rmult_0_r in H3; rewrite Rmult_0_l in H3; - elim (Rlt_irrefl 0 H3). - unfold Rdiv in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rmult_comm. - unfold Rdiv in |- *; apply Rmult_comm. - pattern PI at 1 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - reflexivity. -Qed. - -Lemma sin_increasing_1 : - forall x y:R, - - (PI / 2) <= x -> - x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> x < y -> sin x < sin y. -Proof. - intros; generalize (Rplus_lt_compat_l x x y H3); intro H4; - generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) x H H); - replace (- (PI / 2) + - (PI / 2)) with (- PI). - assert (Hyp : 0 < 2). - prove_sup0. - intro H5; generalize (Rle_lt_trans (- PI) (x + x) (x + y) H5 H4); intro H6; - generalize - (Rmult_lt_compat_l (/ 2) (- PI) (x + y) (Rinv_0_lt_compat 2 Hyp) H6); - replace (/ 2 * - PI) with (- (PI / 2)). - replace (/ 2 * (x + y)) with ((x + y) / 2). - clear H4 H5 H6; intro H4; generalize (Rplus_lt_compat_l y x y H3); intro H5; - rewrite Rplus_comm in H5; - generalize (Rplus_le_compat y (PI / 2) y (PI / 2) H2 H2). - rewrite <- double_var. - intro H6; generalize (Rlt_le_trans (x + y) (y + y) PI H5 H6); intro H7; - generalize (Rmult_lt_compat_l (/ 2) (x + y) PI (Rinv_0_lt_compat 2 Hyp) H7); - replace (/ 2 * PI) with (PI / 2). - replace (/ 2 * (x + y)) with ((x + y) / 2). - clear H5 H6 H7; intro H5; generalize (Ropp_le_ge_contravar (- (PI / 2)) y H1); - rewrite Ropp_involutive; clear H1; intro H1; - generalize (Rge_le (PI / 2) (- y) H1); clear H1; intro H1; - generalize (Ropp_le_ge_contravar y (PI / 2) H2); clear H2; - intro H2; generalize (Rge_le (- y) (- (PI / 2)) H2); - clear H2; intro H2; generalize (Rplus_lt_compat_l (- y) x y H3); - replace (- y + x) with (x - y). - rewrite Rplus_opp_l. - intro H6; - generalize (Rmult_lt_compat_l (/ 2) (x - y) 0 (Rinv_0_lt_compat 2 Hyp) H6); - rewrite Rmult_0_r; replace (/ 2 * (x - y)) with ((x - y) / 2). - clear H6; intro H6; - generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) (- y) H H2); - replace (- (PI / 2) + - (PI / 2)) with (- PI). - replace (x + - y) with (x - y). - intro H7; - generalize - (Rmult_le_compat_l (/ 2) (- PI) (x - y) - (Rlt_le 0 (/ 2) (Rinv_0_lt_compat 2 Hyp)) H7); - replace (/ 2 * - PI) with (- (PI / 2)). - replace (/ 2 * (x - y)) with ((x - y) / 2). - clear H7; intro H7; clear H H0 H1 H2; apply Rminus_lt; rewrite form4; - generalize (cos_gt_0 ((x + y) / 2) H4 H5); intro H8; - generalize (Rmult_lt_0_compat 2 (cos ((x + y) / 2)) Hyp H8); - clear H8; intro H8; cut (- PI < - (PI / 2)). - intro H9; - generalize - (sin_lt_0_var ((x - y) / 2) - (Rlt_le_trans (- PI) (- (PI / 2)) ((x - y) / 2) H9 H7) H6); - intro H10; - generalize - (Rmult_lt_gt_compat_neg_l (sin ((x - y) / 2)) 0 ( - 2 * cos ((x + y) / 2)) H10 H8); intro H11; rewrite Rmult_0_r in H11; - rewrite Rmult_comm; assumption. - apply Ropp_lt_gt_contravar; apply PI2_Rlt_PI. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse; apply Rmult_comm. - reflexivity. - pattern PI at 1 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - reflexivity. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rminus in |- *; apply Rplus_comm. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *; apply Rmult_comm. - unfold Rdiv in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rmult_comm. - pattern PI at 1 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - reflexivity. -Qed. - -Lemma sin_decreasing_0 : - forall x y:R, - x <= 3 * (PI / 2) -> - PI / 2 <= x -> y <= 3 * (PI / 2) -> PI / 2 <= y -> sin x < sin y -> y < x. -Proof. - intros; rewrite <- (sin_PI_x x) in H3; rewrite <- (sin_PI_x y) in H3; - generalize (Ropp_lt_gt_contravar (sin (PI - x)) (sin (PI - y)) H3); - repeat rewrite <- sin_neg; - generalize (Rplus_le_compat_l (- PI) x (3 * (PI / 2)) H); - generalize (Rplus_le_compat_l (- PI) (PI / 2) x H0); - generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1); - generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2); - replace (- PI + x) with (x - PI). - replace (- PI + PI / 2) with (- (PI / 2)). - replace (- PI + y) with (y - PI). - replace (- PI + 3 * (PI / 2)) with (PI / 2). - replace (- (PI - x)) with (x - PI). - replace (- (PI - y)) with (y - PI). - intros; change (sin (y - PI) < sin (x - PI)) in H8; - apply Rplus_lt_reg_r with (- PI); rewrite Rplus_comm; - replace (y + - PI) with (y - PI). - rewrite Rplus_comm; replace (x + - PI) with (x - PI). - apply (sin_increasing_0 (y - PI) (x - PI) H4 H5 H6 H7 H8). - reflexivity. - reflexivity. - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - ring. - unfold Rminus in |- *; apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var. - rewrite Ropp_plus_distr. - ring. - unfold Rminus in |- *; apply Rplus_comm. -Qed. - -Lemma sin_decreasing_1 : - forall x y:R, - x <= 3 * (PI / 2) -> - PI / 2 <= x -> y <= 3 * (PI / 2) -> PI / 2 <= y -> x < y -> sin y < sin x. -Proof. - intros; rewrite <- (sin_PI_x x); rewrite <- (sin_PI_x y); - generalize (Rplus_le_compat_l (- PI) x (3 * (PI / 2)) H); - generalize (Rplus_le_compat_l (- PI) (PI / 2) x H0); - generalize (Rplus_le_compat_l (- PI) y (3 * (PI / 2)) H1); - generalize (Rplus_le_compat_l (- PI) (PI / 2) y H2); - generalize (Rplus_lt_compat_l (- PI) x y H3); - replace (- PI + PI / 2) with (- (PI / 2)). - replace (- PI + y) with (y - PI). - replace (- PI + 3 * (PI / 2)) with (PI / 2). - replace (- PI + x) with (x - PI). - intros; apply Ropp_lt_cancel; repeat rewrite <- sin_neg; - replace (- (PI - x)) with (x - PI). - replace (- (PI - y)) with (y - PI). - apply (sin_increasing_1 (x - PI) (y - PI) H7 H8 H5 H6 H4). - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - unfold Rminus in |- *; rewrite Ropp_plus_distr. - rewrite Ropp_involutive. - apply Rplus_comm. - unfold Rminus in |- *; apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var; ring. - unfold Rminus in |- *; apply Rplus_comm. - pattern PI at 2 in |- *; rewrite double_var; ring. -Qed. - -Lemma cos_increasing_0 : - forall x y:R, - PI <= x -> x <= 2 * PI -> PI <= y -> y <= 2 * PI -> cos x < cos y -> x < y. -Proof. - intros x y H1 H2 H3 H4; rewrite <- (cos_neg x); rewrite <- (cos_neg y); - rewrite <- (cos_period (- x) 1); rewrite <- (cos_period (- y) 1); - unfold INR in |- *; - replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))). - replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))). - repeat rewrite cos_shift; intro H5; - generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI x H1); - generalize (Rplus_le_compat_l (-3 * (PI / 2)) x (2 * PI) H2); - generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI y H3); - generalize (Rplus_le_compat_l (-3 * (PI / 2)) y (2 * PI) H4). - replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)). - replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)). - replace (-3 * (PI / 2) + 2 * PI) with (PI / 2). - replace (-3 * (PI / 2) + PI) with (- (PI / 2)). - clear H1 H2 H3 H4; intros H1 H2 H3 H4; - apply Rplus_lt_reg_r with (-3 * (PI / 2)); - replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)). - replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)). - apply (sin_increasing_0 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H4 H3 H2 H1 H5). - unfold Rminus in |- *. - rewrite Ropp_mult_distr_l_reverse. - apply Rplus_comm. - unfold Rminus in |- *. - rewrite Ropp_mult_distr_l_reverse. - apply Rplus_comm. - pattern PI at 3 in |- *; rewrite double_var. - ring. - rewrite double; pattern PI at 3 4 in |- *; rewrite double_var. - ring. - unfold Rminus in |- *. - rewrite Ropp_mult_distr_l_reverse. - apply Rplus_comm. - unfold Rminus in |- *. - rewrite Ropp_mult_distr_l_reverse. - apply Rplus_comm. - rewrite Rmult_1_r. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - rewrite Rmult_1_r. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. -Qed. - -Lemma cos_increasing_1 : - forall x y:R, - PI <= x -> x <= 2 * PI -> PI <= y -> y <= 2 * PI -> x < y -> cos x < cos y. -Proof. - intros x y H1 H2 H3 H4 H5; - generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI x H1); - generalize (Rplus_le_compat_l (-3 * (PI / 2)) x (2 * PI) H2); - generalize (Rplus_le_compat_l (-3 * (PI / 2)) PI y H3); - generalize (Rplus_le_compat_l (-3 * (PI / 2)) y (2 * PI) H4); - generalize (Rplus_lt_compat_l (-3 * (PI / 2)) x y H5); - rewrite <- (cos_neg x); rewrite <- (cos_neg y); - rewrite <- (cos_period (- x) 1); rewrite <- (cos_period (- y) 1); - unfold INR in |- *; replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)). - replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)). - replace (-3 * (PI / 2) + PI) with (- (PI / 2)). - replace (-3 * (PI / 2) + 2 * PI) with (PI / 2). - clear H1 H2 H3 H4 H5; intros H1 H2 H3 H4 H5; - replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))). - replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))). - repeat rewrite cos_shift; - apply - (sin_increasing_1 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H5 H4 H3 H2 H1). - rewrite Rmult_1_r. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - rewrite Rmult_1_r. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite double_var. - ring. - pattern PI at 3 in |- *; rewrite double_var; ring. - unfold Rminus in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rplus_comm. - unfold Rminus in |- *. - rewrite <- Ropp_mult_distr_l_reverse. - apply Rplus_comm. -Qed. - -Lemma cos_decreasing_0 : - forall x y:R, - 0 <= x -> x <= PI -> 0 <= y -> y <= PI -> cos x < cos y -> y < x. -Proof. - intros; generalize (Ropp_lt_gt_contravar (cos x) (cos y) H3); - repeat rewrite <- neg_cos; intro H4; - change (cos (y + PI) < cos (x + PI)) in H4; rewrite (Rplus_comm x) in H4; - rewrite (Rplus_comm y) in H4; generalize (Rplus_le_compat_l PI 0 x H); - generalize (Rplus_le_compat_l PI x PI H0); - generalize (Rplus_le_compat_l PI 0 y H1); - generalize (Rplus_le_compat_l PI y PI H2); rewrite Rplus_0_r. - rewrite <- double. - clear H H0 H1 H2 H3; intros; apply Rplus_lt_reg_r with PI; - apply (cos_increasing_0 (PI + y) (PI + x) H0 H H2 H1 H4). -Qed. - -Lemma cos_decreasing_1 : - forall x y:R, - 0 <= x -> x <= PI -> 0 <= y -> y <= PI -> x < y -> cos y < cos x. -Proof. - intros; apply Ropp_lt_cancel; repeat rewrite <- neg_cos; - rewrite (Rplus_comm x); rewrite (Rplus_comm y); - generalize (Rplus_le_compat_l PI 0 x H); - generalize (Rplus_le_compat_l PI x PI H0); - generalize (Rplus_le_compat_l PI 0 y H1); - generalize (Rplus_le_compat_l PI y PI H2); rewrite Rplus_0_r. - rewrite <- double. - generalize (Rplus_lt_compat_l PI x y H3); clear H H0 H1 H2 H3; intros; - apply (cos_increasing_1 (PI + x) (PI + y) H3 H2 H1 H0 H). -Qed. - -Lemma tan_diff : - forall x y:R, - cos x <> 0 -> cos y <> 0 -> tan x - tan y = sin (x - y) / (cos x * cos y). -Proof. - intros; unfold tan in |- *; rewrite sin_minus. - unfold Rdiv in |- *. - unfold Rminus in |- *. - rewrite Rmult_plus_distr_r. - rewrite Rinv_mult_distr. - repeat rewrite (Rmult_comm (sin x)). - repeat rewrite Rmult_assoc. - rewrite (Rmult_comm (cos y)). - repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - rewrite (Rmult_comm (sin x)). - apply Rplus_eq_compat_l. - rewrite <- Ropp_mult_distr_l_reverse. - rewrite <- Ropp_mult_distr_r_reverse. - rewrite (Rmult_comm (/ cos x)). - repeat rewrite Rmult_assoc. - rewrite (Rmult_comm (cos x)). - repeat rewrite Rmult_assoc. - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r. - reflexivity. - assumption. - assumption. - assumption. - assumption. -Qed. - -Lemma tan_increasing_0 : - forall x y:R, - - (PI / 4) <= x -> - x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> tan x < tan y -> x < y. -Proof. - intros; generalize PI4_RLT_PI2; intro H4; - generalize (Ropp_lt_gt_contravar (PI / 4) (PI / 2) H4); - intro H5; change (- (PI / 2) < - (PI / 4)) in H5; - generalize - (cos_gt_0 x (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) x H5 H) - (Rle_lt_trans x (PI / 4) (PI / 2) H0 H4)); intro HP1; - generalize - (cos_gt_0 y (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) y H5 H1) - (Rle_lt_trans y (PI / 4) (PI / 2) H2 H4)); intro HP2; - generalize - (sym_not_eq - (Rlt_not_eq 0 (cos x) - (cos_gt_0 x (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) x H5 H) - (Rle_lt_trans x (PI / 4) (PI / 2) H0 H4)))); - intro H6; - generalize - (sym_not_eq - (Rlt_not_eq 0 (cos y) - (cos_gt_0 y (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) y H5 H1) - (Rle_lt_trans y (PI / 4) (PI / 2) H2 H4)))); - intro H7; generalize (tan_diff x y H6 H7); intro H8; - generalize (Rlt_minus (tan x) (tan y) H3); clear H3; - intro H3; rewrite H8 in H3; cut (sin (x - y) < 0). - intro H9; generalize (Ropp_le_ge_contravar (- (PI / 4)) y H1); - rewrite Ropp_involutive; intro H10; generalize (Rge_le (PI / 4) (- y) H10); - clear H10; intro H10; generalize (Ropp_le_ge_contravar y (PI / 4) H2); - intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11); - clear H11; intro H11; - generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11); - generalize (Rplus_le_compat x (PI / 4) (- y) (PI / 4) H0 H10); - replace (x + - y) with (x - y). - replace (PI / 4 + PI / 4) with (PI / 2). - replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)). - intros; case (Rtotal_order 0 (x - y)); intro H14. - generalize - (sin_gt_0 (x - y) H14 (Rle_lt_trans (x - y) (PI / 2) PI H12 PI2_Rlt_PI)); - intro H15; elim (Rlt_irrefl 0 (Rlt_trans 0 (sin (x - y)) 0 H15 H9)). - elim H14; intro H15. - rewrite <- H15 in H9; rewrite sin_0 in H9; elim (Rlt_irrefl 0 H9). - apply Rminus_lt; assumption. - pattern PI at 1 in |- *; rewrite double_var. - unfold Rdiv in |- *. - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - rewrite Ropp_plus_distr. - replace 4 with 4. - reflexivity. - ring. - discrR. - discrR. - pattern PI at 1 in |- *; rewrite double_var. - unfold Rdiv in |- *. - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - replace 4 with 4. - reflexivity. - ring. - discrR. - discrR. - reflexivity. - case (Rcase_abs (sin (x - y))); intro H9. - assumption. - generalize (Rge_le (sin (x - y)) 0 H9); clear H9; intro H9; - generalize (Rinv_0_lt_compat (cos x) HP1); intro H10; - generalize (Rinv_0_lt_compat (cos y) HP2); intro H11; - generalize (Rmult_lt_0_compat (/ cos x) (/ cos y) H10 H11); - replace (/ cos x * / cos y) with (/ (cos x * cos y)). - intro H12; - generalize - (Rmult_le_pos (sin (x - y)) (/ (cos x * cos y)) H9 - (Rlt_le 0 (/ (cos x * cos y)) H12)); intro H13; - elim - (Rlt_irrefl 0 (Rle_lt_trans 0 (sin (x - y) * / (cos x * cos y)) 0 H13 H3)). - rewrite Rinv_mult_distr. - reflexivity. - assumption. - assumption. -Qed. - -Lemma tan_increasing_1 : - forall x y:R, - - (PI / 4) <= x -> - x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> x < y -> tan x < tan y. -Proof. - intros; apply Rminus_lt; generalize PI4_RLT_PI2; intro H4; - generalize (Ropp_lt_gt_contravar (PI / 4) (PI / 2) H4); - intro H5; change (- (PI / 2) < - (PI / 4)) in H5; - generalize - (cos_gt_0 x (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) x H5 H) - (Rle_lt_trans x (PI / 4) (PI / 2) H0 H4)); intro HP1; - generalize - (cos_gt_0 y (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) y H5 H1) - (Rle_lt_trans y (PI / 4) (PI / 2) H2 H4)); intro HP2; - generalize - (sym_not_eq - (Rlt_not_eq 0 (cos x) - (cos_gt_0 x (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) x H5 H) - (Rle_lt_trans x (PI / 4) (PI / 2) H0 H4)))); - intro H6; - generalize - (sym_not_eq - (Rlt_not_eq 0 (cos y) - (cos_gt_0 y (Rlt_le_trans (- (PI / 2)) (- (PI / 4)) y H5 H1) - (Rle_lt_trans y (PI / 4) (PI / 2) H2 H4)))); - intro H7; rewrite (tan_diff x y H6 H7); - generalize (Rinv_0_lt_compat (cos x) HP1); intro H10; - generalize (Rinv_0_lt_compat (cos y) HP2); intro H11; - generalize (Rmult_lt_0_compat (/ cos x) (/ cos y) H10 H11); - replace (/ cos x * / cos y) with (/ (cos x * cos y)). - clear H10 H11; intro H8; generalize (Ropp_le_ge_contravar y (PI / 4) H2); - intro H11; generalize (Rge_le (- y) (- (PI / 4)) H11); - clear H11; intro H11; - generalize (Rplus_le_compat (- (PI / 4)) x (- (PI / 4)) (- y) H H11); - replace (x + - y) with (x - y). - replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)). - clear H11; intro H9; generalize (Rlt_minus x y H3); clear H3; intro H3; - clear H H0 H1 H2 H4 H5 HP1 HP2; generalize PI2_Rlt_PI; - intro H1; generalize (Ropp_lt_gt_contravar (PI / 2) PI H1); - clear H1; intro H1; - generalize - (sin_lt_0_var (x - y) (Rlt_le_trans (- PI) (- (PI / 2)) (x - y) H1 H9) H3); - intro H2; - generalize - (Rmult_lt_gt_compat_neg_l (sin (x - y)) 0 (/ (cos x * cos y)) H2 H8); - rewrite Rmult_0_r; intro H4; assumption. - pattern PI at 1 in |- *; rewrite double_var. - unfold Rdiv in |- *. - rewrite Rmult_plus_distr_r. - repeat rewrite Rmult_assoc. - rewrite <- Rinv_mult_distr. - replace 4 with 4. - rewrite Ropp_plus_distr. - reflexivity. - ring. - discrR. - discrR. - reflexivity. - apply Rinv_mult_distr; assumption. -Qed. - -Lemma sin_incr_0 : - forall x y:R, - - (PI / 2) <= x -> - x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> sin x <= sin y -> x <= y. -Proof. - intros; case (Rtotal_order (sin x) (sin y)); intro H4; - [ left; apply (sin_increasing_0 x y H H0 H1 H2 H4) - | elim H4; intro H5; - [ case (Rtotal_order x y); intro H6; - [ left; assumption - | elim H6; intro H7; - [ right; assumption - | generalize (sin_increasing_1 y x H1 H2 H H0 H7); intro H8; - rewrite H5 in H8; elim (Rlt_irrefl (sin y) H8) ] ] - | elim (Rlt_irrefl (sin x) (Rle_lt_trans (sin x) (sin y) (sin x) H3 H5)) ] ]. -Qed. - -Lemma sin_incr_1 : - forall x y:R, - - (PI / 2) <= x -> - x <= PI / 2 -> - (PI / 2) <= y -> y <= PI / 2 -> x <= y -> sin x <= sin y. -Proof. - intros; case (Rtotal_order x y); intro H4; - [ left; apply (sin_increasing_1 x y H H0 H1 H2 H4) - | elim H4; intro H5; - [ case (Rtotal_order (sin x) (sin y)); intro H6; - [ left; assumption - | elim H6; intro H7; - [ right; assumption - | generalize (sin_increasing_0 y x H1 H2 H H0 H7); intro H8; - rewrite H5 in H8; elim (Rlt_irrefl y H8) ] ] - | elim (Rlt_irrefl x (Rle_lt_trans x y x H3 H5)) ] ]. -Qed. - -Lemma sin_decr_0 : - forall x y:R, - x <= 3 * (PI / 2) -> - PI / 2 <= x -> - y <= 3 * (PI / 2) -> PI / 2 <= y -> sin x <= sin y -> y <= x. -Proof. - intros; case (Rtotal_order (sin x) (sin y)); intro H4; - [ left; apply (sin_decreasing_0 x y H H0 H1 H2 H4) - | elim H4; intro H5; - [ case (Rtotal_order x y); intro H6; - [ generalize (sin_decreasing_1 x y H H0 H1 H2 H6); intro H8; - rewrite H5 in H8; elim (Rlt_irrefl (sin y) H8) - | elim H6; intro H7; - [ right; symmetry in |- *; assumption | left; assumption ] ] - | elim (Rlt_irrefl (sin x) (Rle_lt_trans (sin x) (sin y) (sin x) H3 H5)) ] ]. -Qed. - -Lemma sin_decr_1 : - forall x y:R, - x <= 3 * (PI / 2) -> - PI / 2 <= x -> - y <= 3 * (PI / 2) -> PI / 2 <= y -> x <= y -> sin y <= sin x. -Proof. - intros; case (Rtotal_order x y); intro H4; - [ left; apply (sin_decreasing_1 x y H H0 H1 H2 H4) - | elim H4; intro H5; - [ case (Rtotal_order (sin x) (sin y)); intro H6; - [ generalize (sin_decreasing_0 x y H H0 H1 H2 H6); intro H8; - rewrite H5 in H8; elim (Rlt_irrefl y H8) - | elim H6; intro H7; - [ right; symmetry in |- *; assumption | left; assumption ] ] - | elim (Rlt_irrefl x (Rle_lt_trans x y x H3 H5)) ] ]. -Qed. - -Lemma cos_incr_0 : - forall x y:R, - PI <= x -> - x <= 2 * PI -> PI <= y -> y <= 2 * PI -> cos x <= cos y -> x <= y. -Proof. - intros; case (Rtotal_order (cos x) (cos y)); intro H4; - [ left; apply (cos_increasing_0 x y H H0 H1 H2 H4) - | elim H4; intro H5; - [ case (Rtotal_order x y); intro H6; - [ left; assumption - | elim H6; intro H7; - [ right; assumption - | generalize (cos_increasing_1 y x H1 H2 H H0 H7); intro H8; - rewrite H5 in H8; elim (Rlt_irrefl (cos y) H8) ] ] - | elim (Rlt_irrefl (cos x) (Rle_lt_trans (cos x) (cos y) (cos x) H3 H5)) ] ]. -Qed. - -Lemma cos_incr_1 : - forall x y:R, - PI <= x -> - x <= 2 * PI -> PI <= y -> y <= 2 * PI -> x <= y -> cos x <= cos y. -Proof. - intros; case (Rtotal_order x y); intro H4; - [ left; apply (cos_increasing_1 x y H H0 H1 H2 H4) - | elim H4; intro H5; - [ case (Rtotal_order (cos x) (cos y)); intro H6; - [ left; assumption - | elim H6; intro H7; - [ right; assumption - | generalize (cos_increasing_0 y x H1 H2 H H0 H7); intro H8; - rewrite H5 in H8; elim (Rlt_irrefl y H8) ] ] - | elim (Rlt_irrefl x (Rle_lt_trans x y x H3 H5)) ] ]. -Qed. - -Lemma cos_decr_0 : - forall x y:R, - 0 <= x -> x <= PI -> 0 <= y -> y <= PI -> cos x <= cos y -> y <= x. -Proof. - intros; case (Rtotal_order (cos x) (cos y)); intro H4; - [ left; apply (cos_decreasing_0 x y H H0 H1 H2 H4) - | elim H4; intro H5; - [ case (Rtotal_order x y); intro H6; - [ generalize (cos_decreasing_1 x y H H0 H1 H2 H6); intro H8; - rewrite H5 in H8; elim (Rlt_irrefl (cos y) H8) - | elim H6; intro H7; - [ right; symmetry in |- *; assumption | left; assumption ] ] - | elim (Rlt_irrefl (cos x) (Rle_lt_trans (cos x) (cos y) (cos x) H3 H5)) ] ]. -Qed. - -Lemma cos_decr_1 : - forall x y:R, - 0 <= x -> x <= PI -> 0 <= y -> y <= PI -> x <= y -> cos y <= cos x. -Proof. - intros; case (Rtotal_order x y); intro H4; - [ left; apply (cos_decreasing_1 x y H H0 H1 H2 H4) - | elim H4; intro H5; - [ case (Rtotal_order (cos x) (cos y)); intro H6; - [ generalize (cos_decreasing_0 x y H H0 H1 H2 H6); intro H8; - rewrite H5 in H8; elim (Rlt_irrefl y H8) - | elim H6; intro H7; - [ right; symmetry in |- *; assumption | left; assumption ] ] - | elim (Rlt_irrefl x (Rle_lt_trans x y x H3 H5)) ] ]. -Qed. - -Lemma tan_incr_0 : - forall x y:R, - - (PI / 4) <= x -> - x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> tan x <= tan y -> x <= y. -Proof. - intros; case (Rtotal_order (tan x) (tan y)); intro H4; - [ left; apply (tan_increasing_0 x y H H0 H1 H2 H4) - | elim H4; intro H5; - [ case (Rtotal_order x y); intro H6; - [ left; assumption - | elim H6; intro H7; - [ right; assumption - | generalize (tan_increasing_1 y x H1 H2 H H0 H7); intro H8; - rewrite H5 in H8; elim (Rlt_irrefl (tan y) H8) ] ] - | elim (Rlt_irrefl (tan x) (Rle_lt_trans (tan x) (tan y) (tan x) H3 H5)) ] ]. -Qed. - -Lemma tan_incr_1 : - forall x y:R, - - (PI / 4) <= x -> - x <= PI / 4 -> - (PI / 4) <= y -> y <= PI / 4 -> x <= y -> tan x <= tan y. -Proof. - intros; case (Rtotal_order x y); intro H4; - [ left; apply (tan_increasing_1 x y H H0 H1 H2 H4) - | elim H4; intro H5; - [ case (Rtotal_order (tan x) (tan y)); intro H6; - [ left; assumption - | elim H6; intro H7; - [ right; assumption - | generalize (tan_increasing_0 y x H1 H2 H H0 H7); intro H8; - rewrite H5 in H8; elim (Rlt_irrefl y H8) ] ] - | elim (Rlt_irrefl x (Rle_lt_trans x y x H3 H5)) ] ]. -Qed. - -(**********) -Lemma sin_eq_0_1 : forall x:R, (exists k : Z, x = IZR k * PI) -> sin x = 0. -Proof. - intros. - elim H; intros. - apply (Zcase_sign x0). - intro. - rewrite H1 in H0. - simpl in H0. - rewrite H0; rewrite Rmult_0_l; apply sin_0. - intro. - cut (0 <= x0)%Z. - intro. - elim (IZN x0 H2); intros. - rewrite H3 in H0. - rewrite <- INR_IZR_INZ in H0. - rewrite H0. - elim (even_odd_cor x1); intros. - elim H4; intro. - rewrite H5. - rewrite mult_INR. - simpl in |- *. - rewrite <- (Rplus_0_l (2 * INR x2 * PI)). - rewrite sin_period. - apply sin_0. - rewrite H5. - rewrite S_INR; rewrite mult_INR. - simpl in |- *. - rewrite Rmult_plus_distr_r. - rewrite Rmult_1_l; rewrite sin_plus. - rewrite sin_PI. - rewrite Rmult_0_r. - rewrite <- (Rplus_0_l (2 * INR x2 * PI)). - rewrite sin_period. - rewrite sin_0; ring. - apply le_IZR. - left; apply IZR_lt. - assert (H2 := Zorder.Zgt_iff_lt). - elim (H2 x0 0%Z); intros. - apply H3; assumption. - intro. - rewrite H0. - replace (sin (IZR x0 * PI)) with (- sin (- IZR x0 * PI)). - cut (0 <= - x0)%Z. - intro. - rewrite <- Ropp_Ropp_IZR. - elim (IZN (- x0) H2); intros. - rewrite H3. - rewrite <- INR_IZR_INZ. - elim (even_odd_cor x1); intros. - elim H4; intro. - rewrite H5. - rewrite mult_INR. - simpl in |- *. - rewrite <- (Rplus_0_l (2 * INR x2 * PI)). - rewrite sin_period. - rewrite sin_0; ring. - rewrite H5. - rewrite S_INR; rewrite mult_INR. - simpl in |- *. - rewrite Rmult_plus_distr_r. - rewrite Rmult_1_l; rewrite sin_plus. - rewrite sin_PI. - rewrite Rmult_0_r. - rewrite <- (Rplus_0_l (2 * INR x2 * PI)). - rewrite sin_period. - rewrite sin_0; ring. - apply le_IZR. - apply Rplus_le_reg_l with (IZR x0). - rewrite Rplus_0_r. - rewrite Ropp_Ropp_IZR. - rewrite Rplus_opp_r. - left; replace 0 with (IZR 0); [ apply IZR_lt | reflexivity ]. - assumption. - rewrite <- sin_neg. - rewrite Ropp_mult_distr_l_reverse. - rewrite Ropp_involutive. - reflexivity. -Qed. - -Lemma sin_eq_0_0 : forall x:R, sin x = 0 -> exists k : Z, x = IZR k * PI. -Proof. - intros. - assert (H0 := euclidian_division x PI PI_neq0). - elim H0; intros q H1. - elim H1; intros r H2. - exists q. - cut (r = 0). - intro. - elim H2; intros H4 _; rewrite H4; rewrite H3. - apply Rplus_0_r. - elim H2; intros. - rewrite H3 in H. - rewrite sin_plus in H. - cut (sin (IZR q * PI) = 0). - intro. - rewrite H5 in H. - rewrite Rmult_0_l in H. - rewrite Rplus_0_l in H. - assert (H6 := Rmult_integral _ _ H). - elim H6; intro. - assert (H8 := sin2_cos2 (IZR q * PI)). - rewrite H5 in H8; rewrite H7 in H8. - rewrite Rsqr_0 in H8. - rewrite Rplus_0_r in H8. - elim R1_neq_R0; symmetry in |- *; assumption. - cut (r = 0 \/ 0 < r < PI). - intro; elim H8; intro. - assumption. - elim H9; intros. - assert (H12 := sin_gt_0 _ H10 H11). - rewrite H7 in H12; elim (Rlt_irrefl _ H12). - rewrite Rabs_right in H4. - elim H4; intros. - case (Rtotal_order 0 r); intro. - right; split; assumption. - elim H10; intro. - left; symmetry in |- *; assumption. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H8 H11)). - apply Rle_ge. - left; apply PI_RGT_0. - apply sin_eq_0_1. - exists q; reflexivity. -Qed. - -Lemma cos_eq_0_0 : - forall x:R, cos x = 0 -> exists k : Z, x = IZR k * PI + PI / 2. -Proof. - intros x H; rewrite cos_sin in H; generalize (sin_eq_0_0 (PI / INR 2 + x) H); - intro H2; elim H2; intros x0 H3; exists (x0 - Z_of_nat 1)%Z; - rewrite <- Z_R_minus; simpl. -unfold INR in H3. field_simplify [(sym_eq H3)]. field. -(** - ring_simplify. - (* rewrite (Rmult_comm PI);*) (* old ring compat *) - rewrite <- H3; simpl; - field;repeat split; discrR. -*) -Qed. - -Lemma cos_eq_0_1 : - forall x:R, (exists k : Z, x = IZR k * PI + PI / 2) -> cos x = 0. -Proof. - intros x H1; rewrite cos_sin; elim H1; intros x0 H2; rewrite H2; - replace (PI / 2 + (IZR x0 * PI + PI / 2)) with (IZR x0 * PI + PI). - rewrite neg_sin; rewrite <- Ropp_0. - apply Ropp_eq_compat; apply sin_eq_0_1; exists x0; reflexivity. - pattern PI at 2 in |- *; rewrite (double_var PI); ring. -Qed. - -Lemma sin_eq_O_2PI_0 : - forall x:R, - 0 <= x -> x <= 2 * PI -> sin x = 0 -> x = 0 \/ x = PI \/ x = 2 * PI. -Proof. - intros; generalize (sin_eq_0_0 x H1); intro. - elim H2; intros k0 H3. - case (Rtotal_order PI x); intro. - rewrite H3 in H4; rewrite H3 in H0. - right; right. - generalize - (Rmult_lt_compat_r (/ PI) PI (IZR k0 * PI) (Rinv_0_lt_compat PI PI_RGT_0) H4); - rewrite Rmult_assoc; repeat rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; intro; - generalize - (Rmult_le_compat_r (/ PI) (IZR k0 * PI) (2 * PI) - (Rlt_le 0 (/ PI) (Rinv_0_lt_compat PI PI_RGT_0)) H0); - repeat rewrite Rmult_assoc; repeat rewrite <- Rinv_r_sym. - repeat rewrite Rmult_1_r; intro; - generalize (Rplus_lt_compat_l (IZR (-2)) 1 (IZR k0) H5); - rewrite <- plus_IZR. - replace (IZR (-2) + 1) with (-1). - intro; generalize (Rplus_le_compat_l (IZR (-2)) (IZR k0) 2 H6); - rewrite <- plus_IZR. - replace (IZR (-2) + 2) with 0. - intro; cut (-1 < IZR (-2 + k0) < 1). - intro; generalize (one_IZR_lt1 (-2 + k0) H9); intro. - cut (k0 = 2%Z). - intro; rewrite H11 in H3; rewrite H3; simpl in |- *. - reflexivity. - rewrite <- (Zplus_opp_l 2) in H10; generalize (Zplus_reg_l (-2) k0 2 H10); - intro; assumption. - split. - assumption. - apply Rle_lt_trans with 0. - assumption. - apply Rlt_0_1. - simpl in |- *; ring. - simpl in |- *; ring. - apply PI_neq0. - apply PI_neq0. - elim H4; intro. - right; left. - symmetry in |- *; assumption. - left. - rewrite H3 in H5; rewrite H3 in H; - generalize - (Rmult_lt_compat_r (/ PI) (IZR k0 * PI) PI (Rinv_0_lt_compat PI PI_RGT_0) - H5); rewrite Rmult_assoc; repeat rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; intro; - generalize - (Rmult_le_compat_r (/ PI) 0 (IZR k0 * PI) - (Rlt_le 0 (/ PI) (Rinv_0_lt_compat PI PI_RGT_0)) H); - repeat rewrite Rmult_assoc; repeat rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; rewrite Rmult_0_l; intro. - cut (-1 < IZR k0 < 1). - intro; generalize (one_IZR_lt1 k0 H8); intro; rewrite H9 in H3; rewrite H3; - simpl in |- *; apply Rmult_0_l. - split. - apply Rlt_le_trans with 0. - rewrite <- Ropp_0; apply Ropp_gt_lt_contravar; apply Rlt_0_1. - assumption. - assumption. - apply PI_neq0. - apply PI_neq0. -Qed. - -Lemma sin_eq_O_2PI_1 : - forall x:R, - 0 <= x -> x <= 2 * PI -> x = 0 \/ x = PI \/ x = 2 * PI -> sin x = 0. -Proof. - intros x H1 H2 H3; elim H3; intro H4; - [ rewrite H4; rewrite sin_0; reflexivity - | elim H4; intro H5; - [ rewrite H5; rewrite sin_PI; reflexivity - | rewrite H5; rewrite sin_2PI; reflexivity ] ]. -Qed. - -Lemma cos_eq_0_2PI_0 : - forall x:R, - 0 <= x -> x <= 2 * PI -> cos x = 0 -> x = PI / 2 \/ x = 3 * (PI / 2). -Proof. - intros; case (Rtotal_order x (3 * (PI / 2))); intro. - rewrite cos_sin in H1. - cut (0 <= PI / 2 + x). - cut (PI / 2 + x <= 2 * PI). - intros; generalize (sin_eq_O_2PI_0 (PI / 2 + x) H4 H3 H1); intros. - decompose [or] H5. - generalize (Rplus_le_compat_l (PI / 2) 0 x H); rewrite Rplus_0_r; rewrite H6; - intro. - elim (Rlt_irrefl 0 (Rlt_le_trans 0 (PI / 2) 0 PI2_RGT_0 H7)). - left. - generalize (Rplus_eq_compat_l (- (PI / 2)) (PI / 2 + x) PI H7). - replace (- (PI / 2) + (PI / 2 + x)) with x. - replace (- (PI / 2) + PI) with (PI / 2). - intro; assumption. - pattern PI at 3 in |- *; rewrite (double_var PI); ring. - ring. - right. - generalize (Rplus_eq_compat_l (- (PI / 2)) (PI / 2 + x) (2 * PI) H7). - replace (- (PI / 2) + (PI / 2 + x)) with x. - replace (- (PI / 2) + 2 * PI) with (3 * (PI / 2)). - intro; assumption. - rewrite double; pattern PI at 3 4 in |- *; rewrite (double_var PI); ring. - ring. - left; replace (2 * PI) with (PI / 2 + 3 * (PI / 2)). - apply Rplus_lt_compat_l; assumption. - rewrite (double PI); pattern PI at 3 4 in |- *; rewrite (double_var PI); ring. - apply Rplus_le_le_0_compat. - left; unfold Rdiv in |- *; apply Rmult_lt_0_compat. - apply PI_RGT_0. - apply Rinv_0_lt_compat; prove_sup0. - assumption. - elim H2; intro. - right; assumption. - generalize (cos_eq_0_0 x H1); intro; elim H4; intros k0 H5. - rewrite H5 in H3; rewrite H5 in H0; - generalize - (Rplus_lt_compat_l (- (PI / 2)) (3 * (PI / 2)) (IZR k0 * PI + PI / 2) H3); - generalize - (Rplus_le_compat_l (- (PI / 2)) (IZR k0 * PI + PI / 2) (2 * PI) H0). - replace (- (PI / 2) + 3 * (PI / 2)) with PI. - replace (- (PI / 2) + (IZR k0 * PI + PI / 2)) with (IZR k0 * PI). - replace (- (PI / 2) + 2 * PI) with (3 * (PI / 2)). - intros; - generalize - (Rmult_lt_compat_l (/ PI) PI (IZR k0 * PI) (Rinv_0_lt_compat PI PI_RGT_0) - H7); - generalize - (Rmult_le_compat_l (/ PI) (IZR k0 * PI) (3 * (PI / 2)) - (Rlt_le 0 (/ PI) (Rinv_0_lt_compat PI PI_RGT_0)) H6). - replace (/ PI * (IZR k0 * PI)) with (IZR k0). - replace (/ PI * (3 * (PI / 2))) with (3 * / 2). - rewrite <- Rinv_l_sym. - intros; generalize (Rplus_lt_compat_l (IZR (-2)) 1 (IZR k0) H9); - rewrite <- plus_IZR. - replace (IZR (-2) + 1) with (-1). - intro; generalize (Rplus_le_compat_l (IZR (-2)) (IZR k0) (3 * / 2) H8); - rewrite <- plus_IZR. - replace (IZR (-2) + 2) with 0. - intro; cut (-1 < IZR (-2 + k0) < 1). - intro; generalize (one_IZR_lt1 (-2 + k0) H12); intro. - cut (k0 = 2%Z). - intro; rewrite H14 in H8. - assert (Hyp : 0 < 2). - prove_sup0. - generalize (Rmult_le_compat_l 2 (IZR 2) (3 * / 2) (Rlt_le 0 2 Hyp) H8); - simpl in |- *. - replace 4 with 4. - replace (2 * (3 * / 2)) with 3. - intro; cut (3 < 4). - intro; elim (Rlt_irrefl 3 (Rlt_le_trans 3 4 3 H16 H15)). - generalize (Rplus_lt_compat_l 3 0 1 Rlt_0_1); rewrite Rplus_0_r. - replace (3 + 1) with 4. - intro; assumption. - ring. - symmetry in |- *; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m. - discrR. - ring. - rewrite <- (Zplus_opp_l 2) in H13; generalize (Zplus_reg_l (-2) k0 2 H13); - intro; assumption. - split. - assumption. - apply Rle_lt_trans with (IZR (-2) + 3 * / 2). - assumption. - simpl in |- *; replace (-2 + 3 * / 2) with (- (1 * / 2)). - apply Rlt_trans with 0. - rewrite <- Ropp_0; apply Ropp_lt_gt_contravar. - apply Rmult_lt_0_compat; - [ apply Rlt_0_1 | apply Rinv_0_lt_compat; prove_sup0 ]. - apply Rlt_0_1. - rewrite Rmult_1_l; apply Rmult_eq_reg_l with 2. - rewrite Ropp_mult_distr_r_reverse; rewrite <- Rinv_r_sym. - rewrite Rmult_plus_distr_l; rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m. - ring. - discrR. - discrR. - discrR. - simpl in |- *; ring. - simpl in |- *; ring. - apply PI_neq0. - unfold Rdiv in |- *; pattern 3 at 1 in |- *; rewrite (Rmult_comm 3); - repeat rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_l; apply Rmult_comm. - apply PI_neq0. - symmetry in |- *; rewrite (Rmult_comm (/ PI)); rewrite Rmult_assoc; - rewrite <- Rinv_r_sym. - apply Rmult_1_r. - apply PI_neq0. - rewrite double; pattern PI at 3 4 in |- *; rewrite double_var; ring. - ring. - pattern PI at 1 in |- *; rewrite double_var; ring. -Qed. - -Lemma cos_eq_0_2PI_1 : - forall x:R, - 0 <= x -> x <= 2 * PI -> x = PI / 2 \/ x = 3 * (PI / 2) -> cos x = 0. -Proof. - intros x H1 H2 H3; elim H3; intro H4; - [ rewrite H4; rewrite cos_PI2; reflexivity - | rewrite H4; rewrite cos_3PI2; reflexivity ]. -Qed. +Require Export Rtrigo1. +Require Export Ratan. +Require Export Machin.
\ No newline at end of file |