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