]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/CoRN-Decl/reals/Bridges_iso.ma
made executable again
[helm.git] / matita / matita / contribs / CoRN-Decl / reals / Bridges_iso.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/reals/Bridges_iso".
18
19 include "CoRN.ma".
20
21 (* begin hide *)
22
23 (* file        : bridges_gives_our.v                               *)
24
25 (* version     : 1.50 - 09/05/2001                                 *)
26
27 (* version     : 1.00 - 09/03/2001                                 *)
28
29 (* author      : Milad Niqui                                       *)
30
31 (* language    : coq7.0bet26feb                                    *)
32
33 (* dependency  : least_upper_bound_principle                       *)
34
35 (* description : Bridges' proof of Cauchy completeness in TCS-219  *)
36
37 include "reals/Bridges_LUB.ma".
38
39 (* This lemma comes from lemmas.v of Martijn Oostdijk *)
40
41 inline "cic:/CoRN/reals/Bridges_iso/le_witness_informative.con".
42
43 (* UNEXPORTED
44 Section bridges_axioms_imply_ours
45 *)
46
47 alias id "OF" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/OF.var".
48
49 alias id "lubp" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/lubp.var".
50
51 alias id "is_Archimedes" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/is_Archimedes.var".
52
53 inline "cic:/CoRN/reals/Bridges_iso/is_Archimedes'.con".
54
55 (* UNEXPORTED
56 Section proofs_in_TCS
57 *)
58
59 inline "cic:/CoRN/reals/Bridges_iso/leEq_geEq.con".
60
61 inline "cic:/CoRN/reals/Bridges_iso/glbp.con".
62
63 (* UNEXPORTED
64 Section supremum
65 *)
66
67 alias id "P" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/P.var".
68
69 inline "cic:/CoRN/reals/Bridges_iso/inequality1.con".
70
71 inline "cic:/CoRN/reals/Bridges_iso/inequality2.con".
72
73 inline "cic:/CoRN/reals/Bridges_iso/inequality3.con".
74
75 inline "cic:/CoRN/reals/Bridges_iso/inequality4.con".
76
77 inline "cic:/CoRN/reals/Bridges_iso/Hum.con".
78
79 inline "cic:/CoRN/reals/Bridges_iso/bound_tk1.con".
80
81 inline "cic:/CoRN/reals/Bridges_iso/bound_tk2.con".
82
83 inline "cic:/CoRN/reals/Bridges_iso/trick.con".
84
85 inline "cic:/CoRN/reals/Bridges_iso/trick'.con".
86
87 inline "cic:/CoRN/reals/Bridges_iso/up_bound_for_n_element.con".
88
89 inline "cic:/CoRN/reals/Bridges_iso/low_bound_for_n_element.con".
90
91 inline "cic:/CoRN/reals/Bridges_iso/saghf.con".
92
93 inline "cic:/CoRN/reals/Bridges_iso/Psaghf.con".
94
95 inline "cic:/CoRN/reals/Bridges_iso/kaf.con".
96
97 inline "cic:/CoRN/reals/Bridges_iso/Pkaf.con".
98
99 alias id "is_finite_P" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/is_finite_P.var".
100
101 inline "cic:/CoRN/reals/Bridges_iso/card.con".
102
103 inline "cic:/CoRN/reals/Bridges_iso/Pcard1.con".
104
105 inline "cic:/CoRN/reals/Bridges_iso/seq.con".
106
107 inline "cic:/CoRN/reals/Bridges_iso/Pseq1.con".
108
109 inline "cic:/CoRN/reals/Bridges_iso/Pseq1_unfolded.con".
110
111 inline "cic:/CoRN/reals/Bridges_iso/indeks.con".
112
113 inline "cic:/CoRN/reals/Bridges_iso/Pindeks.con".
114
115 alias id "is_onto_seq_P" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/is_onto_seq_P.var".
116
117 inline "cic:/CoRN/reals/Bridges_iso/P_is_inhabited.con".
118
119 (*
120 Lemma bounded_quantifier:(N:nat;phi,psi:nat->Prop)
121                  ((m:nat)(le m N)->(phi m)\/(psi m))->
122         ((m:nat)(le m N)->(phi m))\/(Ex [j:nat](le j N)/\(psi j)).
123 Proof.
124  Intros.
125  Induction N.
126  Cut (phi O)\/(psi O).
127  Intro.
128  Case H0.
129  Intros.
130  Left.
131  Intros.
132  Rewrite <- (le_n_O_eq m H2).
133  Assumption.
134  Intro.
135  Right.
136  Exists O.
137  Split.
138  Constructor.
139  Assumption.
140  Apply H.
141  Constructor.*)
142
143 (* n=(S n0) *)
144
145 (* Case HrecN.
146  Intros.
147  Apply H.
148  Apply le_trans with m:=N.
149  Assumption.
150  Apply le_n_Sn.
151  Intro.
152  Case (H (S N)).
153  Apply le_n.
154  Intros.
155  Left.
156  Intros.
157  Case (le_lt_eq_dec m (S N)).
158  Assumption.
159  Intros.
160  Apply H0.
161  Apply (lt_n_Sm_le m N).
162  Assumption.
163  Intro.
164  Rewrite e.
165  Assumption.
166  Intro.
167  Right.
168  Exists (S N).
169  Split.
170  Apply le_n.
171  Assumption.
172  Intro.
173  Right.
174  Case H0.
175  Intro j.
176  Intros.
177  Exists j.
178  Elim H1.
179  Intros.
180  Split.
181  Apply le_trans with m:=N.
182  Assumption.
183  Apply le_n_Sn.
184  Assumption.
185 Qed. 
186 *)
187
188 inline "cic:/CoRN/reals/Bridges_iso/bounded_quantifier_informative.con".
189
190 inline "cic:/CoRN/reals/Bridges_iso/bridges_lemma1a.con".
191
192 alias id "P_is_strongly_extensional" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/supremum/P_is_strongly_extensional.var".
193
194 inline "cic:/CoRN/reals/Bridges_iso/bridges_lemma1b.con".
195
196 (* UNEXPORTED
197 End supremum
198 *)
199
200 (*#**********************************)
201
202 (*#**********************************)
203
204 (*#**********************************)
205
206 (*#**********************************)
207
208 (* UNEXPORTED
209 Section Every_Cauchy_Sequence_is_bounded
210 *)
211
212 inline "cic:/CoRN/reals/Bridges_iso/seq2set.con".
213
214 alias id "g" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/Every_Cauchy_Sequence_is_bounded/g.var".
215
216 inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/Every_Cauchy_Sequence_is_bounded/g_.con" "bridges_axioms_imply_ours__proofs_in_TCS__Every_Cauchy_Sequence_is_bounded__".
217
218 inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/Every_Cauchy_Sequence_is_bounded/pg.con" "bridges_axioms_imply_ours__proofs_in_TCS__Every_Cauchy_Sequence_is_bounded__".
219
220 inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/Every_Cauchy_Sequence_is_bounded/P.con" "bridges_axioms_imply_ours__proofs_in_TCS__Every_Cauchy_Sequence_is_bounded__".
221
222 inline "cic:/CoRN/reals/Bridges_iso/fin_is_fin.con".
223
224 inline "cic:/CoRN/reals/Bridges_iso/card_fin.con".
225
226 inline "cic:/CoRN/reals/Bridges_iso/finite_seq.con".
227
228 inline "cic:/CoRN/reals/Bridges_iso/bridges_lemma2a.con".
229
230 inline "cic:/CoRN/reals/Bridges_iso/sup.con".
231
232 inline "cic:/CoRN/reals/Bridges_iso/Psup.con".
233
234 inline "cic:/CoRN/reals/Bridges_iso/Psup_proj1.con".
235
236 inline "cic:/CoRN/reals/Bridges_iso/Psup_unfolded1.con".
237
238 inline "cic:/CoRN/reals/Bridges_iso/Psup_unfolded2.con".
239
240 inline "cic:/CoRN/reals/Bridges_iso/bridges_lemma2b.con".
241
242 inline "cic:/CoRN/reals/Bridges_iso/inf.con".
243
244 inline "cic:/CoRN/reals/Bridges_iso/Pinf.con".
245
246 inline "cic:/CoRN/reals/Bridges_iso/Pinf_proj1.con".
247
248 inline "cic:/CoRN/reals/Bridges_iso/Pinf_unfolded1.con".
249
250 inline "cic:/CoRN/reals/Bridges_iso/Pinf_unfolded2.con".
251
252 (* I tried very much not to mention this lemma! *)
253
254 inline "cic:/CoRN/reals/Bridges_iso/sup_leEq.con".
255
256 inline "cic:/CoRN/reals/Bridges_iso/inf_geEq.con".
257
258 inline "cic:/CoRN/reals/Bridges_iso/tail_is_Cauchy.con".
259
260 inline "cic:/CoRN/reals/Bridges_iso/tail_seq.con".
261
262 (* UNEXPORTED
263 End Every_Cauchy_Sequence_is_bounded
264 *)
265
266 alias id "g" = "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/g.var".
267
268 inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/g_.con" "bridges_axioms_imply_ours__proofs_in_TCS__".
269
270 inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/pg.con" "bridges_axioms_imply_ours__proofs_in_TCS__".
271
272 inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/sup_tail.con" "bridges_axioms_imply_ours__proofs_in_TCS__".
273
274 inline "cic:/CoRN/reals/Bridges_iso/sup_tail_leEq.con".
275
276 inline "cic:/CoRN/reals/Bridges_iso/sup_tail_is_Cauchy.con".
277
278 inline "cic:/CoRN/reals/Bridges_iso/sup_tail_as_Cauchy.con".
279
280 inline "cic:/CoRN/reals/Bridges_iso/bridges_axioms_imply_ours/proofs_in_TCS/L.con" "bridges_axioms_imply_ours__proofs_in_TCS__".
281
282 inline "cic:/CoRN/reals/Bridges_iso/sup_tail_decrease.con".
283
284 inline "cic:/CoRN/reals/Bridges_iso/L_less_sup_n.con".
285
286 inline "cic:/CoRN/reals/Bridges_iso/Psup_unfolded2_informative.con".
287
288 inline "cic:/CoRN/reals/Bridges_iso/Pinf_unfolded2_informative.con".
289
290 inline "cic:/CoRN/reals/Bridges_iso/convergent_subseq.con".
291
292 (* very elegant proof almost as short as text version! *)
293
294 inline "cic:/CoRN/reals/Bridges_iso/lubp_gives_Cauchy.con".
295
296 (* UNEXPORTED
297 End proofs_in_TCS
298 *)
299
300 inline "cic:/CoRN/reals/Bridges_iso/Bridges_R_is_CReals.con".
301
302 inline "cic:/CoRN/reals/Bridges_iso/Bridges_R_as_CReals.con".
303
304 (* UNEXPORTED
305 End bridges_axioms_imply_ours
306 *)
307
308 (* end hide *)
309
310 (*#* remove printing Q *)
311