(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * 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.
Require Import Rfunctions.
Require Import SeqSeries.
Require Export Rtrigo_fun.
Require Export Rtrigo_def.
Require Export Rtrigo_alt.
Require Export Cos_rel.
Require Export Cos_plus.
Require Import ZArith_base.
Require Import Zcomplements.
Require Import Lia.
Require Import Lra.
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 }.
intros (x,p).
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_inv.
rewrite Rabs_right.
reflexivity.
apply Rle_ge; apply Rle_0_sqr.
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_inv.
rewrite Rabs_mult; rewrite (pow_1_abs n); rewrite Rmult_1_l;
rewrite <- Rabs_inv.
rewrite Rinv_inv.
rewrite Rinv_mult.
rewrite Rabs_inv.
rewrite Rinv_inv.
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_inv.
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).
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) as (x1,HUn); case (exist_cos (Rsqr x)) as (x0,Hcos); intros.
symmetry; eapply UL_sequence.
apply HUn.
unfold cos_in, infinite_sum in Hcos; unfold Un_cv in |- *; intros.
elim (Hcos _ 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 lra.
assert (up1 : 7/8 <= 4) by lra.
assert (lo : -2 <= 7/8) by lra.
assert (up : 7/8 <= 2) by lra.
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.
unfold cos_term, sin_term; simpl fact; rewrite !INR_IZR_INZ.
simpl plus; simpl mult; simpl Z_of_nat.
field_simplify.
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].
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; lra).
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.
lra.
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; lra.
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); lra).
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 | lra ].
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; lra.
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; lra. Qed.
Lemma PI_4 : PI <= 4.
Proof. unfold PI; destruct pi2_int; lra. 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.
change (-1) with (-(1)) 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; [lra |].
replace ((-PI/2) * 2) with (-PI) by field.
assert (t := PI_4); lra.
apply Rle_trans with (1 := upper).
apply Rmult_le_reg_r with 2; [lra | ].
replace ((PI/2) * 2) with PI by field.
generalize PI_4; intros; lra.
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.
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.
repeat rewrite Rmult_assoc; repeat rewrite (Rmult_comm (sin x));
repeat rewrite <- Rmult_assoc.
repeat rewrite Rinv_r_simpl_m; [ reflexivity | 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.
ring.
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; destruct (Rle_dec (-1) (sin x)) as [Hle|Hnle].
destruct (Rle_dec (sin x) 1) as [Hle'|Hnle'].
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; change (-1) with (-(1)); 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);
change (-1) with (-(1));
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);
rewrite <- Rplus_assoc; change (-1) with (-(1)); 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_l 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_l 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 Nat.neq_0_lt_0.
assert (H2 := fact_neq_0 (2 * n + 1)).
red in |- *; intro; elim H2; assumption.
rewrite <- Rinv_r_sym.
apply Rmult_lt_reg_l with (INR (fact (2 * S n + 1))).
apply lt_INR_0; apply Nat.neq_0_lt_0.
assert (H2 := fact_neq_0 (2 * S n + 1)).
red in |- *; intro; elim H2; 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.
apply pos_INR.
simpl in |- *; rewrite Rmult_1_r; change 4 with (Rsqr 2);
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;
[ apply PI_4 | 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)))).
apply Rmult_lt_compat_l.
apply lt_INR_0; apply Nat.neq_0_lt_0.
assert (H2 := fact_neq_0 (2 * n + 1)).
red in |- *; intro; elim H2; assumption.
do 2 rewrite S_INR; rewrite plus_INR; rewrite mult_INR; set (x := INR n);
unfold INR in |- *.
replace (((1 + 1) * x + 1 + 1 + 1) * ((1 + 1) * x + 1 + 1)) with (4 * x * x + 10 * x + 6);
[ idtac | ring ].
apply Rplus_lt_reg_l 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.
apply pos_INR.
now apply IZR_lt.
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.
Proof.
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.
Proof.
intros; unfold cos_lb, cos_ub in |- *; apply (cos_bound a 1 H H0).
Qed.
(**********)
Lemma _PI2_RLT_0 : - (PI / 2) < 0.
Proof.
assert (H := PI_RGT_0).
lra.
Qed.
Lemma PI4_RLT_PI2 : PI / 4 < PI / 2.
Proof.
assert (H := PI_RGT_0).
lra.
Qed.
Lemma PI2_Rlt_PI : PI / 2 < PI.
Proof.
assert (H := PI_RGT_0).
lra.
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 + - (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.
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).
field.
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) by field.
unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_le_compat_l;
assumption.
unfold Rminus in |- *; rewrite Rplus_comm;
replace (PI / 2) with (- PI + 3 * (PI / 2)) by field.
apply Rplus_le_compat_l; assumption.
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) by field.
unfold Rminus in |- *; rewrite (Rplus_comm x); apply Rplus_lt_compat_l;
assumption.
unfold Rminus in |- *; rewrite Rplus_comm;
replace (PI / 2) with (- PI + 3 * (PI / 2)) by field.
apply Rplus_lt_compat_l; assumption.
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) by ring.
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) by field.
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).
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) by field.
rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2) by field.
rewrite cos_plus; rewrite cos_minus; 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) by field.
rewrite <- (cos_neg q); replace (- q) with ((p - q) / 2 - (p + q) / 2) by field.
rewrite cos_plus; rewrite cos_minus; 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) by field.
pattern q at 3 in |- *; replace q with ((p + q) / 2 - (p - q) / 2) by field.
rewrite sin_plus; rewrite sin_minus; 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) by field.
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) by apply Rmult_comm.
replace (/ 2 * - PI) with (- (PI / 2)) by field.
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).
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) by field.
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)) by field.
replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm.
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) by apply Rmult_comm.
replace (/ 2 * (x + y)) with ((x + y) / 2) by apply Rmult_comm.
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) by apply Rplus_comm.
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) by apply Rmult_comm.
clear H6; intro H6;
generalize (Rplus_le_compat (- (PI / 2)) x (- (PI / 2)) (- y) H H2);
replace (- (PI / 2) + - (PI / 2)) with (- PI) by field.
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)) by field.
replace (/ 2 * (x - y)) with ((x - y) / 2) by apply Rmult_comm.
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.
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) by apply Rplus_comm.
replace (- PI + PI / 2) with (- (PI / 2)) by field.
replace (- PI + y) with (y - PI) by apply Rplus_comm.
replace (- PI + 3 * (PI / 2)) with (PI / 2) by field.
replace (- (PI - x)) with (x - PI) by ring.
replace (- (PI - y)) with (y - PI) by ring.
intros; change (sin (y - PI) < sin (x - PI)) in H8;
apply Rplus_lt_reg_l with (- PI); rewrite Rplus_comm.
rewrite (Rplus_comm _ x).
apply (sin_increasing_0 (y - PI) (x - PI) H4 H5 H6 H7 H8).
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)) by field.
replace (- PI + y) with (y - PI) by apply Rplus_comm.
replace (- PI + 3 * (PI / 2)) with (PI / 2) by field.
replace (- PI + x) with (x - PI) by apply Rplus_comm.
intros; apply Ropp_lt_cancel; repeat rewrite <- sin_neg;
replace (- (PI - x)) with (x - PI) by ring.
replace (- (PI - y)) with (y - PI) by ring.
apply (sin_increasing_1 (x - PI) (y - PI) H7 H8 H5 H6 H4).
Qed.
Lemma sin_inj x y : -(PI/2) <= x <= PI/2 -> -(PI/2) <= y <= PI/2 -> sin x = sin y -> x = y.
Proof.
intros xP yP Hsin.
destruct (total_order_T x y) as [[H|H]|H]; auto.
- assert (sin x < sin y).
now apply sin_increasing_1; lra.
now lra.
- assert (sin y < sin x).
now apply sin_increasing_1; lra.
now lra.
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))) by field.
replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))) by field.
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)) by ring.
replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)) by ring.
replace (-3 * (PI / 2) + 2 * PI) with (PI / 2) by field.
replace (-3 * (PI / 2) + PI) with (- (PI / 2)) by field.
clear H1 H2 H3 H4; intros H1 H2 H3 H4;
apply Rplus_lt_reg_l with (-3 * (PI / 2));
replace (-3 * (PI / 2) + x) with (x - 3 * (PI / 2)) by ring.
replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)) by ring.
apply (sin_increasing_0 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H4 H3 H2 H1 H5).
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)) by ring.
replace (-3 * (PI / 2) + y) with (y - 3 * (PI / 2)) by ring.
replace (-3 * (PI / 2) + PI) with (- (PI / 2)) by field.
replace (-3 * (PI / 2) + 2 * PI) with (PI / 2) by field.
clear H1 H2 H3 H4 H5; intros H1 H2 H3 H4 H5;
replace (- x + 2 * 1 * PI) with (PI / 2 - (x - 3 * (PI / 2))) by field.
replace (- y + 2 * 1 * PI) with (PI / 2 - (y - 3 * (PI / 2))) by field.
repeat rewrite cos_shift;
apply
(sin_increasing_1 (x - 3 * (PI / 2)) (y - 3 * (PI / 2)) H5 H4 H3 H2 H1).
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_l 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 cos_inj x y : 0 <= x <= PI -> 0 <= y <= PI -> cos x = cos y -> x = y.
Proof.
intros xP yP Hcos.
destruct (total_order_T x y) as [[H|H]|H]; auto.
- assert (cos y < cos x).
now apply cos_decreasing_1; lra.
now lra.
- assert (cos x < cos y).
now apply cos_decreasing_1; lra.
now lra.
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.
field.
now split.
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
(not_eq_sym
(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
(not_eq_sym
(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 (PI / 4 + PI / 4) with (PI / 2) by field.
replace (- (PI / 4) + - (PI / 4)) with (- (PI / 2)) by field.
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.
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)).
apply Rinv_mult.
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
(not_eq_sym
(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
(not_eq_sym
(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 (- (PI / 4) + - (PI / 4)) with (- (PI / 2)) by field.
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.
apply Rinv_mult.
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 ((1 + 1) * 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 ((1 + 1) * INR x2 * PI)).
rewrite sin_period.
rewrite sin_0; ring.
apply le_IZR.
left; apply IZR_lt.
assert (H2 := Z.gt_lt_iff).
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 ((1 + 1) * 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 ((1 + 1) * 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.
now apply Rlt_le, IZR_lt.
rewrite <- sin_neg.
rewrite Ropp_mult_distr_l_reverse.
rewrite Ropp_involutive.
reflexivity.
Qed.
Lemma sin_eq_0_0 (x:R) : sin x = 0 -> exists k : Z, x = IZR k * PI.
Proof.
intros Hx.
destruct (euclidian_division x PI PI_neq0) as (q & r & EQ & Hr & Hr').
exists q.
rewrite <- (Rplus_0_r (_*_)). subst. apply Rplus_eq_compat_l.
rewrite sin_plus in Hx.
assert (H : sin (IZR q * PI) = 0) by (apply sin_eq_0_1; now exists q).
rewrite H, Rmult_0_l, Rplus_0_l in Hx.
destruct (Rmult_integral _ _ Hx) as [H'|H'].
- exfalso.
generalize (sin2_cos2 (IZR q * PI)).
rewrite H, H', Rsqr_0, Rplus_0_l.
intros; now apply R1_neq_R0.
- rewrite Rabs_right in Hr'; [|left; apply PI_RGT_0].
destruct Hr as [Hr | ->]; trivial.
exfalso.
generalize (sin_gt_0 r Hr Hr'). rewrite H'. apply Rlt_irrefl.
Qed.
Lemma cos_eq_0_0 (x:R) :
cos x = 0 -> exists k : Z, x = IZR k * PI + PI / 2.
Proof.
rewrite cos_sin. intros Hx.
destruct (sin_eq_0_0 (PI/2 + x) Hx) as (k,Hk). clear Hx.
exists (k-1)%Z. rewrite <- Z_R_minus; simpl.
symmetry in Hk. field_simplify [Hk]. field.
Qed.
Lemma cos_eq_0_1 (x:R) :
(exists k : Z, x = IZR k * PI + PI / 2) -> cos x = 0.
Proof.
rewrite cos_sin. intros (k,->).
replace (_ + _) with (IZR k * PI + PI) by field.
rewrite neg_sin, <- Ropp_0. apply Ropp_eq_compat.
apply sin_eq_0_1. now exists k.
Qed.
Lemma sin_eq_O_2PI_0 (x:R) :
0 <= x -> x <= 2 * PI -> sin x = 0 ->
x = 0 \/ x = PI \/ x = 2 * PI.
Proof.
intros Lo Hi Hx. destruct (sin_eq_0_0 x Hx) as (k,Hk). clear Hx.
destruct (Rtotal_order PI x) as [Hx|[Hx|Hx]].
- right; right.
clear Lo. subst.
f_equal. change 2 with (IZR (- (-2))). f_equal.
apply Z.add_move_0_l.
apply one_IZR_lt1.
rewrite plus_IZR; simpl.
split.
+ replace (-1) with (-2 + 1) by ring.
apply Rplus_lt_compat_l.
apply Rmult_lt_reg_r with PI; [apply PI_RGT_0|].
now rewrite Rmult_1_l.
+ apply Rle_lt_trans with 0; [|apply Rlt_0_1].
replace 0 with (-2 + 2) by ring.
apply Rplus_le_compat_l.
apply Rmult_le_reg_r with PI; [apply PI_RGT_0|].
trivial.
- right; left; auto.
- left.
clear Hi. subst.
replace 0 with (IZR 0 * PI) by apply Rmult_0_l. f_equal. f_equal.
apply one_IZR_lt1.
split.
+ apply Rlt_le_trans with 0;
[rewrite <- Ropp_0; apply Ropp_gt_lt_contravar, Rlt_0_1 | ].
apply Rmult_le_reg_r with PI; [apply PI_RGT_0|].
now rewrite Rmult_0_l.
+ apply Rmult_lt_reg_r with PI; [apply PI_RGT_0|].
now rewrite Rmult_1_l.
Qed.
Lemma sin_eq_O_2PI_1 (x:R) :
0 <= x -> x <= 2 * PI ->
x = 0 \/ x = PI \/ x = 2 * PI -> sin x = 0.
Proof.
intros _ _ [ -> |[ -> | -> ]].
- now rewrite sin_0.
- now rewrite sin_PI.
- now rewrite sin_2PI.
Qed.
Lemma cos_eq_0_2PI_0 (x:R) :
0 <= x -> x <= 2 * PI -> cos x = 0 ->
x = PI / 2 \/ x = 3 * (PI / 2).
Proof.
intros Lo Hi Hx.
destruct (Rtotal_order x (3 * (PI / 2))) as [LT|[EQ|GT]].
- rewrite cos_sin in Hx.
assert (Lo' : 0 <= PI / 2 + x).
{ apply Rplus_le_le_0_compat. apply Rlt_le, PI2_RGT_0. trivial. }
assert (Hi' : PI / 2 + x <= 2 * PI).
{ apply Rlt_le.
replace (2 * PI) with (PI / 2 + 3 * (PI / 2)) by field.
now apply Rplus_lt_compat_l. }
destruct (sin_eq_O_2PI_0 (PI / 2 + x) Lo' Hi' Hx) as [H|[H|H]].
+ exfalso.
apply (Rplus_le_compat_l (PI/2)) in Lo.
rewrite Rplus_0_r, H in Lo.
apply (Rlt_irrefl 0 (Rlt_le_trans 0 (PI / 2) 0 PI2_RGT_0 Lo)).
+ left.
apply (Rplus_eq_compat_l (-(PI/2))) in H.
ring_simplify in H. rewrite H. field.
+ right.
apply (Rplus_eq_compat_l (-(PI/2))) in H.
ring_simplify in H. rewrite H. field.
- now right.
- exfalso.
destruct (cos_eq_0_0 x Hx) as (k,Hk). clear Hx Lo.
subst.
assert (LT : (k < 2)%Z).
{ apply lt_IZR. simpl.
apply (Rmult_lt_reg_r PI); [apply PI_RGT_0|].
apply Rlt_le_trans with (IZR k * PI + PI/2); trivial.
rewrite <- (Rplus_0_r (IZR k * PI)) at 1.
apply Rplus_lt_compat_l. apply PI2_RGT_0. }
assert (GT' : (1 < k)%Z).
{ apply lt_IZR. simpl.
apply (Rmult_lt_reg_r PI); [apply PI_RGT_0|rewrite Rmult_1_l].
replace (3*(PI/2)) with (PI/2 + PI) in GT by field.
rewrite Rplus_comm in GT.
now apply Rplus_lt_reg_l in GT. }
lia.
Qed.
Lemma cos_eq_0_2PI_1 (x:R) :
0 <= x -> x <= 2 * PI ->
x = PI / 2 \/ x = 3 * (PI / 2) -> cos x = 0.
Proof.
intros Lo Hi [ -> | -> ].
- now rewrite cos_PI2.
- now rewrite cos_3PI2.
Qed.