matita/contribs/CoRN-Decl/transc/Pi.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/transc/Pi".
  18
  19 include "CoRN.ma".
  20
  21 include "transc/SinCos.ma".
  22
  23 (* UNEXPORTED
  24 Section Properties_of_Pi
  25 *)
  26
  27 (*#* printing Pi %\ensuremath{\pi}% #&pi;# *)
  28
  29 (*#* **Definition of Pi
  30
  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.
  32 *)
  33
  34 inline "cic:/CoRN/transc/Pi/pi_seq.con".
  35
  36 (* UNEXPORTED
  37 Opaque Cosine.
  38 *)
  39
  40 (* begin hide *)
  41
  42 (* UNEXPORTED
  43 Opaque Sine.
  44 *)
  45
  46 inline "cic:/CoRN/transc/Pi/pi_seq_lemma.con".
  47
  48 (* end hide *)
  49
  50 (*#*
  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.
  54 *)
  55
  56 inline "cic:/CoRN/transc/Pi/pi_seq_nonneg.con".
  57
  58 inline "cic:/CoRN/transc/Pi/cos_pi_seq_pos.con".
  59
  60 inline "cic:/CoRN/transc/Pi/pi_seq_incr.con".
  61
  62 (*#* Trivial---but useful---consequences. *)
  63
  64 inline "cic:/CoRN/transc/Pi/sin_pi_seq_mon.con".
  65
  66 inline "cic:/CoRN/transc/Pi/sin_pi_seq_nonneg.con".
  67
  68 inline "cic:/CoRN/transc/Pi/sin_pi_seq_gt_one.con".
  69
  70 inline "cic:/CoRN/transc/Pi/cos_pi_seq_mon.con".
  71
  72 (* begin hide *)
  73
  74 inline "cic:/CoRN/transc/Pi/pi_seq_gt_one.con".
  75
  76 (* UNEXPORTED
  77 Opaque Sine Cosine.
  78 *)
  79
  80 inline "cic:/CoRN/transc/Pi/pi_seq_bnd.con".
  81
  82 inline "cic:/CoRN/transc/Pi/pi_seq_bnd'.con".
  83
  84 inline "cic:/CoRN/transc/Pi/pi_seq_bnd''.con".
  85
  86 (* end hide *)
  87
  88 (*#* An auxiliary result. *)
  89
  90 inline "cic:/CoRN/transc/Pi/Sin_One_pos.con".
  91
  92 (*#* We can now prove that this is a Cauchy sequence.  We define [Pi] as
  93 twice its limit.
  94 *)
  95
  96 inline "cic:/CoRN/transc/Pi/pi_seq_Cauchy.con".
  97
  98 inline "cic:/CoRN/transc/Pi/Pi.con".
  99
 100 (*#*
 101 For $x\in[0,\frac{\pi}2)$#x&isin;[0,&pi;/2)#, [(Cos x) [>] 0];
 102 $\cos(\frac{pi}2)=0$#cos(&pi;/2)=0#.
 103 *)
 104
 105 inline "cic:/CoRN/transc/Pi/pos_cos.con".
 106
 107 inline "cic:/CoRN/transc/Pi/Cos_HalfPi.con".
 108
 109 (*#* Convergence to [Pi [/] Two] is increasing; therefore, [Pi] is positive. *)
 110
 111 inline "cic:/CoRN/transc/Pi/HalfPi_gt_pi_seq.con".
 112
 113 inline "cic:/CoRN/transc/Pi/pos_Pi.con".
 114
 115 (* UNEXPORTED
 116 End Properties_of_Pi
 117 *)
 118
 119 (* UNEXPORTED
 120 Hint Resolve Cos_HalfPi: algebra.
 121 *)
 122
 123 (* UNEXPORTED
 124 Section Pi_and_Order
 125 *)
 126
 127 (*#* **Properties of Pi
 128
 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.
 133
 134 A summary of what is being proved is simply:
 135 [[
 136 [--]Pi [<] [--]Pi[/]Two [<] [--] Pi[/]Four [<] Zero [<] Pi[/]Four [<] Pi[/]Two [<] Pi
 137 ]]
 138
 139 [PiSolve] will prove any of these inequalities.
 140 *)
 141
 142 inline "cic:/CoRN/transc/Pi/pos_HalfPi.con".
 143
 144 inline "cic:/CoRN/transc/Pi/pos_QuarterPi.con".
 145
 146 inline "cic:/CoRN/transc/Pi/QuarterPi_less_HalfPi.con".
 147
 148 inline "cic:/CoRN/transc/Pi/HalfPi_less_Pi.con".
 149
 150 inline "cic:/CoRN/transc/Pi/QuarterPi_less_Pi.con".
 151
 152 inline "cic:/CoRN/transc/Pi/neg_invPi.con".
 153
 154 inline "cic:/CoRN/transc/Pi/neg_invHalfPi.con".
 155
 156 inline "cic:/CoRN/transc/Pi/neg_invQuarterPi.con".
 157
 158 inline "cic:/CoRN/transc/Pi/invHalfPi_less_invQuarterPi.con".
 159
 160 inline "cic:/CoRN/transc/Pi/invPi_less_invHalfPi.con".
 161
 162 inline "cic:/CoRN/transc/Pi/invPi_less_invQuarterPi.con".
 163
 164 inline "cic:/CoRN/transc/Pi/invPi_less_Pi.con".
 165
 166 inline "cic:/CoRN/transc/Pi/invPi_less_HalfPi.con".
 167
 168 inline "cic:/CoRN/transc/Pi/invPi_less_QuarterPi.con".
 169
 170 inline "cic:/CoRN/transc/Pi/invHalfPi_less_Pi.con".
 171
 172 inline "cic:/CoRN/transc/Pi/invHalfPi_less_HalfPi.con".
 173
 174 inline "cic:/CoRN/transc/Pi/invHalfPi_less_QuarterPi.con".
 175
 176 inline "cic:/CoRN/transc/Pi/invQuarterPi_less_Pi.con".
 177
 178 inline "cic:/CoRN/transc/Pi/invQuarterPi_less_HalfPi.con".
 179
 180 inline "cic:/CoRN/transc/Pi/invQuarterPi_less_QuarterPi.con".
 181
 182 (* UNEXPORTED
 183 End Pi_and_Order
 184 *)
 185
 186 (* UNEXPORTED
 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.
 193 *)
 194
 195 (* begin hide *)
 196
 197 (* UNEXPORTED
 198 Ltac PiSolve := try apply less_leEq; auto with piorder.
 199 *)
 200
 201 (* end hide *)
 202
 203 (* UNEXPORTED
 204 Section Sin_And_Cos
 205 *)
 206
 207 (*#* **More formulas
 208
 209 We now move back to trigonometric identities: sine, cosine and tangent of
 210 the double.
 211 *)
 212
 213 inline "cic:/CoRN/transc/Pi/Cos_double.con".
 214
 215 inline "cic:/CoRN/transc/Pi/Sin_double.con".
 216
 217 inline "cic:/CoRN/transc/Pi/Tan_double.con".
 218
 219 (* begin hide *)
 220
 221 inline "cic:/CoRN/transc/Pi/sqrt_lemma.con".
 222
 223 (* end hide *)
 224
 225 (*#* Value of trigonometric functions at [Pi[/]Four]. *)
 226
 227 inline "cic:/CoRN/transc/Pi/Cos_QuarterPi.con".
 228
 229 inline "cic:/CoRN/transc/Pi/Sin_QuarterPi.con".
 230
 231 (* UNEXPORTED
 232 Hint Resolve Sin_QuarterPi Cos_QuarterPi: algebra.
 233 *)
 234
 235 (* UNEXPORTED
 236 Opaque Sine Cosine.
 237 *)
 238
 239 inline "cic:/CoRN/transc/Pi/Tan_QuarterPi.con".
 240
 241 (*#* Shifting sine and cosine by [Pi[/]Two] and [Pi]. *)
 242
 243 inline "cic:/CoRN/transc/Pi/Sin_HalfPi.con".
 244
 245 (* UNEXPORTED
 246 Hint Resolve Sin_HalfPi: algebra.
 247 *)
 248
 249 inline "cic:/CoRN/transc/Pi/Sin_plus_HalfPi.con".
 250
 251 inline "cic:/CoRN/transc/Pi/Sin_HalfPi_minus.con".
 252
 253 inline "cic:/CoRN/transc/Pi/Cos_plus_HalfPi.con".
 254
 255 inline "cic:/CoRN/transc/Pi/Cos_HalfPi_minus.con".
 256
 257 inline "cic:/CoRN/transc/Pi/Sin_Pi.con".
 258
 259 inline "cic:/CoRN/transc/Pi/Cos_Pi.con".
 260
 261 inline "cic:/CoRN/transc/Pi/Sin_plus_Pi.con".
 262
 263 inline "cic:/CoRN/transc/Pi/Cos_plus_Pi.con".
 264
 265 (* UNEXPORTED
 266 Hint Resolve Sin_plus_Pi Cos_plus_Pi: algebra.
 267 *)
 268
 269 (*#* Sine and cosine have period [Two Pi], tangent has period [Pi]. *)
 270
 271 inline "cic:/CoRN/transc/Pi/Sin_periodic.con".
 272
 273 inline "cic:/CoRN/transc/Pi/Cos_periodic.con".
 274
 275 inline "cic:/CoRN/transc/Pi/Tan_periodic.con".
 276
 277 (* UNEXPORTED
 278 End Sin_And_Cos
 279 *)
 280
 281 (* UNEXPORTED
 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.
 286 *)
 287