# Library Coq.Reals.Rtrigo

Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Export Rtrigo_fun.
Require Export Rtrigo_def.
Require Export Rtrigo_alt.
Require Export Cos_rel.
Require Export Cos_plus.
Require Import ZArith_base.
Require Import Zcomplements.
Require Import Classical_Prop.
Local Open Scope nat_scope.
Local Open Scope R_scope.

sin_PI2 is the only remaining axiom
Axiom sin_PI2 : sin (PI / 2) = 1.

Lemma PI_neq0 : PI <> 0.

Lemma cos_minus : forall x y:R, cos (x - y) = cos x * cos y + sin x * sin y.

Lemma sin2_cos2 : forall x:R, Rsqr (sin x) + Rsqr (cos x) = 1.

Lemma cos2 : forall x:R, Rsqr (cos x) = 1 - Rsqr (sin x).

Lemma cos_PI2 : cos (PI / 2) = 0.

Lemma cos_PI : cos PI = -1.

Lemma sin_PI : sin PI = 0.

Lemma neg_cos : forall x:R, cos (x + PI) = - cos x.

Lemma sin_cos : forall x:R, sin x = - cos (PI / 2 + x).

Lemma sin_plus : forall x y:R, sin (x + y) = sin x * cos y + cos x * sin y.

Lemma sin_minus : forall x y:R, sin (x - y) = sin x * cos y - cos x * sin y.

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).

# Some properties of cos, sin and tan

Lemma sin2 : forall x:R, Rsqr (sin x) = 1 - Rsqr (cos x).

Lemma sin_2a : forall x:R, sin (2 * x) = 2 * sin x * cos x.

Lemma cos_2a : forall x:R, cos (2 * x) = cos x * cos x - sin x * sin x.

Lemma cos_2a_cos : forall x:R, cos (2 * x) = 2 * cos x * cos x - 1.

Lemma cos_2a_sin : forall x:R, cos (2 * x) = 1 - 2 * sin x * sin x.

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).

Lemma sin_neg : forall x:R, sin (- x) = - sin x.

Lemma cos_neg : forall x:R, cos (- x) = cos x.

Lemma tan_0 : tan 0 = 0.

Lemma tan_neg : forall x:R, tan (- x) = - tan x.

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).

Lemma cos_3PI2 : cos (3 * (PI / 2)) = 0.

Lemma sin_2PI : sin (2 * PI) = 0.

Lemma cos_2PI : cos (2 * PI) = 1.

Lemma neg_sin : forall x:R, sin (x + PI) = - sin x.

Lemma sin_PI_x : forall x:R, sin (PI - x) = sin x.

Lemma sin_period : forall (x:R) (k:nat), sin (x + 2 * INR k * PI) = sin x.

Lemma cos_period : forall (x:R) (k:nat), cos (x + 2 * INR k * PI) = cos x.

Lemma sin_shift : forall x:R, sin (PI / 2 - x) = cos x.

Lemma cos_shift : forall x:R, cos (PI / 2 - x) = sin x.

Lemma cos_sin : forall x:R, cos x = sin (PI / 2 + x).

Lemma PI2_RGT_0 : 0 < PI / 2.

Lemma SIN_bound : forall x:R, -1 <= sin x <= 1.

Lemma COS_bound : forall x:R, -1 <= cos x <= 1.

Lemma cos_sin_0 : forall x:R, ~ (cos x = 0 /\ sin x = 0).

Lemma cos_sin_0_var : forall x:R, cos x <> 0 \/ sin x <> 0.

# Using series definitions of cos and sin

Definition sin_lb (a:R) : R := sin_approx a 3.
Definition sin_ub (a:R) : R := sin_approx a 4.
Definition cos_lb (a:R) : R := cos_approx a 3.
Definition cos_ub (a:R) : R := cos_approx a 4.

Lemma sin_lb_gt_0 : forall a:R, 0 < a -> a <= PI / 2 -> 0 < sin_lb a.

Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a.

Lemma COS :
forall a:R, - PI / 2 <= a -> a <= PI / 2 -> cos_lb a <= cos a <= cos_ub a.

Lemma _PI2_RLT_0 : - (PI / 2) < 0.

Lemma PI4_RLT_PI2 : PI / 4 < PI / 2.

Lemma PI2_Rlt_PI : PI / 2 < PI.

# Increasing and decreasing of cos and sin

Theorem sin_gt_0 : forall x:R, 0 < x -> x < PI -> 0 < sin x.

Theorem cos_gt_0 : forall x:R, - (PI / 2) < x -> x < PI / 2 -> 0 < cos x.

Lemma sin_ge_0 : forall x:R, 0 <= x -> x <= PI -> 0 <= sin x.

