1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/transc/Pi".
24 Section Properties_of_Pi.
27 (*#* printing Pi %\ensuremath{\pi}% #π# *)
29 (*#* **Definition of Pi
31 [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.
34 inline cic:/CoRN/transc/Pi/pi_seq.con.
46 inline cic:/CoRN/transc/Pi/pi_seq_lemma.con.
51 This sequence is nonnegative and the cosine of any number between
52 [Zero] and any of its values is strictly positive; therefore the
53 sequence is strictly increasing.
56 inline cic:/CoRN/transc/Pi/pi_seq_nonneg.con.
58 inline cic:/CoRN/transc/Pi/cos_pi_seq_pos.con.
60 inline cic:/CoRN/transc/Pi/pi_seq_incr.con.
62 (*#* Trivial---but useful---consequences. *)
64 inline cic:/CoRN/transc/Pi/sin_pi_seq_mon.con.
66 inline cic:/CoRN/transc/Pi/sin_pi_seq_nonneg.con.
68 inline cic:/CoRN/transc/Pi/sin_pi_seq_gt_one.con.
70 inline cic:/CoRN/transc/Pi/cos_pi_seq_mon.con.
74 inline cic:/CoRN/transc/Pi/pi_seq_gt_one.con.
80 inline cic:/CoRN/transc/Pi/pi_seq_bnd.con.
82 inline cic:/CoRN/transc/Pi/pi_seq_bnd'.con.
84 inline cic:/CoRN/transc/Pi/pi_seq_bnd''.con.
88 (*#* An auxiliary result. *)
90 inline cic:/CoRN/transc/Pi/Sin_One_pos.con.
92 (*#* We can now prove that this is a Cauchy sequence. We define [Pi] as
96 inline cic:/CoRN/transc/Pi/pi_seq_Cauchy.con.
98 inline cic:/CoRN/transc/Pi/Pi.con.
101 For $x\in[0,\frac{\pi}2)$#x∈[0,π/2)#, [(Cos x) [>] 0];
102 $\cos(\frac{pi}2)=0$#cos(π/2)=0#.
105 inline cic:/CoRN/transc/Pi/pos_cos.con.
107 inline cic:/CoRN/transc/Pi/Cos_HalfPi.con.
109 (*#* Convergence to [Pi [/] Two] is increasing; therefore, [Pi] is positive. *)
111 inline cic:/CoRN/transc/Pi/HalfPi_gt_pi_seq.con.
113 inline cic:/CoRN/transc/Pi/pos_Pi.con.
116 End Properties_of_Pi.
120 Hint Resolve Cos_HalfPi: algebra.
124 Section Pi_and_Order.
127 (*#* **Properties of Pi
129 The following are trivial ordering properties of multiples of [Pi]
130 that will be used so often that it is convenient to state as lemmas;
131 also, we define a hint database that automatically tries to apply this
132 lemmas, to make proof development easier.
134 A summary of what is being proved is simply:
136 [--]Pi [<] [--]Pi[/]Two [<] [--] Pi[/]Four [<] Zero [<] Pi[/]Four [<] Pi[/]Two [<] Pi
139 [PiSolve] will prove any of these inequalities.
142 inline cic:/CoRN/transc/Pi/pos_HalfPi.con.
144 inline cic:/CoRN/transc/Pi/pos_QuarterPi.con.
146 inline cic:/CoRN/transc/Pi/QuarterPi_less_HalfPi.con.
148 inline cic:/CoRN/transc/Pi/HalfPi_less_Pi.con.
150 inline cic:/CoRN/transc/Pi/QuarterPi_less_Pi.con.
152 inline cic:/CoRN/transc/Pi/neg_invPi.con.
154 inline cic:/CoRN/transc/Pi/neg_invHalfPi.con.
156 inline cic:/CoRN/transc/Pi/neg_invQuarterPi.con.
158 inline cic:/CoRN/transc/Pi/invHalfPi_less_invQuarterPi.con.
160 inline cic:/CoRN/transc/Pi/invPi_less_invHalfPi.con.
162 inline cic:/CoRN/transc/Pi/invPi_less_invQuarterPi.con.
164 inline cic:/CoRN/transc/Pi/invPi_less_Pi.con.
166 inline cic:/CoRN/transc/Pi/invPi_less_HalfPi.con.
168 inline cic:/CoRN/transc/Pi/invPi_less_QuarterPi.con.
170 inline cic:/CoRN/transc/Pi/invHalfPi_less_Pi.con.
172 inline cic:/CoRN/transc/Pi/invHalfPi_less_HalfPi.con.
174 inline cic:/CoRN/transc/Pi/invHalfPi_less_QuarterPi.con.
176 inline cic:/CoRN/transc/Pi/invQuarterPi_less_Pi.con.
178 inline cic:/CoRN/transc/Pi/invQuarterPi_less_HalfPi.con.
180 inline cic:/CoRN/transc/Pi/invQuarterPi_less_QuarterPi.con.
187 Hint Resolve pos_Pi pos_HalfPi pos_QuarterPi QuarterPi_less_HalfPi
188 HalfPi_less_Pi QuarterPi_less_Pi neg_invPi neg_invHalfPi neg_invQuarterPi
189 invHalfPi_less_invQuarterPi invPi_less_invHalfPi invPi_less_invQuarterPi
190 invPi_less_Pi invPi_less_HalfPi invPi_less_QuarterPi invHalfPi_less_Pi
191 invHalfPi_less_HalfPi invHalfPi_less_QuarterPi invQuarterPi_less_Pi
192 invQuarterPi_less_HalfPi invQuarterPi_less_QuarterPi: piorder.
198 Ltac PiSolve := try apply less_leEq; auto with piorder.
209 We now move back to trigonometric identities: sine, cosine and tangent of
213 inline cic:/CoRN/transc/Pi/Cos_double.con.
215 inline cic:/CoRN/transc/Pi/Sin_double.con.
217 inline cic:/CoRN/transc/Pi/Tan_double.con.
221 inline cic:/CoRN/transc/Pi/sqrt_lemma.con.
225 (*#* Value of trigonometric functions at [Pi[/]Four]. *)
227 inline cic:/CoRN/transc/Pi/Cos_QuarterPi.con.
229 inline cic:/CoRN/transc/Pi/Sin_QuarterPi.con.
232 Hint Resolve Sin_QuarterPi Cos_QuarterPi: algebra.
239 inline cic:/CoRN/transc/Pi/Tan_QuarterPi.con.
241 (*#* Shifting sine and cosine by [Pi[/]Two] and [Pi]. *)
243 inline cic:/CoRN/transc/Pi/Sin_HalfPi.con.
246 Hint Resolve Sin_HalfPi: algebra.
249 inline cic:/CoRN/transc/Pi/Sin_plus_HalfPi.con.
251 inline cic:/CoRN/transc/Pi/Sin_HalfPi_minus.con.
253 inline cic:/CoRN/transc/Pi/Cos_plus_HalfPi.con.
255 inline cic:/CoRN/transc/Pi/Cos_HalfPi_minus.con.
257 inline cic:/CoRN/transc/Pi/Sin_Pi.con.
259 inline cic:/CoRN/transc/Pi/Cos_Pi.con.
261 inline cic:/CoRN/transc/Pi/Sin_plus_Pi.con.
263 inline cic:/CoRN/transc/Pi/Cos_plus_Pi.con.
266 Hint Resolve Sin_plus_Pi Cos_plus_Pi: algebra.
269 (*#* Sine and cosine have period [Two Pi], tangent has period [Pi]. *)
271 inline cic:/CoRN/transc/Pi/Sin_periodic.con.
273 inline cic:/CoRN/transc/Pi/Cos_periodic.con.
275 inline cic:/CoRN/transc/Pi/Tan_periodic.con.
282 Hint Resolve Cos_double Sin_double Tan_double Cos_QuarterPi Sin_QuarterPi
283 Tan_QuarterPi Sin_Pi Cos_Pi Sin_HalfPi Sin_plus_HalfPi Sin_HalfPi_minus
284 Cos_plus_HalfPi Cos_HalfPi_minus Sin_plus_Pi Cos_plus_Pi Sin_periodic
285 Cos_periodic Tan_periodic: algebra.