forked from coq-community/corn
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathRreals.v
429 lines (387 loc) · 9.24 KB
/
Rreals.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
(* Copyright © 2008-2008
* Cezary Kaliszyk
*
* This work is free software; you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation; either version 2 of the License, or
* (at your option) any later version.
*
* This work is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License along
* with this work; if not, write to the Free Software Foundation, Inc.,
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*)
Require Import CSetoids.
Require Import CSemiGroups.
Require Import CMonoids.
Require Import CGroups.
Require Import CornTac.
Require Import CAbGroups.
Require Import CRings.
Require Import CFields.
Require Import COrdFields.
Require Import CReals.
Require Import RIneq.
Require Import Rcomplete.
Require Import Rlimit.
Require Import Rbasic_fun.
Require Import Fourier.
Lemma R_is_CSetoid: is_CSetoid R (@eq R) (fun x y : R => x <> y).
constructor.
unfold irreflexive.
intros x H.
apply H; reflexivity.
unfold Csymmetric.
intros x y H.
auto.
unfold cotransitive.
intros x y H z.
elim (total_order_T x z); intro H1.
elim H1; intro H2.
left.
apply Rlt_not_eq; assumption.
right.
rewrite <- H2.
assumption.
left.
apply Rgt_not_eq; assumption.
unfold tight_apart.
intros x y.
constructor.
intro xy.
elim (total_order_T x y); intro H1.
elim H1; clear H1; intro H2.
elimtype False.
apply xy.
apply Rlt_not_eq; assumption.
assumption.
elimtype False.
apply xy.
apply Rgt_not_eq; assumption.
intros H H0.
apply H0; assumption.
Qed.
Definition RSetoid : CSetoid := Build_CSetoid R (@eq R) (fun x y => x <> y) R_is_CSetoid.
Canonical Structure RSetoid.
Lemma RPlus_is_setoid_bin_fun: bin_fun_strext RSetoid RSetoid RSetoid Rplus.
unfold bin_fun_strext.
intros x1 x2 y1 y2 H.
elim (total_order_T x1 x2); intro H1.
elim H1; clear H1; intro H2.
left.
rapply Rlt_not_eq; assumption.
right.
intro H0.
apply H.
rewrite H2.
rewrite H0.
reflexivity.
left.
rapply Rgt_not_eq; assumption.
Qed.
Definition RPlus_sbinfun : CSetoid_bin_op RSetoid := Build_CSetoid_bin_op RSetoid Rplus RPlus_is_setoid_bin_fun.
Lemma R_is_CSemiGroup : is_CSemiGroup RSetoid RPlus_sbinfun.
unfold is_CSemiGroup.
unfold associative.
intros x y z.
apply eq_symmetric.
rapply Rplus_assoc.
Qed.
Definition RSemiGroup : CSemiGroup := Build_CSemiGroup RSetoid RPlus_sbinfun R_is_CSemiGroup.
Canonical Structure RSemiGroup.
Lemma R_is_CMonoid : is_CMonoid RSemiGroup (0%R).
constructor.
unfold is_rht_unit.
intro x.
rapply Rplus_0_r.
unfold is_lft_unit.
apply Rplus_0_l.
Qed.
Definition RMonoid : CMonoid := Build_CMonoid _ _ R_is_CMonoid.
Canonical Structure RMonoid.
Lemma RNeg_sunop : fun_strext (S1:=RSetoid) (S2:=RSetoid) Ropp.
unfold fun_strext.
intros x y H H0.
apply H.
rewrite H0.
reflexivity.
Qed.
Definition RNeg_op : CSetoid_un_op RMonoid := Build_CSetoid_un_op RSetoid Ropp RNeg_sunop.
Lemma R_is_Group : is_CGroup RMonoid RNeg_op.
unfold is_CGroup.
intro x.
unfold is_inverse.
split.
rapply Rplus_opp_r.
rapply Rplus_opp_l.
Qed.
Definition RGroup := Build_CGroup _ _ R_is_Group.
Canonical Structure RGroup.
Lemma R_is_AbGroup : is_CAbGroup RGroup.
unfold is_CAbGroup.
unfold commutes.
intros x y.
rapply Rplus_comm.
Qed.
Definition RAbGroup := Build_CAbGroup _ R_is_AbGroup.
Canonical Structure RAbGroup.
Lemma RMul_is_csbinop : bin_fun_strext RSetoid RSetoid RSetoid Rmult.
unfold bin_fun_strext.
intros x1 x2 y1 y2 H.
elim (total_order_T x1 x2); intro H1.
elim H1; clear H1; intro H2.
left.
rapply Rlt_not_eq; assumption.
right.
Focus 2.
left.
rapply Rgt_not_eq; assumption.
intro H0.
apply H.
rewrite H0.
rewrite H2.
reflexivity.
Qed.
Definition RMul_op : CSetoid_bin_op RMonoid := Build_CSetoid_bin_op RSetoid Rmult RMul_is_csbinop.
Lemma RMul_assoc : associative (S:=RAbGroup) RMul_op.
unfold associative.
intros x y z.
apply eq_symmetric.
rapply Rmult_assoc.
Qed.
Lemma R_is_Ring : is_CRing RAbGroup (1%R) RMul_op.
exists RMul_assoc.
constructor.
unfold is_rht_unit; intro x.
rapply Rmult_1_r.
unfold is_lft_unit; intro x.
rapply Rmult_1_l.
unfold commutes.
rapply Rmult_comm.
unfold distributive; intros x y z.
rapply Rmult_plus_distr_l.
rapply R1_neq_R0.
Qed.
Definition RRing := Build_CRing _ _ _ R_is_Ring.
Canonical Structure RRing.
Definition Rrecip : forall x : RRing, x [#] Zero -> RRing := fun x _ => Rinv x.
Lemma R_is_Field : is_CField RRing Rrecip.
constructor.
rapply Rinv_r.
assumption.
rapply Rinv_l.
assumption.
Qed.
Lemma R_is_Field2: forall (x y : RRing) (x_ : x[#]Zero) (y_ : y[#]Zero),
Rrecip x x_[#]Rrecip y y_ -> x[#]y.
intros x y x1 y1 H.
intro.
apply H.
clear H.
unfold Rrecip.
rewrite H0.
trivial.
Qed.
Definition RField : CField := Build_CField _ _ R_is_Field R_is_Field2.
Canonical Structure RField.
Lemma Rlt_strext : Crel_strext RField Rlt.
unfold Crel_strext.
intros x1 x2 y1 y2 H.
elim (total_order_T x2 y2); intro H1.
elim H1; clear H1; intro H2.
left; assumption.
right.
elim (total_order_T x1 x2); intro H1.
elim H1; clear H1; intro H3.
left.
rapply Rlt_not_eq; assumption.
right.
rewrite <- H2.
rewrite <- H3.
rapply Rgt_not_eq; assumption.
left.
rapply Rgt_not_eq; assumption.
right.
elim (total_order_T x1 x2); intro H2.
elim H2; clear H2; intro H3.
left; rapply Rlt_not_eq; assumption.
right.
rapply Rgt_not_eq.
apply Rgt_trans with x1.
assumption.
rewrite H3; assumption.
left; rapply Rgt_not_eq; assumption.
Qed.
Definition Rless_rel : CCSetoid_relation RField := Build_CCSetoid_relation RField Rlt Rlt_strext.
Lemma Rgt_strext : Crel_strext RField Rgt.
intros x1 x2 y1 y2.
pose (G := Rlt_strext y1 y2 x1 x2).
tauto.
Qed.
Definition Rgt_rel : CCSetoid_relation RField := Build_CCSetoid_relation RField Rgt Rgt_strext.
Lemma R_is_OrdField : is_COrdField RField Rless_rel Rle Rgt_rel Rge.
constructor.
constructor.
unfold Ctransitive.
apply Rlt_trans.
unfold CSetoids.antisymmetric.
apply Rlt_asym.
intros x y xy z.
rapply Rplus_lt_compat_r.
assumption.
intros x y x0 y0.
rapply Rmult_gt_0_compat; assumption.
intros x y.
constructor.
intro xy.
elim (total_order_T x y); intro H2.
elim H2; clear H2; intro H3.
left; assumption.
elimtype False; apply xy; assumption.
right; assumption.
intro H; destruct H.
rapply Rlt_not_eq; assumption.
rapply Rgt_not_eq; assumption.
intros x y.
simpl in *.
unfold Not; split.
intros; fourier.
intro.
apply Rnot_lt_le.
assumption.
auto with *.
auto with *.
Qed.
Definition ROrdField : COrdField := Build_COrdField _ _ _ _ _ R_is_OrdField.
Canonical Structure ROrdField.
Lemma cauchy_prop_cauchy_crit : (CauchySeq ROrdField) ->
forall s : (nat -> ROrdField), (Cauchy_prop (R:=ROrdField) s) -> (Rseries.Cauchy_crit s).
intros x seq cprop.
unfold Cauchy_prop in cprop.
unfold Rseries.Cauchy_crit.
intros eps epsgt.
elim (cprop ((eps / 2 / 2)%R) (eps2_Rgt_R0 _ (eps2_Rgt_R0 _ epsgt))).
intros N NProp.
exists N.
intros n m ngt mgt.
assert (AbsSmall (eps / 2) ((seq n) - (seq m)) )%R.
stepr ((seq n - seq N) + (seq N - seq m))%R by (simpl; ring).
stepl (eps / 2 / 2 + eps / 2 / 2)%R by (simpl; field).
rapply AbsSmall_plus.
rapply NProp; assumption.
rapply (AbsSmall_minus).
rapply NProp; assumption.
destruct H.
unfold Rfunctions.R_dist.
apply Rabs_def1.
clear - H0 epsgt.
simpl in *.
fourier.
clear - H epsgt.
simpl in *.
fourier.
Qed.
Definition RLim : CauchySeq ROrdField -> ROrdField.
intro x.
elim x.
intros seq cprop.
cut (Rseries.Cauchy_crit seq).
intro crit.
elim (R_complete seq crit).
intros lim uncv.
exact lim.
rapply (cauchy_prop_cauchy_crit x).
exact cprop.
Defined.
Lemma R_INR_as_IR : forall n : nat, INR n = nring (R:=RRing) n.
induction n.
simpl; trivial.
induction n.
simpl; auto with *.
simpl in *.
rewrite IHn.
trivial.
Qed.
Hint Rewrite R_INR_as_IR : RtoIR.
Require Import ConstructiveEpsilon.
Require Import Rlogic.
Lemma RisReals : is_CReals ROrdField RLim.
constructor.
intros [s hs].
unfold SeqLimit.
unfold RLim.
intros e e0.
simpl.
destruct (R_complete s ((cauchy_prop_cauchy_crit (Build_CauchySeq ROrdField s hs) s hs))).
unfold Rseries.Un_cv in u.
simpl in *.
cut (@sig nat
(fun N : nat =>
forall m : nat, le N m -> @AbsSmall ROrdField e (@cg_minus RGroup (s m) x))).
intros [N HN].
exists N.
assumption.
apply constructive_indefinite_description_nat.
intros x0.
apply forall_dec.
intro n.
destruct (le_gt_dec x0 n).
unfold AbsSmall.
simpl.
destruct (Rle_dec (- e) (s n[-]x)).
destruct (Rle_dec (s n[-]x) e).
left; intro.
split; assumption.
right; intro.
destruct (H l).
apply n0.
apply H1.
right; intro.
destruct (H l).
apply n0.
apply H0.
left.
intro.
elimtype False.
omega.
destruct (u e e0).
exists x0.
intros m Hm.
unfold AbsSmall.
assert (x0H := Rabs_def2 _ _ (H m Hm)).
unfold Rfunctions.R_dist in x0H.
clear - x0H e0.
destruct x0H.
simpl; split.
apply Rlt_le; assumption.
apply Rlt_le; assumption.
intro x.
exists (Zabs_nat (up x)).
unfold Zabs_nat.
elim (archimed x).
destruct (up x); simpl.
intros; fourier.
unfold nat_of_P.
intros H _.
apply Rlt_le.
rewrite <- R_INR_as_IR.
auto.
intros I _.
cut (x < 0%R).
intro H; clear I.
rewrite <- R_INR_as_IR.
cut (0 <= INR (nat_of_P p)).
intro.
fourier.
apply pos_INR.
cut (0 <= INR (nat_of_P p)).
intro.
fourier.
apply pos_INR.
Qed.
Definition RReals : CReals := Build_CReals ROrdField RLim RisReals.
Canonical Structure RReals.