]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/CoRN-Decl/transc/SinCos.ma
update in delayed_updating
[helm.git] / 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