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 *********************)
19 (* $Id: SinCos.v,v 1.6 2004/04/23 10:01:08 lcf Exp $ *)
21 include "transc/Trigonometric.ma".
33 inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/F.con" "Sum_and_so_on__".
35 inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/G.con" "Sum_and_so_on__".
37 inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/F'.con" "Sum_and_so_on__".
39 inline procedural "cic:/CoRN/transc/SinCos/Sum_and_so_on/G'.con" "Sum_and_so_on__".
43 inline procedural "cic:/CoRN/transc/SinCos/Sin_plus.con".
45 inline procedural "cic:/CoRN/transc/SinCos/Cos_plus.con".
52 Hint Resolve Cos_plus Sin_plus: algebra.
55 (*#* As a corollary we get the rule for the tangent of the sum. *)
57 inline procedural "cic:/CoRN/transc/SinCos/Tan_plus.con".
60 Transparent Sine Cosine.
63 (*#* Sine, cosine and tangent of [[--]x]. *)
65 inline procedural "cic:/CoRN/transc/SinCos/Cos_inv.con".
67 inline procedural "cic:/CoRN/transc/SinCos/Sin_inv.con".
74 Hint Resolve Cos_inv Sin_inv: algebra.
77 inline procedural "cic:/CoRN/transc/SinCos/Tan_inv.con".
80 Transparent Sine Cosine.
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>)#.
88 Hint Resolve Cos_zero: algebra.
91 inline procedural "cic:/CoRN/transc/SinCos/FFT.con".
98 Hint Resolve FFT: algebra.
101 inline procedural "cic:/CoRN/transc/SinCos/FFT'.con".
108 Hint Resolve Derivative_Sin Derivative_Cos: derivate.
112 Hint Resolve Continuous_Sin Continuous_Cos: continuous.
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.
121 Opaque Min Sine Cosine.
125 Section Basic_Properties
128 (*#* **Basic properties
130 We now prove most of the usual trigonometric (in)equalities.
132 Sine, cosine and tangent are strongly extensional and well defined.
135 inline procedural "cic:/CoRN/transc/SinCos/Sin_strext.con".
137 inline procedural "cic:/CoRN/transc/SinCos/Cos_strext.con".
139 inline procedural "cic:/CoRN/transc/SinCos/Tan_strext.con".
141 inline procedural "cic:/CoRN/transc/SinCos/Sin_wd.con".
143 inline procedural "cic:/CoRN/transc/SinCos/Cos_wd.con".
145 inline procedural "cic:/CoRN/transc/SinCos/Tan_wd.con".
148 The sine and cosine produce values in [[-1,1]].
151 inline procedural "cic:/CoRN/transc/SinCos/AbsIR_Sin_leEq_One.con".
153 inline procedural "cic:/CoRN/transc/SinCos/AbsIR_Cos_leEq_One.con".
155 inline procedural "cic:/CoRN/transc/SinCos/Sin_leEq_One.con".
157 inline procedural "cic:/CoRN/transc/SinCos/Cos_leEq_One.con".
160 If the cosine is positive then the sine is in [(-1,1)].
163 inline procedural "cic:/CoRN/transc/SinCos/Sin_less_One.con".
165 inline procedural "cic:/CoRN/transc/SinCos/AbsIR_Sin_less_One.con".
172 Hint Resolve Sin_wd Cos_wd Tan_wd: algebra.