Lemma cos_ge_0 : forall x:R, - (PI / 2) <= x -> x <= PI / 2 -> 0 <= cos x.

Lemma sin_le_0 : forall x:R, PI <= x -> x <= 2 * PI -> sin x <= 0.

Lemma cos_le_0 : forall x:R, PI / 2 <= x -> x <= 3 * (PI / 2) -> cos x <= 0.

Lemma sin_lt_0 : forall x:R, PI < x -> x < 2 * PI -> sin x < 0.

Lemma sin_lt_0_var : forall x:R, - PI < x -> x < 0 -> sin x < 0.

Lemma cos_lt_0 : forall x:R, PI / 2 < x -> x < 3 * (PI / 2) -> cos x < 0.

Lemma tan_gt_0 : forall x:R, 0 < x -> x < PI / 2 -> 0 < tan x.

Lemma tan_lt_0 : forall x:R, - (PI / 2) < x -> x < 0 -> tan x < 0.

Lemma cos_ge_0_3PI2 :
forall x:R, 3 * (PI / 2) <= x -> x <= 2 * PI -> 0 <= cos x.

Lemma form1 :
forall p q:R, cos p + cos q = 2 * cos ((p - q) / 2) * cos ((p + q) / 2).

Lemma form2 :
forall p q:R, cos p - cos q = -2 * sin ((p - q) / 2) * sin ((p + q) / 2).

Lemma form3 :
forall p q:R, sin p + sin q = 2 * cos ((p - q) / 2) * sin ((p + q) / 2).

Lemma form4 :
forall p q:R, sin p - sin q = 2 * cos ((p + q) / 2) * sin ((p - q) / 2).

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.

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.

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.

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.

Lemma cos_increasing_0 :
forall x y:R,
PI <= x -> x <= 2 * PI -> PI <= y -> y <= 2 * PI -> cos x < cos y -> x < y.

Lemma cos_increasing_1 :
forall x y:R,
PI <= x -> x <= 2 * PI -> PI <= y -> y <= 2 * PI -> x < y -> cos x < cos y.

Lemma cos_decreasing_0 :
forall x y:R,
0 <= x -> x <= PI -> 0 <= y -> y <= PI -> cos x < cos y -> y < x.

Lemma cos_decreasing_1 :
forall x y:R,
0 <= x -> x <= PI -> 0 <= y -> y <= PI -> x < y -> cos y < cos x.

Lemma tan_diff :
forall x y:R,
cos x <> 0 -> cos y <> 0 -> tan x - tan y = sin (x - y) / (cos x * cos y).

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.

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.

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.

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.

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.

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.

Lemma cos_incr_0 :
forall x y:R,
PI <= x ->
x <= 2 * PI -> PI <= y -> y <= 2 * PI -> cos x <= cos y -> x <= y.

Lemma cos_incr_1 :
forall x y:R,
PI <= x ->
x <= 2 * PI -> PI <= y -> y <= 2 * PI -> x <= y -> cos x <= cos y.

Lemma cos_decr_0 :
forall x y:R,
0 <= x -> x <= PI -> 0 <= y -> y <= PI -> cos x <= cos y -> y <= x.

Lemma cos_decr_1 :
forall x y:R,
0 <= x -> x <= PI -> 0 <= y -> y <= PI -> x <= y -> cos y <= cos x.

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.

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.

Lemma sin_eq_0_1 : forall x:R, (exists k : Z, x = IZR k * PI) -> sin x = 0.

Lemma sin_eq_0_0 : forall x:R, sin x = 0 -> exists k : Z, x = IZR k * PI.

Lemma cos_eq_0_0 :
forall x:R, cos x = 0 -> exists k : Z, x = IZR k * PI + PI / 2.
ring_simplify. rewrite <- H3; simpl; field;repeat split; discrR.

Lemma cos_eq_0_1 :
forall x:R, (exists k : Z, x = IZR k * PI + PI / 2) -> cos x = 0.

Lemma sin_eq_O_2PI_0 :
forall x:R,
0 <= x -> x <= 2 * PI -> sin x = 0 -> x = 0 \/ x = PI \/ x = 2 * PI.

Lemma sin_eq_O_2PI_1 :
forall x:R,
0 <= x -> x <= 2 * PI -> x = 0 \/ x = PI \/ x = 2 * PI -> sin x = 0.

Lemma cos_eq_0_2PI_0 :
forall x:R,
0 <= x -> x <= 2 * PI -> cos x = 0 -> x = PI / 2 \/ x = 3 * (PI / 2).

Lemma cos_eq_0_2PI_1 :
forall x:R,
0 <= x -> x <= 2 * PI -> x = PI / 2 \/ x = 3 * (PI / 2) -> cos x = 0.