helm/software/matita/contribs/procedural/CoRN/transc/Pi.mma

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