CoRN.transc.Pi
Definition of Pi
Fixpoint pi_seq (n : nat) : IR :=
match n with
| O ⇒ [0]
| S p ⇒ pi_seq p[+]Cos (pi_seq p)
end.
Opaque Cosine.
This sequence is nonnegative and the cosine of any number between
[0] and any of its values is strictly positive; therefore the
sequence is strictly increasing.
Lemma pi_seq_nonneg : ∀ n : nat, [0] [<=] pi_seq n.
Proof.
intro; elim (pi_seq_lemma n); auto.
Qed.
Lemma cos_pi_seq_pos : ∀ n t, [0] [<=] t → t [<=] pi_seq n → [0] [<] Cos t.
Proof.
intro; elim (pi_seq_lemma n); auto.
Qed.
Lemma pi_seq_incr : ∀ n : nat, pi_seq n [<] pi_seq (S n).
Proof.
intro; astepr (pi_seq n[+]Cos (pi_seq n)).
apply shift_less_plus'; astepl ZeroR.
apply cos_pi_seq_pos with n.
apply pi_seq_nonneg.
apply leEq_reflexive.
Qed.
Trivial---but useful---consequences.
Lemma sin_pi_seq_mon : ∀ x y n, [0] [<=] x → x [<=] y → y [<=] pi_seq n → Sin x [<=] Sin y.
Proof.
intros; simpl in |- ×.
apply Derivative_imp_resp_leEq with realline I Cosine.
Deriv.
auto.
simpl in |- *; auto.
simpl in |- *; auto.
intros.
apply leEq_glb.
intros y0 H2 Hy.
apply less_leEq.
apply less_wdr with (Cos y0).
2: simpl in |- *; algebra.
inversion_clear H2.
apply cos_pi_seq_pos with n.
apply leEq_transitive with x; auto.
eapply leEq_wdl.
apply H3.
eapply eq_transitive.
apply Min_comm.
apply leEq_imp_Min_is_lft; auto.
apply leEq_transitive with y; auto.
eapply leEq_wdr.
apply H4.
eapply eq_transitive.
apply Max_comm.
apply leEq_imp_Max_is_rht; auto.
Qed.
Lemma sin_pi_seq_nonneg : ∀ n : nat, [0] [<=] Sin (pi_seq n).
Proof.
intro.
astepl (Sin [0]).
apply sin_pi_seq_mon with n.
apply leEq_reflexive.
apply pi_seq_nonneg.
apply leEq_reflexive.
Qed.
Lemma sin_pi_seq_gt_one : ∀ t n, [1] [<=] t → t [<=] pi_seq (S n) → Sin [1] [<=] Sin t.
Proof.
intros.
apply sin_pi_seq_mon with (S n); auto.
apply less_leEq; apply pos_one.
Qed.
Lemma cos_pi_seq_mon : ∀ x y n, [0] [<=] x → x [<=] y → y [<=] pi_seq n → Cos y [<=] Cos x.
Proof.
intros.
apply power_cancel_leEq with 2.
auto.
apply less_leEq; apply cos_pi_seq_pos with n.
auto.
apply leEq_transitive with y; auto.
apply inv_cancel_leEq.
rstepl ([1][-]Cos x[^]2[-][1]).
rstepr ([1][-]Cos y[^]2[-][1]).
apply minus_resp_leEq.
apply leEq_wdl with (Sin x[^]2).
apply leEq_wdr with (Sin y[^]2).
apply nexp_resp_leEq.
astepl (Sin [0]); apply sin_pi_seq_mon with n.
apply leEq_reflexive.
auto.
apply leEq_transitive with y; auto.
apply sin_pi_seq_mon with n; auto.
astepl (Sin y[^]2[+]Cos y[^]2[-]Cos y[^]2).
apply cg_minus_wd.
Step_final (Cos y[^]2[+]Sin y[^]2).
algebra.
astepl (Sin x[^]2[+]Cos x[^]2[-]Cos x[^]2).
apply cg_minus_wd.
Step_final (Cos x[^]2[+]Sin x[^]2).
algebra.
Qed.
An auxiliary result.
Lemma Sin_One_pos : [0] [<] Sin [1].
Proof.
astepl (Sin [0]).
simpl in |- ×.
apply Derivative_imp_resp_less with realline I Cosine.
Deriv.
apply pos_one.
simpl in |- *; auto.
simpl in |- *; auto.
intros.
apply less_leEq_trans with (Cos [1]).
apply less_wdr with (Cos (pi_seq 1)).
2: astepl (Cos ([0][+]Cos [0])); apply Cos_wd; Step_final (Cos [0]).
apply cos_pi_seq_pos with 1.
simpl in |- ×.
astepr (Cos [0]); astepr OneR.
apply less_leEq; apply pos_one.
apply leEq_reflexive.
apply leEq_glb.
intros y H Hy; apply leEq_wdr with (Cos y).
2: simpl in |- *; algebra.
inversion_clear H.
apply cos_pi_seq_mon with 1.
eapply leEq_wdl.
apply H0.
apply leEq_imp_Min_is_lft; apply less_leEq; apply pos_one.
eapply leEq_wdr.
apply H1.
apply leEq_imp_Max_is_rht; apply less_leEq; apply pos_one.
apply eq_imp_leEq; simpl in |- ×.
Step_final (Cos [0]).
Qed.
We can now prove that this is a Cauchy sequence. We define π as
twice its limit.
Lemma pi_seq_Cauchy : Cauchy_prop pi_seq.
Proof.
intros e H.
cut ([0] [<] pi_seq 2[-]pi_seq 1). intro H0.
assert (H1 : pi_seq 2[-]pi_seq 1 [#] [0]). apply Greater_imp_ap; auto.
cut (Sin [1] [<] [1]).
intro Sin_One_less_One.
elim qi_yields_zero with (e := Sin [1][*]e[/] _[//]H1) (q := [1][-]Sin [1]).
intros N HN.
∃ (S (S N)); intros.
apply AbsIR_imp_AbsSmall.
apply leEq_wdl with (pi_seq m[-]pi_seq (S (S N))).
2: apply eq_symmetric; apply AbsIR_eq_x.
2: apply shift_leEq_minus; astepl (pi_seq (S (S N))).
2: apply local_mon_imp_mon'.
2: intro; apply pi_seq_incr; auto.
2: auto.
cut (m = S (pred m)); [ intro | apply S_pred with (S N); auto ].
apply leEq_wdl with (Sum (S (S N)) (pred m) (fun i : nat ⇒ pi_seq (S i) [-]pi_seq i)).
2: eapply eq_transitive.
2: apply Mengolli_Sum_gen with (f := pi_seq).
2: algebra.
2: auto with arith.
2: rewrite <- H3; algebra.
set (z := [1][-]Sin [1]) in ×.
apply leEq_transitive with (Sum (S (S N)) (pred m)
(fun i : nat ⇒ z[^]pred i[*] (pi_seq 2[-]pi_seq 1))).
apply Sum_resp_leEq.
rewrite <- H3; auto.
intros; apply pi_seq_bnd''.
apply le_trans with (S (S N)); auto with arith.
eapply leEq_wdl.
2: apply eq_symmetric; apply Sum_comm_scal with (s := fun i : nat ⇒ z[^]pred i).
rstepl (Sum (S (S N)) (pred m) (fun i : nat ⇒ z[^]pred i) [*] (pi_seq 2[-]pi_seq 1)).
apply shift_mult_leEq with H1.
auto.
apply leEq_wdl with (Sum (S N) (pred (pred m)) (fun i : nat ⇒ z[^]i)).
2: cut (pred m = S (pred (pred m))); [ intro | apply S_pred with N; auto with arith ].
2: pattern (pred m) at 2 in |- *; rewrite H4.
2: apply Sum_shift; algebra.
cut (z[-][1] [#] [0]). intro H4.
eapply leEq_wdl.
2: apply eq_symmetric; apply Sum_c_exp with (H := H4).
rstepl ((z[^]S (pred (pred m)) [/] _[//]H4) [-] (z[^]S N[/] _[//]H4)).
apply leEq_transitive with ( [--] (z[^]S N) [/] _[//]H4).
apply shift_minus_leEq; rstepr ZeroR; apply less_leEq.
unfold z in |- ×.
rstepl ( [--] (([1][-]Sin [1]) [^]S (pred (pred m))) [/] Sin [1][//] pos_ap_zero _ _ Sin_One_pos).
apply shift_div_less.
apply Sin_One_pos.
astepr ZeroR; astepr ( [--]ZeroR).
apply inv_resp_less.
apply less_wdl with (ZeroR[^]S (pred (pred m))).
2: simpl in |- *; algebra.
apply nexp_resp_less.
auto with arith.
apply leEq_reflexive.
apply shift_less_minus; astepl (Sin [1]).
auto.
unfold z at 2 in |- ×.
rstepl (z[^]S N[/] _[//]pos_ap_zero _ _ Sin_One_pos).
apply shift_div_leEq.
apply Sin_One_pos.
eapply leEq_transitive.
eapply leEq_transitive.
2: apply HN.
simpl in |- ×.
astepr (nexp IR N z[*][1]); apply mult_resp_leEq_lft.
unfold z in |- ×.
apply shift_minus_leEq; apply shift_leEq_plus'.
astepl ZeroR; apply less_leEq; apply Sin_One_pos.
astepr (z[^]N); apply nexp_resp_nonneg.
unfold z in |- ×.
apply shift_leEq_minus; astepl (Sin [1]).
apply less_leEq; auto.
apply eq_imp_leEq.
rational.
unfold z in |- ×.
rstepl ( [--] (Sin [1])).
apply inv_resp_ap_zero.
apply Greater_imp_ap; apply Sin_One_pos.
apply shift_leEq_minus.
apply less_leEq; astepl (Sin [1]); auto.
apply shift_minus_less; apply shift_less_plus'.
astepl ZeroR; apply Sin_One_pos.
apply div_resp_pos.
auto.
apply mult_resp_pos; auto.
apply Sin_One_pos.
apply Sin_less_One.
apply cos_pi_seq_pos with 1.
apply less_leEq; apply pos_one.
simpl in |- ×.
apply eq_imp_leEq; Step_final (Cos [0]).
apply shift_less_minus; astepl (pi_seq 1).
apply pi_seq_incr; auto.
Qed.
Definition π := Two[*]Lim (Build_CauchySeq _ _ pi_seq_Cauchy).
Lemma pos_cos : ∀ x, [0] [<=] x → x [<] π [/]TwoNZ → [0] [<] Cos x.
Proof.
intros x H H0.
assert (H1 : x [<] Lim (Build_CauchySeq _ _ pi_seq_Cauchy)).
apply less_wdr with (π [/]TwoNZ); auto; unfold π in |- *; rational.
elim (less_Lim_so_less_seq _ _ H1); intros N HN.
apply cos_pi_seq_pos with N.
auto.
apply less_leEq; auto.
Qed.
Lemma Cos_HalfPi : Cos (π [/]TwoNZ) [=] [0].
Proof.
transitivity (Cos (Lim (Build_CauchySeq _ _ pi_seq_Cauchy))).
apply Cos_wd; unfold π in |- *; rational.
astepr (Lim (Build_CauchySeq _ _ pi_seq_Cauchy) [-] Lim (Build_CauchySeq _ _ pi_seq_Cauchy)).
assert (H : Cauchy_prop (fun n : nat ⇒ pi_seq (S n))).
apply conv_seq_imp_conv_subseq with pi_seq S; auto with arith.
intro; ∃ (S n); split; apply lt_n_Sn.
simpl in |- *; auto.
algebra.
apply pi_seq_Cauchy.
transitivity
(Lim (Build_CauchySeq _ _ H) [-]Lim (Build_CauchySeq _ _ pi_seq_Cauchy)).
2: apply cg_minus_wd; algebra.
2: apply Lim_subseq_eq_Lim_seq with S; auto with arith.
2: intro; ∃ (S n); split; apply lt_n_Sn.
2: simpl in |- *; auto.
2: algebra.
2: left; intros; simpl in |- ×.
2: apply local_mon_imp_mon'; auto; apply pi_seq_incr.
eapply eq_transitive.
2: apply Lim_minus.
assert (H0 : Cauchy_prop (fun n : nat ⇒ Cosine (pi_seq n) (cos_domain _))).
apply Cauchy_prop_wd with (fun n : nat ⇒ pi_seq (S n) [-]pi_seq n).
2: intros; simpl in |- *; rational.
exact (Cauchy_minus (Build_CauchySeq _ _ H) (Build_CauchySeq _ _ pi_seq_Cauchy)).
transitivity (Lim (Build_CauchySeq _ _ H0)).
2: apply Lim_wd'; intros; simpl in |- *; rational.
simpl in |- ×.
apply Continuous_imp_comm_Lim with (e := OneR) (x := Build_CauchySeq _ _ pi_seq_Cauchy)
(Hxn := fun n : nat ⇒ cos_domain (pi_seq n)).
apply pos_one.
apply Included_imp_Continuous with realline; Contin.
Qed.
Lemma HalfPi_gt_pi_seq : ∀ n : nat, pi_seq n [<] π [/]TwoNZ.
Proof.
intros.
unfold π in |- ×.
rstepr (Lim (Build_CauchySeq _ _ pi_seq_Cauchy)).
apply less_leEq_trans with (pi_seq (S n)).
apply pi_seq_incr.
apply str_leEq_seq_so_leEq_Lim.
∃ (S n); intros.
apply local_mon_imp_mon'.
apply pi_seq_incr.
auto.
Qed.
Lemma pos_Pi : [0] [<] π.
Proof.
astepr (Two[*]π [/]TwoNZ).
apply mult_resp_pos.
apply pos_two.
astepl (pi_seq 0).
apply HalfPi_gt_pi_seq.
Qed.
End Properties_of_Pi.
Hint Resolve Cos_HalfPi: algebra.
Section Pi_and_Order.
Properties of Pi
[--]π [<] [--]π[/]Two [<] [--] π[/]Four [<] [0] [<] π[/]Four [<] π[/]Two [<] π
Lemma pos_HalfPi : [0] [<] π [/]TwoNZ.
Proof.
apply pos_div_two; apply pos_Pi.
Qed.
Lemma pos_QuarterPi : [0] [<] π [/]FourNZ.
Proof.
apply pos_div_four; apply pos_Pi.
Qed.
Lemma QuarterPi_less_HalfPi : π [/]FourNZ [<] π [/]TwoNZ.
Proof.
rstepl ((π [/]TwoNZ) [/]TwoNZ).
apply pos_div_two'; apply pos_HalfPi.
Qed.
Lemma HalfPi_less_Pi : π [/]TwoNZ [<] π.
Proof.
apply pos_div_two'; apply pos_Pi.
Qed.
Lemma QuarterPi_less_Pi : π [/]FourNZ [<] π.
Proof.
apply pos_div_four'; apply pos_Pi.
Qed.
Lemma neg_invPi : [--]π [<] [0].
Proof.
astepr ( [--]ZeroR); apply inv_resp_less; apply pos_Pi.
Qed.
Lemma neg_invHalfPi : [--] (π [/]TwoNZ) [<] [0].
Proof.
astepr ( [--]ZeroR); apply inv_resp_less; apply pos_HalfPi.
Qed.
Lemma neg_invQuarterPi : [--] (π [/]FourNZ) [<] [0].
Proof.
astepr ( [--]ZeroR); apply inv_resp_less; apply pos_QuarterPi.
Qed.
Lemma invHalfPi_less_invQuarterPi : [--] (π [/]TwoNZ) [<] [--] (π [/]FourNZ).
Proof.
apply inv_resp_less; apply QuarterPi_less_HalfPi.
Qed.
Lemma invPi_less_invHalfPi : [--]π [<] [--] (π [/]TwoNZ).
Proof.
apply inv_resp_less; apply HalfPi_less_Pi.
Qed.
Lemma invPi_less_invQuarterPi : [--]π [<] [--] (π [/]FourNZ).
Proof.
apply inv_resp_less; apply QuarterPi_less_Pi.
Qed.
Lemma invPi_less_Pi : [--]π [<] π.
Proof.
apply less_transitive_unfolded with ZeroR.
apply neg_invPi.
apply pos_Pi.
Qed.
Lemma invPi_less_HalfPi : [--]π [<] π [/]TwoNZ.
Proof.
apply less_transitive_unfolded with ZeroR.
apply neg_invPi.
apply pos_HalfPi.
Qed.
Lemma invPi_less_QuarterPi : [--]π [<] π [/]FourNZ.
Proof.
apply less_transitive_unfolded with ZeroR.
apply neg_invPi.
apply pos_QuarterPi.
Qed.
Lemma invHalfPi_less_Pi : [--] (π [/]TwoNZ) [<] π.
Proof.
apply less_transitive_unfolded with ZeroR.
apply neg_invHalfPi.
apply pos_Pi.
Qed.
Lemma invHalfPi_less_HalfPi : [--] (π [/]TwoNZ) [<] π [/]TwoNZ.
Proof.
apply less_transitive_unfolded with ZeroR.
apply neg_invHalfPi.
apply pos_HalfPi.
Qed.
Lemma invHalfPi_less_QuarterPi : [--] (π [/]TwoNZ) [<] π [/]FourNZ.
Proof.
apply less_transitive_unfolded with ZeroR.
apply neg_invHalfPi.
apply pos_QuarterPi.
Qed.
Lemma invQuarterPi_less_Pi : [--] (π [/]FourNZ) [<] π.
Proof.
apply less_transitive_unfolded with ZeroR.
apply neg_invQuarterPi.
apply pos_Pi.
Qed.
Lemma invQuarterPi_less_HalfPi : [--] (π [/]FourNZ) [<] π [/]TwoNZ.
Proof.
apply less_transitive_unfolded with ZeroR.
apply neg_invQuarterPi.
apply pos_HalfPi.
Qed.
Lemma invQuarterPi_less_QuarterPi : [--] (π [/]FourNZ) [<] π [/]FourNZ.
Proof.
apply less_transitive_unfolded with ZeroR.
apply neg_invQuarterPi.
apply pos_QuarterPi.
Qed.
End Pi_and_Order.
Hint Resolve pos_Pi pos_HalfPi pos_QuarterPi QuarterPi_less_HalfPi
HalfPi_less_Pi QuarterPi_less_Pi neg_invPi neg_invHalfPi neg_invQuarterPi
invHalfPi_less_invQuarterPi invPi_less_invHalfPi invPi_less_invQuarterPi
invPi_less_Pi invPi_less_HalfPi invPi_less_QuarterPi invHalfPi_less_Pi
invHalfPi_less_HalfPi invHalfPi_less_QuarterPi invQuarterPi_less_Pi
invQuarterPi_less_HalfPi invQuarterPi_less_QuarterPi: piorder.
Section Sin_And_Cos.
Lemma Cos_double : ∀ x : IR, Cos (Two[*]x) [=] Two[*]Cos x[^]2[-][1].
Proof.
intros.
astepl (Cos (x[+]x)).
astepl (Cos x[*]Cos x[-]Sin x[*]Sin x).
astepl (Cos x[^]2[-]Sin x[^]2).
rstepr (Cos x[^]2[-] ([1][-]Cos x[^]2)).
apply cg_minus_wd; algebra.
astepr (Cos x[^]2[+]Sin x[^]2[-]Cos x[^]2); rational.
Qed.
Lemma Sin_double : ∀ x : IR, Sin (Two[*]x) [=] Two[*]Sin x[*]Cos x.
Proof.
intros.
astepl (Sin (x[+]x)).
eapply eq_transitive_unfolded.
apply Sin_plus.
rational.
Qed.
Lemma Tan_double : ∀ x Hx Hx' H, Tan (Two[*]x) Hx' [=] (Two[*]Tan x Hx[/] [1][-]Tan x Hx[^]2[//]H).
Proof.
intros.
cut (Dom Tang (x[+]x)). intro H0.
astepl (Tan (x[+]x) H0).
cut ([1][-]Tan x Hx[*]Tan x Hx [#] [0]). intro H1.
eapply eq_transitive_unfolded.
apply Tan_plus with (Hx := Hx) (Hy := Hx) (H := H1).
simpl in |- *; rational.
astepl ([1][-]Tan x Hx[^]2). auto.
apply dom_wd with (Two[*]x); algebra.
Qed.
Lemma Cos_QuarterPi : ∀ Hpos H, Cos (π [/]FourNZ) [=] ([1][/] sqrt Two Hpos[//]H).
Proof.
intros.
apply square_eq_pos.
apply recip_resp_pos.
apply power_cancel_less with 2.
apply sqrt_nonneg.
astepr (Two:IR).
simpl in |- *; fold (Two:IR) in |- *; astepl ZeroR.
apply pos_two.
apply pos_cos; PiSolve.
eapply eq_transitive_unfolded.
2: apply sqrt_lemma.
astepr ((ZeroR[+][1]) [/]TwoNZ).
astepr ((Cos (π [/]TwoNZ) [+][1]) [/]TwoNZ).
rstepl ((Two[*]Cos (π [/]FourNZ) [^]2[-][1][+][1]) [/]TwoNZ).
apply div_wd.
2: algebra.
apply bin_op_wd_unfolded.
2: algebra.
transitivity (Cos (Two[*]π [/]FourNZ)).
apply eq_symmetric_unfolded; apply Cos_double.
apply Cos_wd; rational.
Qed.
Lemma Sin_QuarterPi : ∀ Hpos H, Sin (π [/]FourNZ) [=] ([1][/] sqrt Two Hpos[//]H).
Proof.
intros.
apply square_eq_pos.
apply recip_resp_pos.
apply power_cancel_less with 2.
apply sqrt_nonneg.
astepr (Two:IR).
simpl in |- *; fold (Two:IR) in |- *; astepl ZeroR.
apply pos_two.
apply less_leEq_trans with (Sin ([1] [/]TwoNZ)).
cut ([0] [<] Cos ([1] [/]TwoNZ)). intro H0.
apply less_wdr with ((Sin [1][/] _[//]pos_ap_zero _ _ H0) [/]TwoNZ).
apply pos_div_two.
apply div_resp_pos.
auto.
apply Sin_One_pos.
rstepr ((Two[*]Sin ([1] [/]TwoNZ) [*]Cos ([1] [/]TwoNZ) [/] _[//]pos_ap_zero _ _ H0) [/]TwoNZ).
repeat apply div_wd.
astepl (Sin (Two[*][1] [/]TwoNZ)).
apply Sin_double.
algebra.
algebra.
apply pos_cos; PiSolve.
apply pos_div_two; apply pos_one.
apply less_transitive_unfolded with (pi_seq 1).
simpl in |- *; astepr (Cos [0]); astepr OneR.
astepl (OneR [/]TwoNZ); apply pos_div_two'; apply pos_one.
apply HalfPi_gt_pi_seq.
elim (less_Lim_so_less_seq (Build_CauchySeq _ _ pi_seq_Cauchy) (π [/]FourNZ)).
intros N HN; apply sin_pi_seq_mon with N.
apply less_leEq; apply pos_div_two; apply pos_one.
apply shift_div_leEq.
apply pos_two.
astepl (Cos [0]); astepl ([0][+]Cos [0]).
rstepr (π [/]TwoNZ).
apply less_leEq; apply (HalfPi_gt_pi_seq 1).
apply less_leEq; auto.
eapply less_wdr.
apply QuarterPi_less_HalfPi.
unfold π in |- *; rational.
eapply eq_transitive_unfolded.
2: apply sqrt_lemma.
rstepr ([1][-]OneR [/]TwoNZ).
astepr (Cos (π [/]FourNZ) [^]2[+]Sin (π [/]FourNZ) [^]2[-][1] [/]TwoNZ).
rstepl (([1][/] _[//]H) [^]2[+]Sin (π [/]FourNZ) [^]2[-] ([1][/] _[//]H) [^]2).
apply cg_minus_wd.
apply bin_op_wd_unfolded.
apply nexp_wd.
apply eq_symmetric; apply Cos_QuarterPi.
algebra.
apply eq_symmetric; apply sqrt_lemma.
Qed.
Hint Resolve Sin_QuarterPi Cos_QuarterPi: algebra.
Opaque Sine Cosine.
Lemma Tan_QuarterPi : ∀ H, Tan (π [/]FourNZ) H [=] [1].
Proof.
intros.
set (pos2 := less_leEq _ _ _ (pos_two IR)) in ×.
cut (sqrt Two pos2 [#] [0]).
2: apply Greater_imp_ap.
2: apply power_cancel_less with 2.
2: apply sqrt_nonneg.
2: apply less_wdl with ZeroR.
2: astepr (Two:IR); apply pos_two.
2: simpl in |- *; algebra.
intro H0.
unfold Tan in |- *; simpl in |- ×.
astepr (([1][/] _[//]H0) [/] _[//]recip_ap_zero _ _ H0).
apply div_wd.
astepr (Sin (π [/]FourNZ)).
simpl in |- *; algebra.
astepr (Cos (π [/]FourNZ)).
simpl in |- *; algebra.
Qed.
Lemma Sin_HalfPi : Sin (π [/]TwoNZ) [=] [1].
Proof.
transitivity (Sin (Two[*]π [/]FourNZ)).
apply Sin_wd; rational.
eapply eq_transitive.
apply Sin_double.
astepr ((Two:IR) [*][1] [/]TwoNZ).
eapply eq_transitive.
apply eq_symmetric; apply mult_assoc.
apply mult_wdr.
cut (sqrt _ (less_leEq _ _ _ (pos_two IR)) [#] [0]). intro H.
eapply eq_transitive.
2: symmetry; apply (sqrt_lemma _ H).
simpl in |- ×.
eapply eq_transitive.
2: apply mult_assoc.
eapply eq_transitive.
apply eq_symmetric; apply one_mult.
apply mult_wdr.
apply mult_wd.
apply Sin_QuarterPi.
apply Cos_QuarterPi.
apply Greater_imp_ap; apply sqrt_less.
simpl in |- *; astepl ZeroR; apply (pos_two IR).
Qed.
Hint Resolve Sin_HalfPi: algebra.
Lemma Sin_plus_HalfPi : ∀ x : IR, Sin (x[+]π [/]TwoNZ) [=] Cos x.
Proof.
intro.
eapply eq_transitive.
apply Sin_plus.
astepl (Sin x[*][0][+]Cos x[*][1]).
Step_final ([0][+]Cos x).
Qed.
Lemma Sin_HalfPi_minus : ∀ x : IR, Sin (π [/]TwoNZ[-]x) [=] Cos x.
Proof.
intros.
unfold cg_minus in |- ×.
astepl (Sin ( [--]x[+]π [/]TwoNZ)).
eapply eq_transitive.
apply Sin_plus_HalfPi.
algebra.
Qed.
Lemma Cos_plus_HalfPi : ∀ x : IR, Cos (x[+]π [/]TwoNZ) [=] [--] (Sin x).
Proof.
intro.
eapply eq_transitive.
apply Cos_plus.
astepl (Cos x[*][0][-]Sin x[*][1]).
Step_final ([0][-]Sin x).
Qed.
Lemma Cos_HalfPi_minus : ∀ x : IR, Cos (π [/]TwoNZ[-]x) [=] Sin x.
Proof.
intros.
unfold cg_minus in |- ×.
astepl (Cos ( [--]x[+]π [/]TwoNZ)).
eapply eq_transitive.
apply Cos_plus_HalfPi.
Step_final (Sin [--][--]x).
Qed.
Lemma Sin_Pi : Sin π [=] [0].
Proof.
transitivity (Sin (π [/]TwoNZ[+]π [/]TwoNZ)).
apply Sin_wd; rational.
eapply eq_transitive_unfolded.
apply Sin_plus_HalfPi.
algebra.
Qed.
Lemma Cos_Pi : Cos π [=] [--][1].
Proof.
transitivity (Cos (π [/]TwoNZ[+]π [/]TwoNZ)).
apply Cos_wd; rational.
eapply eq_transitive.
apply Cos_plus_HalfPi.
algebra.
Qed.
Lemma Sin_plus_Pi : ∀ x : IR, Sin (x[+]π) [=] [--] (Sin x).
Proof.
intros.
transitivity (Sin (x[+]π [/]TwoNZ[+]π [/]TwoNZ)).
apply Sin_wd; rational.
eapply eq_transitive.
apply Sin_plus_HalfPi.
apply Cos_plus_HalfPi.
Qed.
Lemma Cos_plus_Pi : ∀ x : IR, Cos (x[+]π) [=] [--] (Cos x).
Proof.
intros.
transitivity (Cos (x[+]π [/]TwoNZ[+]π [/]TwoNZ)).
apply Cos_wd; rational.
eapply eq_transitive.
apply Cos_plus_HalfPi.
apply un_op_wd_unfolded; apply Sin_plus_HalfPi.
Qed.
Lemma Tan_plus_HalfPi : ∀ x Hx Hx' H, Tan (x[+]π[/]TwoNZ) Hx[=]([--][1][/](Tan x Hx')[//]H).
Proof.
intros x Hy Hx H.
set (y:=x[+]π [/]TwoNZ) in ×.
assert (H0:Cos y[#][0]).
destruct Hy as [[] [[] Hy]].
apply (Hy I).
assert (H1:Cos x[#][0]).
clear H.
destruct Hx as [[] [[] Hx]].
apply (Hx I).
rewrite (Tan_Sin_over_Cos y Hy H0).
unfold y.
assert (H2:([--](Sin x))[#][0]) by (now csetoid_rewrite_rev (Cos_plus_HalfPi x)).
stepr (Cos x[/]([--](Sin x))[//]H2).
apply div_wd.
apply Sin_plus_HalfPi.
apply Cos_plus_HalfPi.
clear H0.
rstepl (((Cos x[/][--](Sin x)[//]H2)[*](Tan x Hx))[/](Tan x Hx)[//]H).
apply div_wd;[|apply eq_reflexive].
rewrite (Tan_Sin_over_Cos x Hx H1).
rational.
Qed.
Hint Resolve Sin_plus_Pi Cos_plus_Pi: algebra.
Lemma Sin_periodic : ∀ x : IR, Sin (x[+]Two[*]π) [=] Sin x.
Proof.
intro.
transitivity (Sin (x[+]π[+]π)).
apply Sin_wd; rational.
astepl ( [--] (Sin (x[+]π))).
Step_final ( [--][--] (Sin x)).
Qed.
Lemma Cos_periodic : ∀ x : IR, Cos (x[+]Two[*]π) [=] Cos x.
Proof.
intro.
transitivity (Cos (x[+]π[+]π)).
apply Cos_wd; rational.
astepl ( [--] (Cos (x[+]π))).
Step_final ( [--][--] (Cos x)).
Qed.
Lemma Sin_periodic_Z : ∀ (x : IR) z, Sin (x[+]zring z[*](Two[*]π)) [=] Sin x.
Proof.
intros x z; revert x; induction z using Zind; intros x.
rational.
unfold Zsucc.
rewrite → zring_plus.
rstepl (Sin (x[+]zring z[*](Two[*]π)[+]Two[*]π)).
rewrite → Sin_periodic.
auto.
unfold Zpred.
rewrite → zring_plus.
rstepl (Sin (x[-]Two[*]π[+]zring z[*](Two[*]π))).
rstepr (Sin (x[-]Two[*]π[+]Two[*]π)).
rewrite → Sin_periodic.
auto.
Qed.
Lemma Cos_periodic_Z : ∀ (x : IR) z, Cos (x[+]zring z[*](Two[*]π)) [=] Cos x.
Proof.
intros x z; revert x; induction z using Zind; intros x.
rational.
unfold Zsucc.
rewrite → zring_plus.
rstepl (Cos (x[+]zring z[*](Two[*]π)[+]Two[*]π)).
rewrite → Cos_periodic.
auto.
unfold Zpred.
rewrite → zring_plus.
rstepl (Cos (x[-]Two[*]π[+]zring z[*](Two[*]π))).
rstepr (Cos (x[-]Two[*]π[+]Two[*]π)).
rewrite → Cos_periodic.
auto.
Qed.
Lemma Tan_periodic : ∀ (x : IR) Hx Hx', Tan (x[+]π) Hx' [=] Tan x Hx.
Proof.
intros.
cut (Cos x [#] [0]). intro H.
assert (H0 : [--] (Cos x) [#] [0]). apply inv_resp_ap_zero; auto.
transitivity (Sin x[/] _[//]H).
2: unfold Tan, Tang in |- *; simpl in |- *; algebra.
rstepr ( [--] (Sin x) [/] _[//]H0).
assert (H1 : Cos (x[+]π) [#] [0]). astepl ( [--] (Cos x)); auto.
astepr (Sin (x[+]π) [/] _[//]H1).
unfold Tan, Tang in |- *; simpl in |- *; algebra.
inversion_clear Hx.
inversion_clear X0.
simpl in |- *; auto.
Qed.
Lemma Cos_one_gt_0 : [0] [<] Cos [1].
Proof.
apply cos_pi_seq_pos with (1%nat).
apply less_leEq.
apply pos_one.
unfold pi_seq.
rewrite → Cos_zero.
apply eq_imp_leEq.
rational.
Qed.
Lemma Pi_gt_2 : Two [<] π.
Proof.
unfold π.
rstepl (Two [*] [1]:IR).
apply mult_resp_less_lft.
apply less_leEq_trans with ([1] [+] (Cos [1])).
rstepl ([1] [+] [0]:IR).
apply plus_resp_leEq_less.
apply eq_imp_leEq.
reflexivity.
apply Cos_one_gt_0.
apply str_leEq_seq_so_leEq_Lim.
∃ (2%nat).
intros i iH.
change ([1] [+] Cos [1][<=] pi_seq i).
induction i.
elimtype False.
auto with ×.
clear IHi.
induction i.
elimtype False.
auto with ×.
clear iH.
clear IHi.
induction i.
unfold pi_seq.
rewrite → Cos_zero.
setoid_replace ([0] [+] [1]:IR) with ([1]:IR); [|rational].
apply eq_imp_leEq.
reflexivity.
apply leEq_transitive with (pi_seq (S (S i))).
assumption.
apply less_leEq.
apply pi_seq_incr.
apply pos_two.
Qed.
End Sin_And_Cos.
Hint Resolve Cos_double Sin_double Tan_double Cos_QuarterPi Sin_QuarterPi
Tan_QuarterPi Sin_Pi Cos_Pi Sin_HalfPi Sin_plus_HalfPi Sin_HalfPi_minus
Cos_plus_HalfPi Cos_HalfPi_minus Sin_plus_Pi Cos_plus_Pi Sin_periodic
Cos_periodic Tan_periodic: algebra.