helm/software/matita/contribs/procedural/CoRN/transc/SinCos.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 (* $Id: SinCos.v,v 1.6 2004/04/23 10:01:08 lcf Exp $ *)
  20
  21 include "transc/Trigonometric.ma".
  22
  23 (* UNEXPORTED
  24 Section Sum_and_so_on
  25 *)
  26
  27 (* UNEXPORTED
  28 Opaque Sine Cosine.
  29 *)
  30
  31 (* begin hide *)
  32
  33 inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/F.con" "Sum_and_so_on__" as definition.
  34
  35 inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/G.con" "Sum_and_so_on__" as definition.
  36
  37 inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/F'.con" "Sum_and_so_on__" as definition.
  38
  39 inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/G'.con" "Sum_and_so_on__" as definition.
  40
  41 (* end hide *)
  42
  43 inline procedural "cic:/CoRN/transc/SinCos/Sin_plus.con" as lemma.
  44
  45 inline procedural "cic:/CoRN/transc/SinCos/Cos_plus.con" as lemma.
  46
  47 (* UNEXPORTED
  48 Opaque Sine Cosine.
  49 *)
  50
  51 (* UNEXPORTED
  52 Hint Resolve Cos_plus Sin_plus: algebra.
  53 *)
  54
  55 (*#* As a corollary we get the rule for the tangent of the sum. *)
  56
  57 inline procedural "cic:/CoRN/transc/SinCos/Tan_plus.con" as lemma.
  58
  59 (* UNEXPORTED
  60 Transparent Sine Cosine.
  61 *)
  62
  63 (*#* Sine, cosine and tangent of [[--]x]. *)
  64
  65 inline procedural "cic:/CoRN/transc/SinCos/Cos_inv.con" as lemma.
  66
  67 inline procedural "cic:/CoRN/transc/SinCos/Sin_inv.con" as lemma.
  68
  69 (* UNEXPORTED
  70 Opaque Sine Cosine.
  71 *)
  72
  73 (* UNEXPORTED
  74 Hint Resolve Cos_inv Sin_inv: algebra.
  75 *)
  76
  77 inline procedural "cic:/CoRN/transc/SinCos/Tan_inv.con" as lemma.
  78
  79 (* UNEXPORTED
  80 Transparent Sine Cosine.
  81 *)
  82
  83 (*#*
  84 The fundamental formulas of trigonometry: $\cos(x)^2+\sin(x)^2=1$#cos(x)<sup>2</sup>+sin(x)<sup>2</sup>=1# and, equivalently, $1+\tan(x)^2=\frac1{\cos(x)^2}$#1+tan(x)<sup>2</sup>=1/(cos(x)<sup>2</sup>)#.
  85 *)
  86
  87 (* UNEXPORTED
  88 Hint Resolve Cos_zero: algebra.
  89 *)
  90
  91 inline procedural "cic:/CoRN/transc/SinCos/FFT.con" as theorem.
  92
  93 (* UNEXPORTED
  94 Opaque Sine Cosine.
  95 *)
  96
  97 (* UNEXPORTED
  98 Hint Resolve FFT: algebra.
  99 *)
 100
 101 inline procedural "cic:/CoRN/transc/SinCos/FFT'.con" as lemma.
 102
 103 (* UNEXPORTED
 104 End Sum_and_so_on
 105 *)
 106
 107 (* UNEXPORTED
 108 Hint Resolve Derivative_Sin Derivative_Cos: derivate.
 109 *)
 110
 111 (* UNEXPORTED
 112 Hint Resolve Continuous_Sin Continuous_Cos: continuous.
 113 *)
 114
 115 (* UNEXPORTED
 116 Hint Resolve Sin_zero Cos_zero Tan_zero Sin_plus Cos_plus Tan_plus Sin_inv
 117   Cos_inv Tan_inv FFT FFT': algebra.
 118 *)
 119
 120 (* UNEXPORTED
 121 Opaque Min Sine Cosine.
 122 *)
 123
 124 (* UNEXPORTED
 125 Section Basic_Properties
 126 *)
 127
 128 (*#* **Basic properties
 129
 130 We now prove most of the usual trigonometric (in)equalities.
 131
 132 Sine, cosine and tangent are strongly extensional and well defined.
 133 *)
 134
 135 inline procedural "cic:/CoRN/transc/SinCos/Sin_strext.con" as lemma.
 136
 137 inline procedural "cic:/CoRN/transc/SinCos/Cos_strext.con" as lemma.
 138
 139 inline procedural "cic:/CoRN/transc/SinCos/Tan_strext.con" as lemma.
 140
 141 inline procedural "cic:/CoRN/transc/SinCos/Sin_wd.con" as lemma.
 142
 143 inline procedural "cic:/CoRN/transc/SinCos/Cos_wd.con" as lemma.
 144
 145 inline procedural "cic:/CoRN/transc/SinCos/Tan_wd.con" as lemma.
 146
 147 (*#*
 148 The sine and cosine produce values in [[-1,1]].
 149 *)
 150
 151 inline procedural "cic:/CoRN/transc/SinCos/AbsIR_Sin_leEq_One.con" as lemma.
 152
 153 inline procedural "cic:/CoRN/transc/SinCos/AbsIR_Cos_leEq_One.con" as lemma.
 154
 155 inline procedural "cic:/CoRN/transc/SinCos/Sin_leEq_One.con" as lemma.
 156
 157 inline procedural "cic:/CoRN/transc/SinCos/Cos_leEq_One.con" as lemma.
 158
 159 (*#*
 160 If the cosine is positive then the sine is in [(-1,1)].
 161 *)
 162
 163 inline procedural "cic:/CoRN/transc/SinCos/Sin_less_One.con" as lemma.
 164
 165 inline procedural "cic:/CoRN/transc/SinCos/AbsIR_Sin_less_One.con" as lemma.
 166
 167 (* UNEXPORTED
 168 End Basic_Properties
 169 *)
 170
 171 (* UNEXPORTED
 172 Hint Resolve Sin_wd Cos_wd Tan_wd: algebra.
 173 *)
 174