Section Properties_of_Pi.


Definition of Pi



π is defined as twice the first positive zero of the cosine. In order to do this, we follow the construction described in Bishop 1969, section 7.

Fixpoint pi_seq (n : N) : IR :=
  match n with
  | O => 0
  | S p => pi_seq p[+]Cos (pi_seq p)
  end.



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 : forall n : N, 0 [<=] pi_seq n.

Lemma cos_pi_seq_pos : forall n t, 0 [<=] t -> t [<=] pi_seq n -> 0 [<] Cos t.

Lemma pi_seq_incr : forall n : N, pi_seq n [<] pi_seq (S n).

Trivial---but useful---consequences.

Lemma sin_pi_seq_mon : forall x y n, 0 [<=] x -> x [<=] y -> y [<=] pi_seq n -> Sin x [<=] Sin y.

Lemma sin_pi_seq_nonneg : forall n : N, 0 [<=] Sin (pi_seq n).

Lemma sin_pi_seq_gt_one : forall t n, 1 [<=] t -> t [<=] pi_seq (S n) -> Sin 1 [<=] Sin t.

Lemma cos_pi_seq_mon : forall x y n, 0 [<=] x -> x [<=] y -> y [<=] pi_seq n -> Cos y [<=] Cos x.


An auxiliary result.

Lemma Sin_One_pos : 0 [<] Sin 1.

We can now prove that this is a Cauchy sequence. We define π as twice its limit.

Lemma pi_seq_Cauchy : Cauchy_prop pi_seq.




Definition π := 2[*]Lim (Build_CauchySeq _ _ pi_seq_Cauchy).

For x∈[0,π/2), (Cos x) > 0; cos(π/2)=0.

Lemma pos_cos : forall x, 0 [<=] x -> x [<] π [/]2 -> 0 [<] Cos x.

Lemma Cos_HalfPi : Cos (π [/]2) [=] 0.

Convergence to π / 2 is increasing; therefore, π is positive.

Lemma HalfPi_gt_pi_seq : forall n : N, pi_seq n [<] π [/]2.

Lemma pos_Pi : 0 [<] π.

End Properties_of_Pi.


Section Pi_and_Order.

Properties of Pi



The following are trivial ordering properties of multiples of π that will be used so often that it is convenient to state as lemmas; also, we define a hint database that automatically tries to apply this lemmas, to make proof development easier.

A summary of what is being proved is simply:
[--]π [<] [--]π[/]2 [<] [--] π[/]4 [<] 0 [<] π[/]4 [<] π[/]2 [<] π

PiSolve will prove any of these inequalities.

Lemma pos_HalfPi : 0 [<] π [/]2.

Lemma pos_QuarterPi : 0 [<] π [/]4.

Lemma QuarterPi_less_HalfPi : π [/]4 [<] π [/]2.

Lemma HalfPi_less_Pi : π [/]2 [<] π.

Lemma QuarterPi_less_Pi : π [/]4 [<] π.

Lemma neg_invPi : [--]π [<] 0.

Lemma neg_invHalfPi : [--] (π [/]2) [<] 0.

Lemma neg_invQuarterPi : [--] (π [/]4) [<] 0.

Lemma invHalfPi_less_invQuarterPi : [--] (π [/]2) [<] [--] (π [/]4).

Lemma invPi_less_invHalfPi : [--]π [<] [--] (π [/]2).

Lemma invPi_less_invQuarterPi : [--]π [<] [--] (π [/]4).

Lemma invPi_less_Pi : [--]π [<] π.

Lemma invPi_less_HalfPi : [--]π [<] π [/]2.

Lemma invPi_less_QuarterPi : [--]π [<] π [/]4.

Lemma invHalfPi_less_Pi : [--] (π [/]2) [<] π.

Lemma invHalfPi_less_HalfPi : [--] (π [/]2) [<] π [/]2.

Lemma invHalfPi_less_QuarterPi : [--] (π [/]2) [<] π [/]4.

Lemma invQuarterPi_less_Pi : [--] (π [/]4) [<] π.

Lemma invQuarterPi_less_HalfPi : [--] (π [/]4) [<] π [/]2.

Lemma invQuarterPi_less_QuarterPi : [--] (π [/]4) [<] π [/]4.

End Pi_and_Order.



Section Sin_And_Cos.

More formulas



We now move back to trigonometric identities: sine, cosine and tangent of the double.

Lemma Cos_double : forall x : IR, Cos (2[*]x) [=] 2[*]Cos x[^]2[-]1.

Lemma Sin_double : forall x : IR, Sin (2[*]x) [=] 2[*]Sin x[*]Cos x.

Lemma Tan_double : forall x Hx Hx' H, Tan (2[*]x) Hx' [=] (2[*]Tan x Hx[/] 1[-]Tan x Hx[^]2[//]H).





Value of trigonometric functions at π/4.

Lemma Cos_QuarterPi : forall Hpos H, Cos (π [/]4) [=] (1[/] sqrt 2 Hpos[//]H).

Lemma Sin_QuarterPi : forall Hpos H, Sin (π [/]4) [=] (1[/] sqrt 2 Hpos[//]H).




Lemma Tan_QuarterPi : forall H, Tan (π [/]4) H [=] 1.

Shifting sine and cosine by π/2 and π.

Lemma Sin_HalfPi : Sin (π [/]2) [=] 1.



Lemma Sin_plus_HalfPi : forall x : IR, Sin (x[+]π [/]2) [=] Cos x.

Lemma Sin_HalfPi_minus : forall x : IR, Sin (π [/]2[-]x) [=] Cos x.

Lemma Cos_plus_HalfPi : forall x : IR, Cos (x[+]π [/]2) [=] [--] (Sin x).

Lemma Cos_HalfPi_minus : forall x : IR, Cos (π [/]2[-]x) [=] Sin x.

Lemma Sin_Pi : Sin π [=] 0.

Lemma Cos_Pi : Cos π [=] [--]1.

Lemma Sin_plus_Pi : forall x : IR, Sin (x[+]π) [=] [--] (Sin x).

Lemma Cos_plus_Pi : forall x : IR, Cos (x[+]π) [=] [--] (Cos x).

Lemma Tan_plus_HalfPi : forall x Hx Hx' H, Tan (x[+]π[/]2) Hx[=]([--]1[/](Tan x Hx')[//]H).


Sine and cosine have period 2 π, tangent has period π.

Lemma Sin_periodic : forall x : IR, Sin (x[+]2[*]π) [=] Sin x.

Lemma Cos_periodic : forall x : IR, Cos (x[+]2[*]π) [=] Cos x.

Lemma Sin_periodic_Z : forall (x : IR) z, Sin (x[+]zring z[*](2[*]π)) [=] Sin x.

Lemma Cos_periodic_Z : forall (x : IR) z, Cos (x[+]zring z[*](2[*]π)) [=] Cos x.

Lemma Tan_periodic : forall (x : IR) Hx Hx', Tan (x[+]π) Hx' [=] Tan x Hx.




Lemma Cos_one_gt_0 : 0 [<] Cos 1.

Lemma Pi_gt_2 : 2 [<] π.

End Sin_And_Cos.