diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
| commit | 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 (patch) | |
| tree | 77c0021911e3696a8c98e35a51840800db4be2a9 /theories/Reals/Rtrigo.v | |
| parent | 9058fb97426307536f56c3e7447be2f70798e081 (diff) | |
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo.v')
| -rw-r--r-- | theories/Reals/Rtrigo.v | 2570 |
1 files changed, 1583 insertions, 987 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index ae23fd8a6..60f07f610 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -8,1104 +8,1700 @@ (*i $Id$ i*) -Require Rbase. -Require Rfunctions. -Require SeqSeries. +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 ZArith_base. -Require Zcomplements. -Require Classical_Prop. -V7only [Import nat_scope. Import Z_scope. Import R_scope.]. +Require Import ZArith_base. +Require Import Zcomplements. +Require Import Classical_Prop. Open Local Scope nat_scope. Open Local Scope R_scope. (** sin_PI2 is the only remaining axiom **) -Axiom sin_PI2 : ``(sin (PI/2))==1``. +Axiom sin_PI2 : sin (PI / 2) = 1. (**********) -Lemma PI_neq0 : ~``PI==0``. -Red; Intro; Assert H0 := PI_RGT_0; Rewrite H in H0; Elim (Rlt_antirefl ? H0). +Lemma PI_neq0 : PI <> 0. +red in |- *; intro; assert (H0 := PI_RGT_0); rewrite H in H0; + elim (Rlt_irrefl _ H0). Qed. (**********) -Lemma cos_minus : (x,y:R) ``(cos (x-y))==(cos x)*(cos y)+(sin x)*(sin y)``. -Intros; Unfold Rminus; Rewrite cos_plus. -Rewrite <- cos_sym; Rewrite sin_antisym; Ring. +Lemma cos_minus : forall x y:R, cos (x - y) = cos x * cos y + sin x * sin y. +intros; unfold Rminus in |- *; rewrite cos_plus. +rewrite <- cos_sym; rewrite sin_antisym; ring. Qed. (**********) -Lemma sin2_cos2 : (x:R) ``(Rsqr (sin x)) + (Rsqr (cos x))==1``. -Intro; Unfold Rsqr; Rewrite Rplus_sym; Rewrite <- (cos_minus x x); Unfold Rminus; Rewrite Rplus_Ropp_r; Apply cos_0. +Lemma sin2_cos2 : forall x:R, Rsqr (sin x) + Rsqr (cos x) = 1. +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 : (x:R) ``(Rsqr (cos x))==1-(Rsqr (sin x))``. -Intro x; Generalize (sin2_cos2 x); Intro H1; Rewrite <- H1; Unfold Rminus; Rewrite <- (Rplus_sym (Rsqr (cos x))); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Symmetry; Apply Rplus_Or. +Lemma cos2 : forall x:R, Rsqr (cos x) = 1 - Rsqr (sin x). +intro x; generalize (sin2_cos2 x); intro H1; rewrite <- H1; + unfold Rminus in |- *; rewrite <- (Rplus_comm (Rsqr (cos x))); + rewrite Rplus_assoc; rewrite Rplus_opp_r; symmetry in |- *; + apply Rplus_0_r. Qed. (**********) -Lemma cos_PI2 : ``(cos (PI/2))==0``. -Apply Rsqr_eq_0; Rewrite cos2; Rewrite sin_PI2; Rewrite Rsqr_1; Unfold Rminus; Apply Rplus_Ropp_r. +Lemma cos_PI2 : cos (PI / 2) = 0. +apply Rsqr_eq_0; rewrite cos2; rewrite sin_PI2; rewrite Rsqr_1; + unfold Rminus in |- *; apply Rplus_opp_r. Qed. (**********) -Lemma cos_PI : ``(cos PI)==-1``. -Replace ``PI`` with ``PI/2+PI/2``. -Rewrite cos_plus. -Rewrite sin_PI2; Rewrite cos_PI2. -Ring. -Symmetry; Apply double_var. +Lemma cos_PI : cos PI = -1. +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``. -Assert H := (sin2_cos2 PI). -Rewrite cos_PI in H. -Rewrite <- Rsqr_neg in H. -Rewrite Rsqr_1 in H. -Cut (Rsqr (sin PI))==R0. -Intro; Apply (Rsqr_eq_0 ? H0). -Apply r_Rplus_plus with R1. -Rewrite Rplus_Or; Rewrite Rplus_sym; Exact H. +Lemma sin_PI : sin PI = 0. +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 neg_cos : (x:R) ``(cos (x+PI))==-(cos x)``. -Intro x; Rewrite -> cos_plus; Rewrite -> sin_PI; Rewrite -> cos_PI; Ring. +Lemma neg_cos : forall x:R, cos (x + PI) = - cos x. +intro x; rewrite cos_plus; rewrite sin_PI; rewrite cos_PI; ring. Qed. (**********) -Lemma sin_cos : (x:R) ``(sin x)==-(cos (PI/2+x))``. -Intro x; Rewrite -> cos_plus; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. +Lemma sin_cos : forall x:R, sin x = - cos (PI / 2 + x). +intro x; rewrite cos_plus; rewrite sin_PI2; rewrite cos_PI2; ring. Qed. (**********) -Lemma sin_plus : (x,y:R) ``(sin (x+y))==(sin x)*(cos y)+(cos x)*(sin y)``. -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_Ropp; Reflexivity. -Pattern 1 PI; Rewrite (double_var PI); Ring. +Lemma sin_plus : forall x y:R, sin (x + y) = sin x * cos y + cos x * sin y. +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 : (x,y:R) ``(sin (x-y))==(sin x)*(cos y)-(cos x)*(sin y)``. -Intros; Unfold Rminus; Rewrite sin_plus. -Rewrite <- cos_sym; Rewrite sin_antisym; Ring. +Lemma sin_minus : forall x y:R, sin (x - y) = sin x * cos y - cos x * sin y. +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 : (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))``. -Intros; Unfold tan; Rewrite sin_plus; Rewrite cos_plus; Unfold Rdiv; 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_Rmult. -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_Rplus_distrl; Rewrite Rinv_Rmult. -Repeat Rewrite Rmult_assoc; Repeat Rewrite (Rmult_sym ``(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; Rewrite Rmult_Rplus_distr; Rewrite Rmult_1r; Apply Rplus_plus_r; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym ``(sin x)``); Rewrite (Rmult_sym ``(cos y)``); Rewrite <- Ropp_mul3; Repeat Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym. -Rewrite Rmult_1l; Rewrite (Rmult_sym (sin x)); Rewrite <- Ropp_mul3; Repeat Rewrite Rmult_assoc; Apply Rmult_mult_r; Rewrite (Rmult_sym ``/(cos y)``); Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Apply Rmult_1r. -Assumption. -Assumption. +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). +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 sin2 : (x:R) ``(Rsqr (sin x))==1-(Rsqr (cos x))``. -Intro x; Generalize (cos2 x); Intro H1; Rewrite -> H1. -Unfold Rminus; Rewrite Ropp_distr1; Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Ol; Symmetry; Apply Ropp_Ropp. +Lemma sin2 : forall x:R, Rsqr (sin x) = 1 - Rsqr (cos x). +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 sin_2a : (x:R) ``(sin (2*x))==2*(sin x)*(cos x)``. -Intro x; Rewrite double; Rewrite sin_plus. -Rewrite <- (Rmult_sym (sin x)); Symmetry; Rewrite Rmult_assoc; Apply double. +Lemma sin_2a : forall x:R, sin (2 * x) = 2 * sin x * cos x. +intro x; rewrite double; rewrite sin_plus. +rewrite <- (Rmult_comm (sin x)); symmetry in |- *; rewrite Rmult_assoc; + apply double. Qed. -Lemma cos_2a : (x:R) ``(cos (2*x))==(cos x)*(cos x)-(sin x)*(sin x)``. -Intro x; Rewrite double; Apply cos_plus. +Lemma cos_2a : forall x:R, cos (2 * x) = cos x * cos x - sin x * sin x. +intro x; rewrite double; apply cos_plus. Qed. -Lemma cos_2a_cos : (x:R) ``(cos (2*x))==2*(cos x)*(cos x)-1``. -Intro x; Rewrite double; Unfold Rminus; Rewrite Rmult_assoc; Rewrite cos_plus; Generalize (sin2_cos2 x); Rewrite double; Intro H1; Rewrite <- H1; SqRing. +Lemma cos_2a_cos : forall x:R, cos (2 * x) = 2 * cos x * cos x - 1. +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 : (x:R) ``(cos (2*x))==1-2*(sin x)*(sin x)``. -Intro x; Rewrite Rmult_assoc; Unfold Rminus; Repeat Rewrite double. -Generalize (sin2_cos2 x); Intro H1; Rewrite <- H1; Rewrite cos_plus; SqRing. +Lemma cos_2a_sin : forall x:R, cos (2 * x) = 1 - 2 * sin x * sin x. +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 : (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))``. -Repeat Rewrite double; Intros; Repeat Rewrite double; Rewrite double in H0; Apply tan_plus; Assumption. +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). +repeat rewrite double; intros; repeat rewrite double; rewrite double in H0; + apply tan_plus; assumption. Qed. -Lemma sin_neg : (x:R) ``(sin (-x))==-(sin x)``. -Apply sin_antisym. +Lemma sin_neg : forall x:R, sin (- x) = - sin x. +apply sin_antisym. Qed. -Lemma cos_neg : (x:R) ``(cos (-x))==(cos x)``. -Intro; Symmetry; Apply cos_sym. +Lemma cos_neg : forall x:R, cos (- x) = cos x. +intro; symmetry in |- *; apply cos_sym. Qed. -Lemma tan_0 : ``(tan 0)==0``. -Unfold tan; Rewrite -> sin_0; Rewrite -> cos_0. -Unfold Rdiv; Apply Rmult_Ol. +Lemma tan_0 : tan 0 = 0. +unfold tan in |- *; rewrite sin_0; rewrite cos_0. +unfold Rdiv in |- *; apply Rmult_0_l. Qed. -Lemma tan_neg : (x:R) ``(tan (-x))==-(tan x)``. -Intros x; Unfold tan; Rewrite sin_neg; Rewrite cos_neg; Unfold Rdiv. -Apply Ropp_mul1. +Lemma tan_neg : forall x:R, tan (- x) = - tan x. +intros x; unfold tan in |- *; rewrite sin_neg; rewrite cos_neg; + unfold Rdiv in |- *. +apply Ropp_mult_distr_l_reverse. Qed. -Lemma tan_minus : (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))``. -Intros; Unfold Rminus; Rewrite tan_plus. -Rewrite tan_neg; Unfold Rminus; Rewrite <- Ropp_mul1; Rewrite Ropp_mul2; Reflexivity. -Assumption. -Rewrite cos_neg; Assumption. -Assumption. -Rewrite tan_neg; Unfold Rminus; Rewrite <- Ropp_mul1; Rewrite Ropp_mul2; Assumption. +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). +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``. -Replace ``3*(PI/2)`` with ``PI+(PI/2)``. -Rewrite -> cos_plus; Rewrite -> sin_PI; Rewrite -> cos_PI2; Ring. -Pattern 1 PI; Rewrite (double_var PI). -Ring. +Lemma cos_3PI2 : cos (3 * (PI / 2)) = 0. +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``. -Rewrite -> sin_2a; Rewrite -> sin_PI; Ring. +Lemma sin_2PI : sin (2 * PI) = 0. +rewrite sin_2a; rewrite sin_PI; ring. Qed. -Lemma cos_2PI : ``(cos (2*PI))==1``. -Rewrite -> cos_2a; Rewrite -> sin_PI; Rewrite -> cos_PI; Ring. +Lemma cos_2PI : cos (2 * PI) = 1. +rewrite cos_2a; rewrite sin_PI; rewrite cos_PI; ring. Qed. -Lemma neg_sin : (x:R) ``(sin (x+PI))==-(sin x)``. -Intro x; Rewrite -> sin_plus; Rewrite -> sin_PI; Rewrite -> cos_PI; Ring. +Lemma neg_sin : forall x:R, sin (x + PI) = - sin x. +intro x; rewrite sin_plus; rewrite sin_PI; rewrite cos_PI; ring. Qed. -Lemma sin_PI_x : (x:R) ``(sin (PI-x))==(sin x)``. -Intro x; Rewrite -> sin_minus; Rewrite -> sin_PI; Rewrite -> cos_PI; Rewrite Rmult_Ol; Unfold Rminus; Rewrite Rplus_Ol; Rewrite Ropp_mul1; Rewrite Ropp_Ropp; Apply Rmult_1l. +Lemma sin_PI_x : forall x:R, sin (PI - x) = sin x. +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 : (x:R)(k:nat) ``(sin (x+2*(INR k)*PI))==(sin x)``. -Intros x k; Induction k. -Cut ``x+2*(INR O)*PI==x``; [Intro; Rewrite H; Reflexivity | Ring]. -Replace ``x+2*(INR (S k))*PI`` with ``(x+2*(INR k)*PI)+(2*PI)``; [Rewrite -> sin_plus; Rewrite -> sin_2PI; Rewrite -> cos_2PI; Ring; Apply Hreck | Rewrite -> S_INR; Ring]. +Lemma sin_period : forall (x:R) (k:nat), sin (x + 2 * INR k * PI) = sin x. +intros x k; induction k as [| k Hreck]. +cut (x + 2 * INR 0 * PI = x); [ intro; rewrite H; reflexivity | ring ]. +replace (x + 2 * INR (S k) * PI) with (x + 2 * INR k * PI + 2 * PI); + [ rewrite sin_plus; rewrite sin_2PI; rewrite cos_2PI; ring; apply Hreck + | rewrite S_INR; ring ]. Qed. -Lemma cos_period : (x:R)(k:nat) ``(cos (x+2*(INR k)*PI))==(cos x)``. -Intros x k; Induction k. -Cut ``x+2*(INR O)*PI==x``; [Intro; Rewrite H; Reflexivity | Ring]. -Replace ``x+2*(INR (S k))*PI`` with ``(x+2*(INR k)*PI)+(2*PI)``; [Rewrite -> cos_plus; Rewrite -> sin_2PI; Rewrite -> cos_2PI; Ring; Apply Hreck | Rewrite -> S_INR; Ring]. +Lemma cos_period : forall (x:R) (k:nat), cos (x + 2 * INR k * PI) = cos x. +intros x k; induction k as [| k Hreck]. +cut (x + 2 * INR 0 * PI = x); [ intro; rewrite H; reflexivity | ring ]. +replace (x + 2 * INR (S k) * PI) with (x + 2 * INR k * PI + 2 * PI); + [ rewrite cos_plus; rewrite sin_2PI; rewrite cos_2PI; ring; apply Hreck + | rewrite S_INR; ring ]. Qed. -Lemma sin_shift : (x:R) ``(sin (PI/2-x))==(cos x)``. -Intro x; Rewrite -> sin_minus; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. +Lemma sin_shift : forall x:R, sin (PI / 2 - x) = cos x. +intro x; rewrite sin_minus; rewrite sin_PI2; rewrite cos_PI2; ring. Qed. -Lemma cos_shift : (x:R) ``(cos (PI/2-x))==(sin x)``. -Intro x; Rewrite -> cos_minus; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. +Lemma cos_shift : forall x:R, cos (PI / 2 - x) = sin x. +intro x; rewrite cos_minus; rewrite sin_PI2; rewrite cos_PI2; ring. Qed. -Lemma cos_sin : (x:R) ``(cos x)==(sin (PI/2+x))``. -Intro x; Rewrite -> sin_plus; Rewrite -> sin_PI2; Rewrite -> cos_PI2; Ring. +Lemma cos_sin : forall x:R, cos x = sin (PI / 2 + x). +intro x; rewrite sin_plus; rewrite sin_PI2; rewrite cos_PI2; ring. Qed. -Lemma PI2_RGT_0 : ``0<PI/2``. -Unfold Rdiv; Apply Rmult_lt_pos; [Apply PI_RGT_0 | Apply Rlt_Rinv; Sup]. +Lemma PI2_RGT_0 : 0 < PI / 2. +unfold Rdiv in |- *; apply Rmult_lt_0_compat; + [ apply PI_RGT_0 | apply Rinv_0_lt_compat; prove_sup ]. Qed. -Lemma SIN_bound : (x:R) ``-1<=(sin x)<=1``. -Intro; Case (total_order_Rle ``-1`` (sin x)); Intro. -Case (total_order_Rle (sin x) ``1``); Intro. -Split; Assumption. -Cut ``1<(sin x)``. -Intro; Generalize (Rsqr_incrst_1 ``1`` (sin x) H (Rlt_le ``0`` ``1`` Rlt_R0_R1) (Rlt_le ``0`` (sin x) (Rlt_trans ``0`` ``1`` (sin x) Rlt_R0_R1 H))); Rewrite Rsqr_1; Intro; Rewrite sin2 in H0; Unfold Rminus in H0; Generalize (Rlt_compatibility ``-1`` ``1`` ``1+ -(Rsqr (cos x))`` H0); Repeat Rewrite <- Rplus_assoc; Repeat Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Intro; Rewrite <- Ropp_O in H1; Generalize (Rlt_Ropp ``-0`` ``-(Rsqr (cos x))`` H1); Repeat Rewrite Ropp_Ropp; Intro; Generalize (pos_Rsqr (cos x)); Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` (Rsqr (cos x)) ``0`` H3 H2)). -Auto with real. -Cut ``(sin x)< -1``. -Intro; Generalize (Rlt_Ropp (sin x) ``-1`` H); Rewrite Ropp_Ropp; Clear H; Intro; Generalize (Rsqr_incrst_1 ``1`` ``-(sin x)`` H (Rlt_le ``0`` ``1`` Rlt_R0_R1) (Rlt_le ``0`` ``-(sin x)`` (Rlt_trans ``0`` ``1`` ``-(sin x)`` Rlt_R0_R1 H))); Rewrite Rsqr_1; Intro; Rewrite <- Rsqr_neg in H0; Rewrite sin2 in H0; Unfold Rminus in H0; Generalize (Rlt_compatibility ``-1`` ``1`` ``1+ -(Rsqr (cos x))`` H0); Repeat Rewrite <- Rplus_assoc; Repeat Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Intro; Rewrite <- Ropp_O in H1; Generalize (Rlt_Ropp ``-0`` ``-(Rsqr (cos x))`` H1); Repeat Rewrite Ropp_Ropp; Intro; Generalize (pos_Rsqr (cos x)); Intro; Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` (Rsqr (cos x)) ``0`` H3 H2)). -Auto with real. -Qed. - -Lemma COS_bound : (x:R) ``-1<=(cos x)<=1``. -Intro; Rewrite <- sin_shift; Apply SIN_bound. -Qed. - -Lemma cos_sin_0 : (x:R) ~(``(cos x)==0``/\``(sin x)==0``). -Intro; Red; Intro; Elim H; Intros; Generalize (sin2_cos2 x); Intro; Rewrite H0 in H2; Rewrite H1 in H2; Repeat Rewrite Rsqr_O in H2; Rewrite Rplus_Or in H2; Generalize Rlt_R0_R1; Intro; Rewrite <- H2 in H3; Elim (Rlt_antirefl ``0`` H3). +Lemma SIN_bound : forall x:R, -1 <= sin x <= 1. +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. +intro; rewrite <- sin_shift; apply SIN_bound. +Qed. + +Lemma cos_sin_0 : forall x:R, ~ (cos x = 0 /\ sin x = 0). +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 : (x:R) ~``(cos x)==0``\/~``(sin x)==0``. -Intro; Apply not_and_or; Apply cos_sin_0. +Lemma cos_sin_0_var : forall x:R, cos x <> 0 \/ sin x <> 0. +intro; apply not_and_or; apply cos_sin_0. 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 : (a:R) ``0<a``->``a<=PI/2``->``0<(sin_lb a)``. -Intros. -Unfold sin_lb; Unfold sin_approx; Unfold sin_term. -Pose Un := [i:nat]``(pow a (plus (mult (S (S O)) i) (S O)))/(INR (fact (plus (mult (S (S O)) i) (S O))))``. -Replace (sum_f_R0 [i:nat] ``(pow ( -1) i)*(pow a (plus (mult (S (S O)) i) (S O)))/(INR (fact (plus (mult (S (S O)) i) (S O))))`` (S (S (S O)))) with (sum_f_R0 [i:nat]``(pow (-1) i)*(Un i)`` (3)); [Idtac | Apply sum_eq; Intros; Unfold Un; Reflexivity]. -Cut (n:nat)``(Un (S n))<(Un n)``. -Intro; Simpl. -Repeat Rewrite Rmult_1l; Repeat Rewrite Rmult_1r; Replace ``-1*(Un (S O))`` with ``-(Un (S O))``; [Idtac | Ring]; Replace ``-1* -1*(Un (S (S O)))`` with ``(Un (S (S O)))``; [Idtac | Ring]; Replace ``-1*( -1* -1)*(Un (S (S (S O))))`` with ``-(Un (S (S (S O))))``; [Idtac | Ring]; Replace ``(Un O)+ -(Un (S O))+(Un (S (S O)))+ -(Un (S (S (S O))))`` with ``((Un O)-(Un (S O)))+((Un (S (S O)))-(Un (S (S (S O)))))``; [Idtac | Ring]. -Apply gt0_plus_gt0_is_gt0. -Unfold Rminus; Apply Rlt_anti_compatibility with (Un (S O)); Rewrite Rplus_Or; Rewrite (Rplus_sym (Un (S O))); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Apply H1. -Unfold Rminus; Apply Rlt_anti_compatibility with (Un (S (S (S O)))); Rewrite Rplus_Or; Rewrite (Rplus_sym (Un (S (S (S O))))); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Apply H1. -Intro; Unfold Un. -Cut (plus (mult (2) (S n)) (S O)) = (plus (plus (mult (2) n) (S O)) (2)). -Intro; Rewrite H1. -Rewrite pow_add; Unfold Rdiv; Rewrite Rmult_assoc; Apply Rlt_monotony. -Apply pow_lt; Assumption. -Rewrite <- H1; Apply Rlt_monotony_contra with (INR (fact (plus (mult (S (S O)) n) (S O)))). -Apply lt_INR_0; Apply neq_O_lt. -Assert H2 := (fact_neq_0 (plus (mult (2) n) (1))). -Red; Intro; Elim H2; Symmetry; Assumption. -Rewrite <- Rinv_r_sym. -Apply Rlt_monotony_contra with (INR (fact (plus (mult (S (S O)) (S n)) (S O)))). -Apply lt_INR_0; Apply neq_O_lt. -Assert H2 := (fact_neq_0 (plus (mult (2) (S n)) (1))). -Red; Intro; Elim H2; Symmetry; Assumption. -Rewrite (Rmult_sym (INR (fact (plus (mult (S (S O)) (S n)) (S O))))); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Do 2 Rewrite Rmult_1r; Apply Rle_lt_trans with ``(INR (fact (plus (mult (S (S O)) n) (S O))))*4``. -Apply Rle_monotony. -Replace R0 with (INR O); [Idtac | Reflexivity]; Apply le_INR; Apply le_O_n. -Simpl; Rewrite Rmult_1r; Replace ``4`` with ``(Rsqr 2)``; [Idtac | SqRing]; Replace ``a*a`` with (Rsqr a); [Idtac | Reflexivity]; Apply Rsqr_incr_1. -Apply Rle_trans with ``PI/2``; [Assumption | Unfold Rdiv; Apply Rle_monotony_contra with ``2``; [ Sup0 | Rewrite <- Rmult_assoc; Rewrite Rinv_r_simpl_m; [Replace ``2*2`` with ``4``; [Apply PI_4 | Ring] | DiscrR]]]. -Left; Assumption. -Left; Sup0. -Rewrite H1; Replace (plus (plus (mult (S (S O)) n) (S O)) (S (S O))) with (S (S (plus (mult (S (S O)) n) (S O)))). -Do 2 Rewrite fact_simpl; Do 2 Rewrite mult_INR. -Repeat Rewrite <- Rmult_assoc. -Rewrite <- (Rmult_sym (INR (fact (plus (mult (S (S O)) n) (S O))))). -Rewrite Rmult_assoc. -Apply Rlt_monotony. -Apply lt_INR_0; Apply neq_O_lt. -Assert H2 := (fact_neq_0 (plus (mult (2) n) (1))). -Red; Intro; Elim H2; Symmetry; Assumption. -Do 2 Rewrite S_INR; Rewrite plus_INR; Rewrite mult_INR; Pose x := (INR n); Unfold INR. -Replace ``(2*x+1+1+1)*(2*x+1+1)`` with ``4*x*x+10*x+6``; [Idtac | Ring]. -Apply Rlt_anti_compatibility with ``-4``; Rewrite Rplus_Ropp_l; Replace ``-4+(4*x*x+10*x+6)`` with ``(4*x*x+10*x)+2``; [Idtac | Ring]. -Apply ge0_plus_gt0_is_gt0. -Cut ``0<=x``. -Intro; Apply ge0_plus_ge0_is_ge0; Repeat Apply Rmult_le_pos; Assumption Orelse Left; Sup. -Unfold x; Replace R0 with (INR O); [Apply le_INR; Apply le_O_n | Reflexivity]. -Sup0. -Apply INR_eq; Do 2 Rewrite S_INR; Do 3 Rewrite plus_INR; Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Apply INR_fact_neq_0. -Apply INR_fact_neq_0. -Apply INR_eq; Do 3 Rewrite plus_INR; Do 2 Rewrite mult_INR; Repeat Rewrite S_INR; Ring. -Qed. - -Lemma SIN : (a:R) ``0<=a`` -> ``a<=PI`` -> ``(sin_lb a)<=(sin a)<=(sin_ub a)``. -Intros; Unfold sin_lb sin_ub; Apply (sin_bound a (S O) H H0). -Qed. - -Lemma COS : (a:R) ``-PI/2<=a`` -> ``a<=PI/2`` -> ``(cos_lb a)<=(cos a)<=(cos_ub a)``. -Intros; Unfold cos_lb cos_ub; Apply (cos_bound a (S O) H H0). +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. +intros. +unfold sin_lb in |- *; unfold sin_approx in |- *; unfold sin_term in |- *. +pose (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; pose (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. +apply INR_eq; do 2 rewrite S_INR; do 3 rewrite plus_INR; rewrite mult_INR; + repeat rewrite S_INR; ring. +apply INR_fact_neq_0. +apply INR_fact_neq_0. +apply INR_eq; do 3 rewrite plus_INR; do 2 rewrite mult_INR; + repeat rewrite S_INR; 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``. -Rewrite <- Ropp_O; Apply Rlt_Ropp1; Apply PI2_RGT_0. +Lemma _PI2_RLT_0 : - (PI / 2) < 0. +rewrite <- Ropp_0; apply Ropp_lt_contravar; apply PI2_RGT_0. Qed. -Lemma PI4_RLT_PI2 : ``PI/4<PI/2``. -Unfold Rdiv; Apply Rlt_monotony. -Apply PI_RGT_0. -Apply Rinv_lt. -Apply Rmult_lt_pos; Sup0. -Pattern 1 ``2``; Rewrite <- Rplus_Or. -Replace ``4`` with ``2+2``; [Apply Rlt_compatibility; Sup0 | Ring]. +Lemma PI4_RLT_PI2 : PI / 4 < PI / 2. +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``. -Unfold Rdiv; Pattern 2 PI; Rewrite <- Rmult_1r. -Apply Rlt_monotony. -Apply PI_RGT_0. -Pattern 3 R1; Rewrite <- Rinv_R1; Apply Rinv_lt. -Rewrite Rmult_1l; Sup0. -Pattern 1 R1; Rewrite <- Rplus_Or; Apply Rlt_compatibility; Apply Rlt_R0_R1. +Lemma PI2_Rlt_PI : PI / 2 < PI. +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 : (x:R) ``0<x`` -> ``x<PI`` -> ``0<(sin x)``. -Intros; Elim (SIN x (Rlt_le R0 x H) (Rlt_le x PI H0)); Intros H1 _; Case (total_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_R0_R1. -Rewrite <- sin_PI_x; Generalize (Rgt_Ropp x ``PI/2`` H3); Intro H4; Generalize (Rlt_compatibility PI (Ropp x) (Ropp ``PI/2``) H4). -Replace ``PI+(-x)`` with ``PI-x``. -Replace ``PI+ -(PI/2)`` with ``PI/2``. -Intro H5; Generalize (Rlt_Ropp x PI H0); Intro H6; Change ``-PI < -x`` in H6; Generalize (Rlt_compatibility PI (Ropp PI) (Ropp x) H6). -Rewrite Rplus_Ropp_r. -Replace ``PI+ -x`` with ``PI-x``. -Intro H7; Elim (SIN ``PI-x`` (Rlt_le R0 ``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 2 PI; Rewrite double_var; Ring. -Reflexivity. -Qed. - -Theorem cos_gt_0 : (x:R) ``-(PI/2)<x`` -> ``x<PI/2`` -> ``0<(cos x)``. -Intros; Rewrite cos_sin; Generalize (Rlt_compatibility ``PI/2`` ``-(PI/2)`` x H). -Rewrite Rplus_Ropp_r; Intro H1; Generalize (Rlt_compatibility ``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 : (x:R) ``0<=x`` -> ``x<=PI`` -> ``0<=(sin x)``. -Intros x H1 H2; Elim H1; Intro H3; [ Elim H2; Intro H4; [ Left ; Apply (sin_gt_0 x H3 H4) | Rewrite H4; Right; Symmetry; Apply sin_PI ] | Rewrite <- H3; Right; Symmetry; Apply sin_0]. -Qed. - -Lemma cos_ge_0 : (x:R) ``-(PI/2)<=x`` -> ``x<=PI/2`` -> ``0<=(cos x)``. -Intros x H1 H2; Elim H1; Intro H3; [ Elim H2; Intro H4; [ Left ; Apply (cos_gt_0 x H3 H4) | Rewrite H4; Right; Symmetry; Apply cos_PI2 ] | Rewrite <- H3; Rewrite cos_neg; Right; Symmetry; Apply cos_PI2 ]. -Qed. - -Lemma sin_le_0 : (x:R) ``PI<=x`` -> ``x<=2*PI`` -> ``(sin x)<=0``. -Intros x H1 H2; Apply Rle_sym2; Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp (sin x)); Apply Rle_Ropp; Rewrite <- neg_sin; Replace ``x+PI`` with ``(x-PI)+2*(INR (S O))*PI``; [Rewrite -> (sin_period (Rminus x PI) (S O)); Apply sin_ge_0; [Replace ``x-PI`` with ``x+(-PI)``; [Rewrite Rplus_sym; Replace ``0`` with ``(-PI)+PI``; [Apply Rle_compatibility; Assumption | Ring] | Ring] | Replace ``x-PI`` with ``x+(-PI)``; Rewrite Rplus_sym; [Pattern 2 PI; Replace ``PI`` with ``(-PI)+2*PI``; [Apply Rle_compatibility; Assumption | Ring] | Ring]] |Unfold INR; Ring]. -Qed. - -Lemma cos_le_0 : (x:R) ``PI/2<=x``->``x<=3*(PI/2)``->``(cos x)<=0``. -Intros x H1 H2; Apply Rle_sym2; Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp (cos x)); Apply Rle_Ropp; Rewrite <- neg_cos; Replace ``x+PI`` with ``(x-PI)+2*(INR (S O))*PI``. -Rewrite cos_period; Apply cos_ge_0. -Replace ``-(PI/2)`` with ``-PI+(PI/2)``. -Unfold Rminus; Rewrite (Rplus_sym x); Apply Rle_compatibility; Assumption. -Pattern 1 PI; Rewrite (double_var PI); Rewrite Ropp_distr1; Ring. -Unfold Rminus; Rewrite Rplus_sym; Replace ``PI/2`` with ``(-PI)+3*(PI/2)``. -Apply Rle_compatibility; Assumption. -Pattern 1 PI; Rewrite (double_var PI); Rewrite Ropp_distr1; Ring. -Unfold INR; Ring. -Qed. - -Lemma sin_lt_0 : (x:R) ``PI<x`` -> ``x<2*PI`` -> ``(sin x)<0``. -Intros x H1 H2; Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp (sin x)); Apply Rlt_Ropp; Rewrite <- neg_sin; Replace ``x+PI`` with ``(x-PI)+2*(INR (S O))*PI``; [Rewrite -> (sin_period (Rminus x PI) (S O)); Apply sin_gt_0; [Replace ``x-PI`` with ``x+(-PI)``; [Rewrite Rplus_sym; Replace ``0`` with ``(-PI)+PI``; [Apply Rlt_compatibility; Assumption | Ring] | Ring] | Replace ``x-PI`` with ``x+(-PI)``; Rewrite Rplus_sym; [Pattern 2 PI; Replace ``PI`` with ``(-PI)+2*PI``; [Apply Rlt_compatibility; Assumption | Ring] | Ring]] |Unfold INR; Ring]. -Qed. - -Lemma sin_lt_0_var : (x:R) ``-PI<x`` -> ``x<0`` -> ``(sin x)<0``. -Intros; Generalize (Rlt_compatibility ``2*PI`` ``-PI`` x H); Replace ``2*PI+(-PI)`` with ``PI``; [Intro H1; Rewrite Rplus_sym in H1; Generalize (Rlt_compatibility ``2*PI`` x ``0`` H0); Intro H2; Rewrite (Rplus_sym ``2*PI``) in H2; Rewrite <- (Rplus_sym R0) in H2; Rewrite Rplus_Ol in H2; Rewrite <- (sin_period x (1)); Unfold INR; Replace ``2*1*PI`` with ``2*PI``; [Apply (sin_lt_0 ``x+2*PI`` H1 H2) | Ring] | Ring]. -Qed. - -Lemma cos_lt_0 : (x:R) ``PI/2<x`` -> ``x<3*(PI/2)``-> ``(cos x)<0``. -Intros x H1 H2; Rewrite <- Ropp_O; Rewrite <- (Ropp_Ropp (cos x)); Apply Rlt_Ropp; Rewrite <- neg_cos; Replace ``x+PI`` with ``(x-PI)+2*(INR (S O))*PI``. -Rewrite cos_period; Apply cos_gt_0. -Replace ``-(PI/2)`` with ``-PI+(PI/2)``. -Unfold Rminus; Rewrite (Rplus_sym x); Apply Rlt_compatibility; Assumption. -Pattern 1 PI; Rewrite (double_var PI); Rewrite Ropp_distr1; Ring. -Unfold Rminus; Rewrite Rplus_sym; Replace ``PI/2`` with ``(-PI)+3*(PI/2)``. -Apply Rlt_compatibility; Assumption. -Pattern 1 PI; Rewrite (double_var PI); Rewrite Ropp_distr1; Ring. -Unfold INR; Ring. -Qed. - -Lemma tan_gt_0 : (x:R) ``0<x`` -> ``x<PI/2`` -> ``0<(tan x)``. -Intros x H1 H2; Unfold tan; Generalize _PI2_RLT_0; Generalize (Rlt_trans R0 x ``PI/2`` H1 H2); Intros; Generalize (Rlt_trans ``-(PI/2)`` R0 x H0 H1); Intro H5; Generalize (Rlt_trans x ``PI/2`` PI H2 PI2_Rlt_PI); Intro H7; Unfold Rdiv; Apply Rmult_lt_pos. -Apply sin_gt_0; Assumption. -Apply Rlt_Rinv; Apply cos_gt_0; Assumption. -Qed. - -Lemma tan_lt_0 : (x:R) ``-(PI/2)<x``->``x<0``->``(tan x)<0``. -Intros x H1 H2; Unfold tan; Generalize (cos_gt_0 x H1 (Rlt_trans x ``0`` ``PI/2`` H2 PI2_RGT_0)); Intro H3; Rewrite <- Ropp_O; Replace ``(sin x)/(cos x)`` with ``- ((-(sin x))/(cos x))``. -Rewrite <- sin_neg; Apply Rgt_Ropp; Change ``0<(sin (-x))/(cos x)``; Unfold Rdiv; Apply Rmult_lt_pos. -Apply sin_gt_0. -Rewrite <- Ropp_O; Apply Rgt_Ropp; Assumption. -Apply Rlt_trans with ``PI/2``. -Rewrite <- (Ropp_Ropp ``PI/2``); Apply Rgt_Ropp; Assumption. -Apply PI2_Rlt_PI. -Apply Rlt_Rinv; Assumption. -Unfold Rdiv; Ring. -Qed. - -Lemma cos_ge_0_3PI2 : (x:R) ``3*(PI/2)<=x``->``x<=2*PI``->``0<=(cos x)``. -Intros; Rewrite <- cos_neg; Rewrite <- (cos_period ``-x`` (1)); Unfold INR; Replace ``-x+2*1*PI`` with ``2*PI-x``. -Generalize (Rle_Ropp x ``2*PI`` H0); Intro H1; Generalize (Rle_sym2 ``-(2*PI)`` ``-x`` H1); Clear H1; Intro H1; Generalize (Rle_compatibility ``2*PI`` ``-(2*PI)`` ``-x`` H1). -Rewrite Rplus_Ropp_r. -Intro H2; Generalize (Rle_Ropp ``3*(PI/2)`` x H); Intro H3; Generalize (Rle_sym2 ``-x`` ``-(3*(PI/2))`` H3); Clear H3; Intro H3; Generalize (Rle_compatibility ``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 2 3 PI; Rewrite double_var; Ring. -Ring. -Qed. - -Lemma form1 : (p,q:R) ``(cos p)+(cos q)==2*(cos ((p-q)/2))*(cos ((p+q)/2))``. -Intros p q; Pattern 1 p; 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 3 q; Rewrite double_var; Unfold Rdiv; Ring. -Pattern 3 p; Rewrite double_var; Unfold Rdiv; Ring. -Qed. - -Lemma form2 : (p,q:R) ``(cos p)-(cos q)==-2*(sin ((p-q)/2))*(sin ((p+q)/2))``. -Intros p q; Pattern 1 p; 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 3 q; Rewrite double_var; Unfold Rdiv; Ring. -Pattern 3 p; Rewrite double_var; Unfold Rdiv; Ring. -Qed. - -Lemma form3 : (p,q:R) ``(sin p)+(sin q)==2*(cos ((p-q)/2))*(sin ((p+q)/2))``. -Intros p q; Pattern 1 p; Replace ``p`` with ``(p-q)/2+(p+q)/2``. -Pattern 3 q; Replace ``q`` with ``(p+q)/2-(p-q)/2``. -Rewrite sin_plus; Rewrite sin_minus; Ring. -Pattern 3 q; Rewrite double_var; Unfold Rdiv; Ring. -Pattern 3 p; Rewrite double_var; Unfold Rdiv; Ring. -Qed. - -Lemma form4 : (p,q:R) ``(sin p)-(sin q)==2*(cos ((p+q)/2))*(sin ((p-q)/2))``. -Intros p q; Pattern 1 p; Replace ``p`` with ``(p-q)/2+(p+q)/2``. -Pattern 3 q; Replace ``q`` with ``(p+q)/2-(p-q)/2``. -Rewrite sin_plus; Rewrite sin_minus; Ring. -Pattern 3 q; Rewrite double_var; Unfold Rdiv; Ring. -Pattern 3 p; Rewrite double_var; Unfold Rdiv; Ring. - -Qed. - -Lemma sin_increasing_0 : (x,y:R) ``-(PI/2)<=x``->``x<=PI/2``->``-(PI/2)<=y``->``y<=PI/2``->``(sin x)<(sin y)``->``x<y``. -Intros; Cut ``(sin ((x-y)/2))<0``. -Intro H4; Case (total_order ``(x-y)/2`` ``0``); Intro H5. -Assert Hyp : ``0<2``. -Sup0. -Generalize (Rlt_monotony ``2`` ``(x-y)/2`` ``0`` Hyp H5). -Unfold Rdiv. -Rewrite <- Rmult_assoc. -Rewrite Rinv_r_simpl_m. -Rewrite Rmult_Or. -Clear H5; Intro H5; Apply Rminus_lt; Assumption. -DiscrR. -Elim H5; Intro H6. -Rewrite H6 in H4; Rewrite sin_0 in H4; Elim (Rlt_antirefl ``0`` H4). -Change ``0<(x-y)/2`` in H6; Generalize (Rle_Ropp ``-(PI/2)`` y H1). -Rewrite Ropp_Ropp. -Intro H7; Generalize (Rle_sym2 ``-y`` ``PI/2`` H7); Clear H7; Intro H7; Generalize (Rplus_le x ``PI/2`` ``-y`` ``PI/2`` H0 H7). -Rewrite <- double_var. -Intro H8. -Assert Hyp : ``0<2``. -Sup0. -Generalize (Rle_monotony ``(Rinv 2)`` ``x-y`` PI (Rlt_le ``0`` ``/2`` (Rlt_Rinv ``2`` Hyp)) H8). -Repeat Rewrite (Rmult_sym ``/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_antirefl ``(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 x ``PI/2`` y ``PI/2`` H0 H2). -Rewrite <- double_var. -Assert Hyp : ``0<2``. -Sup0. -Intro H4; Generalize (Rle_monotony ``(Rinv 2)`` ``x+y`` PI (Rlt_le ``0`` ``/2`` (Rlt_Rinv ``2`` Hyp)) H4). -Repeat Rewrite (Rmult_sym ``/2``). -Clear H4; Intro H4; Generalize (Rplus_le ``-(PI/2)`` x ``-(PI/2)`` y H H1); Replace ``-(PI/2)+(-(PI/2))`` with ``-PI``. -Intro H5; Generalize (Rle_monotony ``(Rinv 2)`` ``-PI`` ``x+y`` (Rlt_le ``0`` ``/2`` (Rlt_Rinv ``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 (Rlt_monotony ``2`` ``0`` ``(cos ((x+y)/2))`` Hyp H6). -Rewrite Rmult_Or. -Clear H6; Intro H6; Case (case_Rabsolu ``(sin ((x-y)/2))``); Intro H7. -Assumption. -Generalize (Rle_sym2 ``0`` ``(sin ((x-y)/2))`` 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_antirefl ``0`` H9). -Rewrite <- H50 in H3; Rewrite cos_neg in H3; Rewrite cos_PI2 in H3; Rewrite Rmult_Or in H3; Rewrite Rmult_Ol in H3; Elim (Rlt_antirefl ``0`` H3). -Unfold Rdiv in H3. -Rewrite H40 in H3; Assert H50 := cos_PI2; Unfold Rdiv in H50; Rewrite H50 in H3; Rewrite Rmult_Or in H3; Rewrite Rmult_Ol in H3; Elim (Rlt_antirefl ``0`` H3). -Unfold Rdiv. -Rewrite <- Ropp_mul1. -Apply Rmult_sym. -Unfold Rdiv; Apply Rmult_sym. -Pattern 1 PI; Rewrite double_var. -Rewrite Ropp_distr1. -Reflexivity. -Qed. - -Lemma sin_increasing_1 : (x,y:R) ``-(PI/2)<=x``->``x<=PI/2``->``-(PI/2)<=y``->``y<=PI/2``->``x<y``->``(sin x)<(sin y)``. -Intros; Generalize (Rlt_compatibility ``x`` ``x`` ``y`` H3); Intro H4; Generalize (Rplus_le ``-(PI/2)`` x ``-(PI/2)`` x H H); Replace ``-(PI/2)+ (-(PI/2))`` with ``-PI``. -Assert Hyp : ``0<2``. -Sup0. -Intro H5; Generalize (Rle_lt_trans ``-PI`` ``x+x`` ``x+y`` H5 H4); Intro H6; Generalize (Rlt_monotony ``(Rinv 2)`` ``-PI`` ``x+y`` (Rlt_Rinv ``2`` Hyp) H6); Replace ``/2*(-PI)`` with ``-(PI/2)``. -Replace ``/2*(x+y)`` with ``(x+y)/2``. -Clear H4 H5 H6; Intro H4; Generalize (Rlt_compatibility ``y`` ``x`` ``y`` H3); Intro H5; Rewrite Rplus_sym in H5; Generalize (Rplus_le 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 (Rlt_monotony ``(Rinv 2)`` ``x+y`` PI (Rlt_Rinv ``2`` Hyp) H7); Replace ``/2*PI`` with ``PI/2``. -Replace ``/2*(x+y)`` with ``(x+y)/2``. -Clear H5 H6 H7; Intro H5; Generalize (Rle_Ropp ``-(PI/2)`` y H1); Rewrite Ropp_Ropp; Clear H1; Intro H1; Generalize (Rle_sym2 ``-y`` ``PI/2`` H1); Clear H1; Intro H1; Generalize (Rle_Ropp y ``PI/2`` H2); Clear H2; Intro H2; Generalize (Rle_sym2 ``-(PI/2)`` ``-y`` H2); Clear H2; Intro H2; Generalize (Rlt_compatibility ``-y`` x y H3); Replace ``-y+x`` with ``x-y``. -Rewrite Rplus_Ropp_l. -Intro H6; Generalize (Rlt_monotony ``(Rinv 2)`` ``x-y`` ``0`` (Rlt_Rinv ``2`` Hyp) H6); Rewrite Rmult_Or; Replace ``/2*(x-y)`` with ``(x-y)/2``. -Clear H6; Intro H6; Generalize (Rplus_le ``-(PI/2)`` x ``-(PI/2)`` ``-y`` H H2); Replace ``-(PI/2)+ (-(PI/2))`` with ``-PI``. -Replace `` x+ -y`` with ``x-y``. -Intro H7; Generalize (Rle_monotony ``(Rinv 2)`` ``-PI`` ``x-y`` (Rlt_le ``0`` ``/2`` (Rlt_Rinv ``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_pos ``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 (Rlt_anti_monotony ``(sin ((x-y)/2))`` ``0`` ``2*(cos ((x+y)/2))`` H10 H8); Intro H11; Rewrite Rmult_Or in H11; Rewrite Rmult_sym; Assumption. -Apply Rlt_Ropp; Apply PI2_Rlt_PI. -Unfold Rdiv; Apply Rmult_sym. -Unfold Rdiv; Rewrite <- Ropp_mul1; Apply Rmult_sym. -Reflexivity. -Pattern 1 PI; Rewrite double_var. -Rewrite Ropp_distr1. -Reflexivity. -Unfold Rdiv; Apply Rmult_sym. -Unfold Rminus; Apply Rplus_sym. -Unfold Rdiv; Apply Rmult_sym. -Unfold Rdiv; Apply Rmult_sym. -Unfold Rdiv; Apply Rmult_sym. -Unfold Rdiv. -Rewrite <- Ropp_mul1. -Apply Rmult_sym. -Pattern 1 PI; Rewrite double_var. -Rewrite Ropp_distr1. -Reflexivity. -Qed. - -Lemma sin_decreasing_0 : (x,y:R) ``x<=3*(PI/2)``-> ``PI/2<=x`` -> ``y<=3*(PI/2)``-> ``PI/2<=y`` -> ``(sin x)<(sin y)`` -> ``y<x``. -Intros; Rewrite <- (sin_PI_x x) in H3; Rewrite <- (sin_PI_x y) in H3; Generalize (Rlt_Ropp ``(sin (PI-x))`` ``(sin (PI-y))`` H3); Repeat Rewrite <- sin_neg; Generalize (Rle_compatibility ``-PI`` x ``3*(PI/2)`` H); Generalize (Rle_compatibility ``-PI`` ``PI/2`` x H0); Generalize (Rle_compatibility ``-PI`` y ``3*(PI/2)`` H1); Generalize (Rle_compatibility ``-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 Rlt_anti_compatibility with ``-PI``; Rewrite Rplus_sym; Replace ``y+ (-PI)`` with ``y-PI``. -Rewrite Rplus_sym; Replace ``x+ (-PI)`` with ``x-PI``. -Apply (sin_increasing_0 ``y-PI`` ``x-PI`` H4 H5 H6 H7 H8). -Reflexivity. -Reflexivity. -Unfold Rminus; Rewrite Ropp_distr1. -Rewrite Ropp_Ropp. -Apply Rplus_sym. -Unfold Rminus; Rewrite Ropp_distr1. -Rewrite Ropp_Ropp. -Apply Rplus_sym. -Pattern 2 PI; Rewrite double_var. -Rewrite Ropp_distr1. -Ring. -Unfold Rminus; Apply Rplus_sym. -Pattern 2 PI; Rewrite double_var. -Rewrite Ropp_distr1. -Ring. -Unfold Rminus; Apply Rplus_sym. -Qed. - -Lemma sin_decreasing_1 : (x,y:R) ``x<=3*(PI/2)``-> ``PI/2<=x`` -> ``y<=3*(PI/2)``-> ``PI/2<=y`` -> ``x<y`` -> ``(sin y)<(sin x)``. -Intros; Rewrite <- (sin_PI_x x); Rewrite <- (sin_PI_x y); Generalize (Rle_compatibility ``-PI`` x ``3*(PI/2)`` H); Generalize (Rle_compatibility ``-PI`` ``PI/2`` x H0); Generalize (Rle_compatibility ``-PI`` y ``3*(PI/2)`` H1); Generalize (Rle_compatibility ``-PI`` ``PI/2`` y H2); Generalize (Rlt_compatibility ``-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_Rlt; 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; Rewrite Ropp_distr1. -Rewrite Ropp_Ropp. -Apply Rplus_sym. -Unfold Rminus; Rewrite Ropp_distr1. -Rewrite Ropp_Ropp. -Apply Rplus_sym. -Unfold Rminus; Apply Rplus_sym. -Pattern 2 PI; Rewrite double_var; Ring. -Unfold Rminus; Apply Rplus_sym. -Pattern 2 PI; Rewrite double_var; Ring. -Qed. - -Lemma cos_increasing_0 : (x,y:R) ``PI<=x`` -> ``x<=2*PI`` ->``PI<=y`` -> ``y<=2*PI`` -> ``(cos x)<(cos y)`` -> ``x<y``. -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; 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 (Rle_compatibility ``-3*(PI/2)`` PI x H1); Generalize (Rle_compatibility ``-3*(PI/2)`` x ``2*PI`` H2); Generalize (Rle_compatibility ``-3*(PI/2)`` PI y H3); Generalize (Rle_compatibility ``-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 Rlt_anti_compatibility 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. -Rewrite Ropp_mul1. -Apply Rplus_sym. -Unfold Rminus. -Rewrite Ropp_mul1. -Apply Rplus_sym. -Pattern 3 PI; Rewrite double_var. -Ring. -Rewrite double; Pattern 3 4 PI; Rewrite double_var. -Ring. -Unfold Rminus. -Rewrite Ropp_mul1. -Apply Rplus_sym. -Unfold Rminus. -Rewrite Ropp_mul1. -Apply Rplus_sym. -Rewrite Rmult_1r. -Rewrite (double PI); Pattern 3 4 PI; Rewrite double_var. -Ring. -Rewrite Rmult_1r. -Rewrite (double PI); Pattern 3 4 PI; Rewrite double_var. -Ring. -Qed. - -Lemma cos_increasing_1 : (x,y:R) ``PI<=x`` -> ``x<=2*PI`` ->``PI<=y`` -> ``y<=2*PI`` -> ``x<y`` -> ``(cos x)<(cos y)``. -Intros x y H1 H2 H3 H4 H5; Generalize (Rle_compatibility ``-3*(PI/2)`` PI x H1); Generalize (Rle_compatibility ``-3*(PI/2)`` x ``2*PI`` H2); Generalize (Rle_compatibility ``-3*(PI/2)`` PI y H3); Generalize (Rle_compatibility ``-3*(PI/2)`` y ``2*PI`` H4); Generalize (Rlt_compatibility ``-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; 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_1r. -Rewrite (double PI); Pattern 3 4 PI; Rewrite double_var. -Ring. -Rewrite Rmult_1r. -Rewrite (double PI); Pattern 3 4 PI; Rewrite double_var. -Ring. -Rewrite (double PI); Pattern 3 4 PI; Rewrite double_var. -Ring. -Pattern 3 PI; Rewrite double_var; Ring. -Unfold Rminus. -Rewrite <- Ropp_mul1. -Apply Rplus_sym. -Unfold Rminus. -Rewrite <- Ropp_mul1. -Apply Rplus_sym. -Qed. - -Lemma cos_decreasing_0 : (x,y:R) ``0<=x``->``x<=PI``->``0<=y``->``y<=PI``->``(cos x)<(cos y)``->``y<x``. -Intros; Generalize (Rlt_Ropp (cos x) (cos y) H3); Repeat Rewrite <- neg_cos; Intro H4; Change ``(cos (y+PI))<(cos (x+PI))`` in H4; Rewrite (Rplus_sym x) in H4; Rewrite (Rplus_sym y) in H4; Generalize (Rle_compatibility PI ``0`` x H); Generalize (Rle_compatibility PI x PI H0); Generalize (Rle_compatibility PI ``0`` y H1); Generalize (Rle_compatibility PI y PI H2); Rewrite Rplus_Or. -Rewrite <- double. -Clear H H0 H1 H2 H3; Intros; Apply Rlt_anti_compatibility with ``PI``; Apply (cos_increasing_0 ``PI+y`` ``PI+x`` H0 H H2 H1 H4). -Qed. - -Lemma cos_decreasing_1 : (x,y:R) ``0<=x``->``x<=PI``->``0<=y``->``y<=PI``->``x<y``->``(cos y)<(cos x)``. -Intros; Apply Ropp_Rlt; Repeat Rewrite <- neg_cos; Rewrite (Rplus_sym x); Rewrite (Rplus_sym y); Generalize (Rle_compatibility PI ``0`` x H); Generalize (Rle_compatibility PI x PI H0); Generalize (Rle_compatibility PI ``0`` y H1); Generalize (Rle_compatibility PI y PI H2); Rewrite Rplus_Or. -Rewrite <- double. -Generalize (Rlt_compatibility 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 : (x,y:R) ~``(cos x)==0``->~``(cos y)==0``->``(tan x)-(tan y)==(sin (x-y))/((cos x)*(cos y))``. -Intros; Unfold tan;Rewrite sin_minus. -Unfold Rdiv. -Unfold Rminus. -Rewrite Rmult_Rplus_distrl. -Rewrite Rinv_Rmult. -Repeat Rewrite (Rmult_sym (sin x)). -Repeat Rewrite Rmult_assoc. -Rewrite (Rmult_sym (cos y)). -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r. -Rewrite (Rmult_sym (sin x)). -Apply Rplus_plus_r. -Rewrite <- Ropp_mul1. -Rewrite <- Ropp_mul3. -Rewrite (Rmult_sym ``/(cos x)``). -Repeat Rewrite Rmult_assoc. -Rewrite (Rmult_sym (cos x)). -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r. -Reflexivity. -Assumption. -Assumption. -Assumption. -Assumption. -Qed. - -Lemma tan_increasing_0 : (x,y:R) ``-(PI/4)<=x``->``x<=PI/4`` ->``-(PI/4)<=y``->``y<=PI/4``->``(tan x)<(tan y)``->``x<y``. -Intros; Generalize PI4_RLT_PI2; Intro H4; Generalize (Rlt_Ropp ``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_sym ``0`` (cos x) (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_sym ``0`` (cos y) (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 (Rle_Ropp ``-(PI/4)`` y H1); Rewrite Ropp_Ropp; Intro H10; Generalize (Rle_sym2 ``-y`` ``PI/4`` H10); Clear H10; Intro H10; Generalize (Rle_Ropp y ``PI/4`` H2); Intro H11; Generalize (Rle_sym2 ``-(PI/4)`` ``-y`` H11); Clear H11; Intro H11; Generalize (Rplus_le ``-(PI/4)`` x ``-(PI/4)`` ``-y`` H H11); Generalize (Rplus_le 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 (total_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_antirefl ``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_antirefl ``0`` H9). -Apply Rminus_lt; Assumption. -Pattern 1 PI; Rewrite double_var. -Unfold Rdiv. -Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_Rmult. -Rewrite Ropp_distr1. -Replace ``2*2`` with ``4``. -Reflexivity. -Ring. -DiscrR. -DiscrR. -Pattern 1 PI; Rewrite double_var. -Unfold Rdiv. -Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_Rmult. -Replace ``2*2`` with ``4``. -Reflexivity. -Ring. -DiscrR. -DiscrR. -Reflexivity. -Case (case_Rabsolu ``(sin (x-y))``); Intro H9. -Assumption. -Generalize (Rle_sym2 ``0`` ``(sin (x-y))`` H9); Clear H9; Intro H9; Generalize (Rlt_Rinv (cos x) HP1); Intro H10; Generalize (Rlt_Rinv (cos y) HP2); Intro H11; Generalize (Rmult_lt_pos (Rinv (cos x)) (Rinv (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_antirefl ``0`` (Rle_lt_trans ``0`` ``(sin (x-y))*/((cos x)*(cos y))`` ``0`` H13 H3)). -Rewrite Rinv_Rmult. -Reflexivity. -Assumption. -Assumption. -Qed. - -Lemma tan_increasing_1 : (x,y:R) ``-(PI/4)<=x``->``x<=PI/4`` ->``-(PI/4)<=y``->``y<=PI/4``->``x<y``->``(tan x)<(tan y)``. -Intros; Apply Rminus_lt; Generalize PI4_RLT_PI2; Intro H4; Generalize (Rlt_Ropp ``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_sym ``0`` (cos x) (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_sym ``0`` (cos y) (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 (Rlt_Rinv (cos x) HP1); Intro H10; Generalize (Rlt_Rinv (cos y) HP2); Intro H11; Generalize (Rmult_lt_pos (Rinv (cos x)) (Rinv (cos y)) H10 H11); Replace ``/(cos x)*/(cos y)`` with ``/((cos x)*(cos y))``. -Clear H10 H11; Intro H8; Generalize (Rle_Ropp y ``PI/4`` H2); Intro H11; Generalize (Rle_sym2 ``-(PI/4)`` ``-y`` H11); Clear H11; Intro H11; Generalize (Rplus_le ``-(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 (Rlt_Ropp ``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 (Rlt_anti_monotony ``(sin (x-y))`` ``0`` ``/((cos x)*(cos y))`` H2 H8); Rewrite Rmult_Or; Intro H4; Assumption. -Pattern 1 PI; Rewrite double_var. -Unfold Rdiv. -Rewrite Rmult_Rplus_distrl. -Repeat Rewrite Rmult_assoc. -Rewrite <- Rinv_Rmult. -Replace ``2*2`` with ``4``. -Rewrite Ropp_distr1. -Reflexivity. -Ring. -DiscrR. -DiscrR. -Reflexivity. -Apply Rinv_Rmult; Assumption. -Qed. - -Lemma sin_incr_0 : (x,y:R) ``-(PI/2)<=x``->``x<=PI/2``->``-(PI/2)<=y``->``y<=PI/2``->``(sin x)<=(sin y)``->``x<=y``. -Intros; Case (total_order (sin x) (sin y)); Intro H4; [Left; Apply (sin_increasing_0 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_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_antirefl (sin y) H8)]] | Elim (Rlt_antirefl (sin x) (Rle_lt_trans (sin x) (sin y) (sin x) H3 H5))]]. -Qed. - -Lemma sin_incr_1 : (x,y:R) ``-(PI/2)<=x``->``x<=PI/2``->``-(PI/2)<=y``->``y<=PI/2``->``x<=y``->``(sin x)<=(sin y)``. -Intros; Case (total_order x y); Intro H4; [Left; Apply (sin_increasing_1 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_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_antirefl y H8)]] | Elim (Rlt_antirefl x (Rle_lt_trans x y x H3 H5))]]. -Qed. - -Lemma sin_decr_0 : (x,y:R) ``x<=3*(PI/2)``->``PI/2<=x``->``y<=3*(PI/2)``->``PI/2<=y``-> ``(sin x)<=(sin y)`` -> ``y<=x``. -Intros; Case (total_order (sin x) (sin y)); Intro H4; [Left; Apply (sin_decreasing_0 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order x y); Intro H6; [Generalize (sin_decreasing_1 x y H H0 H1 H2 H6); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl (sin y) H8) | Elim H6; Intro H7; [Right; Symmetry; Assumption | Left; Assumption]] | Elim (Rlt_antirefl (sin x) (Rle_lt_trans (sin x) (sin y) (sin x) H3 H5))]]. -Qed. - -Lemma sin_decr_1 : (x,y:R) ``x<=3*(PI/2)``-> ``PI/2<=x`` -> ``y<=3*(PI/2)``-> ``PI/2<=y`` -> ``x<=y`` -> ``(sin y)<=(sin x)``. -Intros; Case (total_order x y); Intro H4; [Left; Apply (sin_decreasing_1 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_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_antirefl y H8) | Elim H6; Intro H7; [Right; Symmetry; Assumption | Left; Assumption]] | Elim (Rlt_antirefl x (Rle_lt_trans x y x H3 H5))]]. -Qed. - -Lemma cos_incr_0 : (x,y:R) ``PI<=x`` -> ``x<=2*PI`` ->``PI<=y`` -> ``y<=2*PI`` -> ``(cos x)<=(cos y)`` -> ``x<=y``. -Intros; Case (total_order (cos x) (cos y)); Intro H4; [Left; Apply (cos_increasing_0 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_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_antirefl (cos y) H8)]] | Elim (Rlt_antirefl (cos x) (Rle_lt_trans (cos x) (cos y) (cos x) H3 H5))]]. -Qed. - -Lemma cos_incr_1 : (x,y:R) ``PI<=x`` -> ``x<=2*PI`` ->``PI<=y`` -> ``y<=2*PI`` -> ``x<=y`` -> ``(cos x)<=(cos y)``. -Intros; Case (total_order x y); Intro H4; [Left; Apply (cos_increasing_1 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_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_antirefl y H8)]] | Elim (Rlt_antirefl x (Rle_lt_trans x y x H3 H5))]]. -Qed. - -Lemma cos_decr_0 : (x,y:R) ``0<=x``->``x<=PI``->``0<=y``->``y<=PI``->``(cos x)<=(cos y)`` -> ``y<=x``. -Intros; Case (total_order (cos x) (cos y)); Intro H4; [Left; Apply (cos_decreasing_0 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_order x y); Intro H6; [Generalize (cos_decreasing_1 x y H H0 H1 H2 H6); Intro H8; Rewrite H5 in H8; Elim (Rlt_antirefl (cos y) H8) | Elim H6; Intro H7; [Right; Symmetry; Assumption | Left; Assumption]] | Elim (Rlt_antirefl (cos x) (Rle_lt_trans (cos x) (cos y) (cos x) H3 H5))]]. -Qed. - -Lemma cos_decr_1 : (x,y:R) ``0<=x``->``x<=PI``->``0<=y``->``y<=PI``->``x<=y``->``(cos y)<=(cos x)``. -Intros; Case (total_order x y); Intro H4; [Left; Apply (cos_decreasing_1 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_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_antirefl y H8) | Elim H6; Intro H7; [Right; Symmetry; Assumption | Left; Assumption]] | Elim (Rlt_antirefl x (Rle_lt_trans x y x H3 H5))]]. -Qed. - -Lemma tan_incr_0 : (x,y:R) ``-(PI/4)<=x``->``x<=PI/4`` ->``-(PI/4)<=y``->``y<=PI/4``->``(tan x)<=(tan y)``->``x<=y``. -Intros; Case (total_order (tan x) (tan y)); Intro H4; [Left; Apply (tan_increasing_0 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_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_antirefl (tan y) H8)]] | Elim (Rlt_antirefl (tan x) (Rle_lt_trans (tan x) (tan y) (tan x) H3 H5))]]. -Qed. - -Lemma tan_incr_1 : (x,y:R) ``-(PI/4)<=x``->``x<=PI/4`` ->``-(PI/4)<=y``->``y<=PI/4``->``x<=y``->``(tan x)<=(tan y)``. -Intros; Case (total_order x y); Intro H4; [Left; Apply (tan_increasing_1 x y H H0 H1 H2 H4) | Elim H4; Intro H5; [Case (total_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_antirefl y H8)]] | Elim (Rlt_antirefl x (Rle_lt_trans x y x H3 H5))]]. +Theorem sin_gt_0 : forall x:R, 0 < x -> x < PI -> 0 < sin x. +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. +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. +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. +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. +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. +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. +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. +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. +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. +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. +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. +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). +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). +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). +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). +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. +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. +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. +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. +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. +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. +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. +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. +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). +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. +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. +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. +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. +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. +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. +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. +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. +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. +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. +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. +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. +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 : (x:R) (EXT k:Z | x==(Rmult (IZR k) PI)) -> (sin x)==R0. -Intros. -Elim H; Intros. -Apply (Zcase_sign x0). -Intro. -Rewrite H1 in H0. -Simpl in H0. -Rewrite H0; Rewrite Rmult_Ol; Apply sin_0. -Intro. -Cut `0<=x0`. -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. -Rewrite <- (Rplus_Ol ``2*(INR x2)*PI``). -Rewrite sin_period. -Apply sin_0. -Rewrite H5. -Rewrite S_INR; Rewrite mult_INR. -Simpl. -Rewrite Rmult_Rplus_distrl. -Rewrite Rmult_1l; Rewrite sin_plus. -Rewrite sin_PI. -Rewrite Rmult_Or. -Rewrite <- (Rplus_Ol ``2*(INR x2)*PI``). -Rewrite sin_period. -Rewrite sin_0; Ring. -Apply le_IZR. -Left; Apply IZR_lt. -Assert H2 := Zgt_iff_lt. -Elim (H2 x0 `0`); Intros. -Apply H3; Assumption. -Intro. -Rewrite H0. -Replace ``(sin ((IZR x0)*PI))`` with ``-(sin (-(IZR x0)*PI))``. -Cut `0<=-x0`. -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. -Rewrite <- (Rplus_Ol ``2*(INR x2)*PI``). -Rewrite sin_period. -Rewrite sin_0; Ring. -Rewrite H5. -Rewrite S_INR; Rewrite mult_INR. -Simpl. -Rewrite Rmult_Rplus_distrl. -Rewrite Rmult_1l; Rewrite sin_plus. -Rewrite sin_PI. -Rewrite Rmult_Or. -Rewrite <- (Rplus_Ol ``2*(INR x2)*PI``). -Rewrite sin_period. -Rewrite sin_0; Ring. -Apply le_IZR. -Apply Rle_anti_compatibility with ``(IZR x0)``. -Rewrite Rplus_Or. -Rewrite Ropp_Ropp_IZR. -Rewrite Rplus_Ropp_r. -Left; Replace R0 with (IZR `0`); [Apply IZR_lt | Reflexivity]. -Assumption. -Rewrite <- sin_neg. -Rewrite Ropp_mul1. -Rewrite Ropp_Ropp. -Reflexivity. -Qed. - -Lemma sin_eq_0_0 : (x:R) (sin x)==R0 -> (EXT k:Z | x==(Rmult (IZR k) PI)). -Intros. -Assert H0 := (euclidian_division x PI PI_neq0). -Elim H0; Intros q H1. -Elim H1; Intros r H2. -Exists q. -Cut r==R0. -Intro. -Elim H2; Intros H4 _; Rewrite H4; Rewrite H3. -Apply Rplus_Or. -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_Ol in H. -Rewrite Rplus_Ol in H. -Assert H6 := (without_div_Od ? ? H). -Elim H6; Intro. -Assert H8 := (sin2_cos2 ``(IZR q)*PI``). -Rewrite H5 in H8; Rewrite H7 in H8. -Rewrite Rsqr_O in H8. -Rewrite Rplus_Or in H8. -Elim R1_neq_R0; Symmetry; Assumption. -Cut r==R0\/``0<r<PI``. -Intro; Elim H8; Intro. -Assumption. -Elim H9; Intros. -Assert H12 := (sin_gt_0 ? H10 H11). -Rewrite H7 in H12; Elim (Rlt_antirefl ? H12). -Rewrite Rabsolu_right in H4. -Elim H4; Intros. -Case (total_order R0 r); Intro. -Right; Split; Assumption. -Elim H10; Intro. -Left; Symmetry; Assumption. -Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H8 H11)). -Apply Rle_sym1. -Left; Apply PI_RGT_0. -Apply sin_eq_0_1. -Exists q; Reflexivity. -Qed. - -Lemma cos_eq_0_0 : (x:R) (cos x)==R0 -> (EXT k : Z | ``x==(IZR k)*PI+PI/2``). -Intros x H; Rewrite -> cos_sin in H; Generalize (sin_eq_0_0 (Rplus (Rdiv PI (INR (2))) x) H); Intro H2; Elim H2; Intros x0 H3; Exists (Zminus x0 (inject_nat (S O))); Rewrite <- Z_R_minus; Ring; Rewrite Rmult_sym; Rewrite <- H3; Unfold INR. -Rewrite (double_var ``-PI``); Unfold Rdiv; Ring. -Qed. - -Lemma cos_eq_0_1 : (x:R) (EXT k : Z | ``x==(IZR k)*PI+PI/2``) -> ``(cos x)==0``. -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_O. -Apply eq_Ropp; Apply sin_eq_0_1; Exists x0; Reflexivity. -Pattern 2 PI; Rewrite (double_var PI); Ring. -Qed. - -Lemma sin_eq_O_2PI_0 : (x:R) ``0<=x`` -> ``x<=2*PI`` -> ``(sin x)==0`` -> ``x==0``\/``x==PI``\/``x==2*PI``. -Intros; Generalize (sin_eq_0_0 x H1); Intro. -Elim H2; Intros k0 H3. -Case (total_order PI x); Intro. -Rewrite H3 in H4; Rewrite H3 in H0. -Right; Right. -Generalize (Rlt_monotony_r ``/PI`` ``PI`` ``(IZR k0)*PI`` (Rlt_Rinv ``PI`` PI_RGT_0) H4); Rewrite Rmult_assoc; Repeat Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Intro; Generalize (Rle_monotony_r ``/PI`` ``(IZR k0)*PI`` ``2*PI`` (Rlt_le ``0`` ``/PI`` (Rlt_Rinv ``PI`` PI_RGT_0)) H0); Repeat Rewrite Rmult_assoc; Repeat Rewrite <- Rinv_r_sym. -Repeat Rewrite Rmult_1r; Intro; Generalize (Rlt_compatibility (IZR `-2`) ``1`` (IZR k0) H5); Rewrite <- plus_IZR. -Replace ``(IZR (NEG (xO xH)))+1`` with ``-1``. -Intro; Generalize (Rle_compatibility (IZR `-2`) (IZR k0) ``2`` H6); Rewrite <- plus_IZR. -Replace ``(IZR (NEG (xO xH)))+2`` with ``0``. -Intro; Cut ``-1 < (IZR (Zplus (NEG (xO xH)) k0)) < 1``. -Intro; Generalize (one_IZR_lt1 (Zplus (NEG (xO xH)) k0) H9); Intro. -Cut k0=`2`. -Intro; Rewrite H11 in H3; Rewrite H3; Simpl. -Reflexivity. -Rewrite <- (Zplus_inverse_l `2`) in H10; Generalize (Zsimpl_plus_l `-2` k0 `2` H10); Intro; Assumption. -Split. -Assumption. -Apply Rle_lt_trans with ``0``. -Assumption. -Apply Rlt_R0_R1. -Simpl; Ring. -Simpl; Ring. -Apply PI_neq0. -Apply PI_neq0. -Elim H4; Intro. -Right; Left. -Symmetry; Assumption. -Left. -Rewrite H3 in H5; Rewrite H3 in H; Generalize (Rlt_monotony_r ``/PI`` ``(IZR k0)*PI`` PI (Rlt_Rinv ``PI`` PI_RGT_0) H5); Rewrite Rmult_assoc; Repeat Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Intro; Generalize (Rle_monotony_r ``/PI`` ``0`` ``(IZR k0)*PI`` (Rlt_le ``0`` ``/PI`` (Rlt_Rinv ``PI`` PI_RGT_0)) H); Repeat Rewrite Rmult_assoc; Repeat Rewrite <- Rinv_r_sym. -Rewrite Rmult_1r; Rewrite Rmult_Ol; Intro. -Cut ``-1 < (IZR (k0)) < 1``. -Intro; Generalize (one_IZR_lt1 k0 H8); Intro; Rewrite H9 in H3; Rewrite H3; Simpl; Apply Rmult_Ol. -Split. -Apply Rlt_le_trans with ``0``. -Rewrite <- Ropp_O; Apply Rgt_Ropp; Apply Rlt_R0_R1. -Assumption. -Assumption. -Apply PI_neq0. -Apply PI_neq0. -Qed. - -Lemma sin_eq_O_2PI_1 : (x:R) ``0<=x`` -> ``x<=2*PI`` -> ``x==0``\/``x==PI``\/``x==2*PI`` -> ``(sin x)==0``. -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 : (x:R) ``R0<=x`` -> ``x<=2*PI`` -> ``(cos x)==0`` -> ``x==(PI/2)``\/``x==3*(PI/2)``. -Intros; Case (total_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 (Rle_compatibility ``PI/2`` ``0`` x H); Rewrite Rplus_Or; Rewrite H6; Intro. -Elim (Rlt_antirefl ``0`` (Rlt_le_trans ``0`` ``PI/2`` ``0`` PI2_RGT_0 H7)). -Left. -Generalize (Rplus_plus_r ``-(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 3 PI; Rewrite (double_var PI); Ring. -Ring. -Right. -Generalize (Rplus_plus_r ``-(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 3 4 PI; Rewrite (double_var PI); Ring. -Ring. -Left; Replace ``2*PI`` with ``PI/2+3*(PI/2)``. -Apply Rlt_compatibility; Assumption. -Rewrite (double PI); Pattern 3 4 PI; Rewrite (double_var PI); Ring. -Apply ge0_plus_ge0_is_ge0. -Left; Unfold Rdiv; Apply Rmult_lt_pos. -Apply PI_RGT_0. -Apply Rlt_Rinv; 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 (Rlt_compatibility ``-(PI/2)`` ``3*PI/2`` ``(IZR k0)*PI+PI/2`` H3); Generalize (Rle_compatibility ``-(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 (Rlt_monotony ``/PI`` ``PI`` ``(IZR k0)*PI`` (Rlt_Rinv PI PI_RGT_0) H7); Generalize (Rle_monotony ``/PI`` ``(IZR k0)*PI`` ``3*(PI/2)`` (Rlt_le ``0`` ``/PI`` (Rlt_Rinv 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 (Rlt_compatibility (IZR `-2`) ``1`` (IZR k0) H9); Rewrite <- plus_IZR. -Replace ``(IZR (NEG (xO xH)))+1`` with ``-1``. -Intro; Generalize (Rle_compatibility (IZR `-2`) (IZR k0) ``3*/2`` H8); Rewrite <- plus_IZR. -Replace ``(IZR (NEG (xO xH)))+2`` with ``0``. -Intro; Cut `` -1 < (IZR (Zplus (NEG (xO xH)) k0)) < 1``. -Intro; Generalize (one_IZR_lt1 (Zplus (NEG (xO xH)) k0) H12); Intro. -Cut k0=`2`. -Intro; Rewrite H14 in H8. -Assert Hyp : ``0<2``. -Sup0. -Generalize (Rle_monotony ``2`` ``(IZR (POS (xO xH)))`` ``3*/2`` (Rlt_le ``0`` ``2`` Hyp) H8); Simpl. -Replace ``2*2`` with ``4``. -Replace ``2*(3*/2)`` with ``3``. -Intro; Cut ``3<4``. -Intro; Elim (Rlt_antirefl ``3`` (Rlt_le_trans ``3`` ``4`` ``3`` H16 H15)). -Generalize (Rlt_compatibility ``3`` ``0`` ``1`` Rlt_R0_R1); Rewrite Rplus_Or. -Replace ``3+1`` with ``4``. -Intro; Assumption. -Ring. -Symmetry; Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m. -DiscrR. -Ring. -Rewrite <- (Zplus_inverse_l `2`) in H13; Generalize (Zsimpl_plus_l `-2` k0 `2` H13); Intro; Assumption. -Split. -Assumption. -Apply Rle_lt_trans with ``(IZR (NEG (xO xH)))+3*/2``. -Assumption. -Simpl; Replace ``-2+3*/2`` with ``-(1*/2)``. -Apply Rlt_trans with ``0``. -Rewrite <- Ropp_O; Apply Rlt_Ropp. -Apply Rmult_lt_pos; [Apply Rlt_R0_R1 | Apply Rlt_Rinv; Sup0]. -Apply Rlt_R0_R1. -Rewrite Rmult_1l; Apply r_Rmult_mult with ``2``. -Rewrite Ropp_mul3; Rewrite <- Rinv_r_sym. -Rewrite Rmult_Rplus_distr; Rewrite <- Rmult_assoc; Rewrite Rinv_r_simpl_m. -Ring. -DiscrR. -DiscrR. -DiscrR. -Simpl; Ring. -Simpl; Ring. -Apply PI_neq0. -Unfold Rdiv; Pattern 1 ``3``; Rewrite (Rmult_sym ``3``); Repeat Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1l; Apply Rmult_sym. -Apply PI_neq0. -Symmetry; Rewrite (Rmult_sym ``/PI``); Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym. -Apply Rmult_1r. -Apply PI_neq0. -Rewrite double; Pattern 3 4 PI; Rewrite double_var; Ring. -Ring. -Pattern 1 PI; Rewrite double_var; Ring. -Qed. - -Lemma cos_eq_0_2PI_1 : (x:R) ``0<=x`` -> ``x<=2*PI`` -> ``x==PI/2``\/``x==3*(PI/2)`` -> ``(cos x)==0``. -Intros x H1 H2 H3; Elim H3; Intro H4; [ Rewrite H4; Rewrite -> cos_PI2; Reflexivity | Rewrite H4; Rewrite -> cos_3PI2; Reflexivity ]. -Qed. +Lemma sin_eq_0_1 : forall x:R, ( exists k : Z | x = IZR k * PI) -> sin x = 0. +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. +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. +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; ring; rewrite Rmult_comm; rewrite <- H3; + unfold INR in |- *. +rewrite (double_var (- PI)); unfold Rdiv in |- *; ring. +Qed. + +Lemma cos_eq_0_1 : + forall x:R, ( exists k : Z | x = IZR k * PI + PI / 2) -> cos x = 0. +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. +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. +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). +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. +intros x H1 H2 H3; elim H3; intro H4; + [ rewrite H4; rewrite cos_PI2; reflexivity + | rewrite H4; rewrite cos_3PI2; reflexivity ]. +Qed.
\ No newline at end of file |