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/SinCos".
19 (* $Id: SinCos.v,v 1.6 2004/04/23 10:01:08 lcf Exp $ *)
26 Section Sum_and_so_on.
35 inline cic:/CoRN/transc/SinCos/F.con.
37 inline cic:/CoRN/transc/SinCos/G.con.
39 inline cic:/CoRN/transc/SinCos/F'.con.
41 inline cic:/CoRN/transc/SinCos/G'.con.
45 inline cic:/CoRN/transc/SinCos/Sin_plus.con.
47 inline cic:/CoRN/transc/SinCos/Cos_plus.con.
54 Hint Resolve Cos_plus Sin_plus: algebra.
57 (*#* As a corollary we get the rule for the tangent of the sum. *)
59 inline cic:/CoRN/transc/SinCos/Tan_plus.con.
62 Transparent Sine Cosine.
65 (*#* Sine, cosine and tangent of [[--]x]. *)
67 inline cic:/CoRN/transc/SinCos/Cos_inv.con.
69 inline cic:/CoRN/transc/SinCos/Sin_inv.con.
76 Hint Resolve Cos_inv Sin_inv: algebra.
79 inline cic:/CoRN/transc/SinCos/Tan_inv.con.
82 Transparent Sine Cosine.
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>)#.
90 Hint Resolve Cos_zero: algebra.
93 inline cic:/CoRN/transc/SinCos/FFT.con.
100 Hint Resolve FFT: algebra.
103 inline cic:/CoRN/transc/SinCos/FFT'.con.
110 Hint Resolve Derivative_Sin Derivative_Cos: derivate.
114 Hint Resolve Continuous_Sin Continuous_Cos: continuous.
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.
123 Opaque Min Sine Cosine.
127 Section Basic_Properties.
130 (*#* **Basic properties
132 We now prove most of the usual trigonometric (in)equalities.
134 Sine, cosine and tangent are strongly extensional and well defined.
137 inline cic:/CoRN/transc/SinCos/Sin_strext.con.
139 inline cic:/CoRN/transc/SinCos/Cos_strext.con.
141 inline cic:/CoRN/transc/SinCos/Tan_strext.con.
143 inline cic:/CoRN/transc/SinCos/Sin_wd.con.
145 inline cic:/CoRN/transc/SinCos/Cos_wd.con.
147 inline cic:/CoRN/transc/SinCos/Tan_wd.con.
150 The sine and cosine produce values in [[-1,1]].
153 inline cic:/CoRN/transc/SinCos/AbsIR_Sin_leEq_One.con.
155 inline cic:/CoRN/transc/SinCos/AbsIR_Cos_leEq_One.con.
157 inline cic:/CoRN/transc/SinCos/Sin_leEq_One.con.
159 inline cic:/CoRN/transc/SinCos/Cos_leEq_One.con.
162 If the cosine is positive then the sine is in [(-1,1)].
165 inline cic:/CoRN/transc/SinCos/Sin_less_One.con.
167 inline cic:/CoRN/transc/SinCos/AbsIR_Sin_less_One.con.
170 End Basic_Properties.
174 Hint Resolve Sin_wd Cos_wd Tan_wd: algebra.