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 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Rtrigo.v,v 1.40.2.1 2004/07/16 19:31:14 herbelin Exp $ i*)
35 include "Reals/Rbase.ma".
37 include "Reals/Rfunctions.ma".
39 include "Reals/SeqSeries.ma".
41 include "Reals/Rtrigo_fun.ma".
43 include "Reals/Rtrigo_def.ma".
45 include "Reals/Rtrigo_alt.ma".
47 include "Reals/Cos_rel.ma".
49 include "Reals/Cos_plus.ma".
51 include "ZArith/ZArith_base.ma".
53 include "ZArith/Zcomplements.ma".
55 include "Logic/Classical_Prop.ma".
58 Open Local Scope nat_scope.
62 Open Local Scope R_scope.
65 (*#* sin_PI2 is the only remaining axiom **)
67 inline procedural "cic:/Coq/Reals/Rtrigo/sin_PI2.con".
71 inline procedural "cic:/Coq/Reals/Rtrigo/PI_neq0.con" as lemma.
75 inline procedural "cic:/Coq/Reals/Rtrigo/cos_minus.con" as lemma.
79 inline procedural "cic:/Coq/Reals/Rtrigo/sin2_cos2.con" as lemma.
81 inline procedural "cic:/Coq/Reals/Rtrigo/cos2.con" as lemma.
85 inline procedural "cic:/Coq/Reals/Rtrigo/cos_PI2.con" as lemma.
89 inline procedural "cic:/Coq/Reals/Rtrigo/cos_PI.con" as lemma.
91 inline procedural "cic:/Coq/Reals/Rtrigo/sin_PI.con" as lemma.
95 inline procedural "cic:/Coq/Reals/Rtrigo/neg_cos.con" as lemma.
99 inline procedural "cic:/Coq/Reals/Rtrigo/sin_cos.con" as lemma.
103 inline procedural "cic:/Coq/Reals/Rtrigo/sin_plus.con" as lemma.
105 inline procedural "cic:/Coq/Reals/Rtrigo/sin_minus.con" as lemma.
109 inline procedural "cic:/Coq/Reals/Rtrigo/tan.con" as definition.
111 inline procedural "cic:/Coq/Reals/Rtrigo/tan_plus.con" as lemma.
113 (*#******************************************************)
115 (* Some properties of cos, sin and tan *)
117 (*#******************************************************)
119 inline procedural "cic:/Coq/Reals/Rtrigo/sin2.con" as lemma.
121 inline procedural "cic:/Coq/Reals/Rtrigo/sin_2a.con" as lemma.
123 inline procedural "cic:/Coq/Reals/Rtrigo/cos_2a.con" as lemma.
125 inline procedural "cic:/Coq/Reals/Rtrigo/cos_2a_cos.con" as lemma.
127 inline procedural "cic:/Coq/Reals/Rtrigo/cos_2a_sin.con" as lemma.
129 inline procedural "cic:/Coq/Reals/Rtrigo/tan_2a.con" as lemma.
131 inline procedural "cic:/Coq/Reals/Rtrigo/sin_neg.con" as lemma.
133 inline procedural "cic:/Coq/Reals/Rtrigo/cos_neg.con" as lemma.
135 inline procedural "cic:/Coq/Reals/Rtrigo/tan_0.con" as lemma.
137 inline procedural "cic:/Coq/Reals/Rtrigo/tan_neg.con" as lemma.
139 inline procedural "cic:/Coq/Reals/Rtrigo/tan_minus.con" as lemma.
141 inline procedural "cic:/Coq/Reals/Rtrigo/cos_3PI2.con" as lemma.
143 inline procedural "cic:/Coq/Reals/Rtrigo/sin_2PI.con" as lemma.
145 inline procedural "cic:/Coq/Reals/Rtrigo/cos_2PI.con" as lemma.
147 inline procedural "cic:/Coq/Reals/Rtrigo/neg_sin.con" as lemma.
149 inline procedural "cic:/Coq/Reals/Rtrigo/sin_PI_x.con" as lemma.
151 inline procedural "cic:/Coq/Reals/Rtrigo/sin_period.con" as lemma.
153 inline procedural "cic:/Coq/Reals/Rtrigo/cos_period.con" as lemma.
155 inline procedural "cic:/Coq/Reals/Rtrigo/sin_shift.con" as lemma.
157 inline procedural "cic:/Coq/Reals/Rtrigo/cos_shift.con" as lemma.
159 inline procedural "cic:/Coq/Reals/Rtrigo/cos_sin.con" as lemma.
161 inline procedural "cic:/Coq/Reals/Rtrigo/PI2_RGT_0.con" as lemma.
163 inline procedural "cic:/Coq/Reals/Rtrigo/SIN_bound.con" as lemma.
165 inline procedural "cic:/Coq/Reals/Rtrigo/COS_bound.con" as lemma.
167 inline procedural "cic:/Coq/Reals/Rtrigo/cos_sin_0.con" as lemma.
169 inline procedural "cic:/Coq/Reals/Rtrigo/cos_sin_0_var.con" as lemma.
171 (*#****************************************************************)
173 (* Using series definitions of cos and sin *)
175 (*#****************************************************************)
177 inline procedural "cic:/Coq/Reals/Rtrigo/sin_lb.con" as definition.
179 inline procedural "cic:/Coq/Reals/Rtrigo/sin_ub.con" as definition.
181 inline procedural "cic:/Coq/Reals/Rtrigo/cos_lb.con" as definition.
183 inline procedural "cic:/Coq/Reals/Rtrigo/cos_ub.con" as definition.
185 inline procedural "cic:/Coq/Reals/Rtrigo/sin_lb_gt_0.con" as lemma.
187 inline procedural "cic:/Coq/Reals/Rtrigo/SIN.con" as lemma.
189 inline procedural "cic:/Coq/Reals/Rtrigo/COS.con" as lemma.
193 inline procedural "cic:/Coq/Reals/Rtrigo/_PI2_RLT_0.con" as lemma.
195 inline procedural "cic:/Coq/Reals/Rtrigo/PI4_RLT_PI2.con" as lemma.
197 inline procedural "cic:/Coq/Reals/Rtrigo/PI2_Rlt_PI.con" as lemma.
199 (*#*******************************************)
201 (* Increasing and decreasing of COS and SIN *)
203 (*#*******************************************)
205 inline procedural "cic:/Coq/Reals/Rtrigo/sin_gt_0.con" as theorem.
207 inline procedural "cic:/Coq/Reals/Rtrigo/cos_gt_0.con" as theorem.
209 inline procedural "cic:/Coq/Reals/Rtrigo/sin_ge_0.con" as lemma.
211 inline procedural "cic:/Coq/Reals/Rtrigo/cos_ge_0.con" as lemma.
213 inline procedural "cic:/Coq/Reals/Rtrigo/sin_le_0.con" as lemma.
215 inline procedural "cic:/Coq/Reals/Rtrigo/cos_le_0.con" as lemma.
217 inline procedural "cic:/Coq/Reals/Rtrigo/sin_lt_0.con" as lemma.
219 inline procedural "cic:/Coq/Reals/Rtrigo/sin_lt_0_var.con" as lemma.
221 inline procedural "cic:/Coq/Reals/Rtrigo/cos_lt_0.con" as lemma.
223 inline procedural "cic:/Coq/Reals/Rtrigo/tan_gt_0.con" as lemma.
225 inline procedural "cic:/Coq/Reals/Rtrigo/tan_lt_0.con" as lemma.
227 inline procedural "cic:/Coq/Reals/Rtrigo/cos_ge_0_3PI2.con" as lemma.
229 inline procedural "cic:/Coq/Reals/Rtrigo/form1.con" as lemma.
231 inline procedural "cic:/Coq/Reals/Rtrigo/form2.con" as lemma.
233 inline procedural "cic:/Coq/Reals/Rtrigo/form3.con" as lemma.
235 inline procedural "cic:/Coq/Reals/Rtrigo/form4.con" as lemma.
237 inline procedural "cic:/Coq/Reals/Rtrigo/sin_increasing_0.con" as lemma.
239 inline procedural "cic:/Coq/Reals/Rtrigo/sin_increasing_1.con" as lemma.
241 inline procedural "cic:/Coq/Reals/Rtrigo/sin_decreasing_0.con" as lemma.
243 inline procedural "cic:/Coq/Reals/Rtrigo/sin_decreasing_1.con" as lemma.
245 inline procedural "cic:/Coq/Reals/Rtrigo/cos_increasing_0.con" as lemma.
247 inline procedural "cic:/Coq/Reals/Rtrigo/cos_increasing_1.con" as lemma.
249 inline procedural "cic:/Coq/Reals/Rtrigo/cos_decreasing_0.con" as lemma.
251 inline procedural "cic:/Coq/Reals/Rtrigo/cos_decreasing_1.con" as lemma.
253 inline procedural "cic:/Coq/Reals/Rtrigo/tan_diff.con" as lemma.
255 inline procedural "cic:/Coq/Reals/Rtrigo/tan_increasing_0.con" as lemma.
257 inline procedural "cic:/Coq/Reals/Rtrigo/tan_increasing_1.con" as lemma.
259 inline procedural "cic:/Coq/Reals/Rtrigo/sin_incr_0.con" as lemma.
261 inline procedural "cic:/Coq/Reals/Rtrigo/sin_incr_1.con" as lemma.
263 inline procedural "cic:/Coq/Reals/Rtrigo/sin_decr_0.con" as lemma.
265 inline procedural "cic:/Coq/Reals/Rtrigo/sin_decr_1.con" as lemma.
267 inline procedural "cic:/Coq/Reals/Rtrigo/cos_incr_0.con" as lemma.
269 inline procedural "cic:/Coq/Reals/Rtrigo/cos_incr_1.con" as lemma.
271 inline procedural "cic:/Coq/Reals/Rtrigo/cos_decr_0.con" as lemma.
273 inline procedural "cic:/Coq/Reals/Rtrigo/cos_decr_1.con" as lemma.
275 inline procedural "cic:/Coq/Reals/Rtrigo/tan_incr_0.con" as lemma.
277 inline procedural "cic:/Coq/Reals/Rtrigo/tan_incr_1.con" as lemma.
281 inline procedural "cic:/Coq/Reals/Rtrigo/sin_eq_0_1.con" as lemma.
283 inline procedural "cic:/Coq/Reals/Rtrigo/sin_eq_0_0.con" as lemma.
285 inline procedural "cic:/Coq/Reals/Rtrigo/cos_eq_0_0.con" as lemma.
287 inline procedural "cic:/Coq/Reals/Rtrigo/cos_eq_0_1.con" as lemma.
289 inline procedural "cic:/Coq/Reals/Rtrigo/sin_eq_O_2PI_0.con" as lemma.
291 inline procedural "cic:/Coq/Reals/Rtrigo/sin_eq_O_2PI_1.con" as lemma.
293 inline procedural "cic:/Coq/Reals/Rtrigo/cos_eq_0_2PI_0.con" as lemma.
295 inline procedural "cic:/Coq/Reals/Rtrigo/cos_eq_0_2PI_1.con" as lemma.