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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/reals/Bridges_iso".
21 (* file : bridges_gives_our.v *)
23 (* version : 1.50 - 09/05/2001 *)
25 (* version : 1.00 - 09/03/2001 *)
27 (* author : Milad Niqui *)
29 (* language : coq7.0bet26feb *)
31 (* dependency : least_upper_bound_principle *)
33 (* description : Bridges' proof of Cauchy completeness in TCS-219 *)
39 (* This lemma comes from lemmas.v of Martijn Oostdijk *)
41 inline cic:/CoRN/reals/Bridges_iso/le_witness_informative.con.
44 Section bridges_axioms_imply_ours.
47 inline cic:/CoRN/reals/Bridges_iso/OF.var.
49 inline cic:/CoRN/reals/Bridges_iso/lubp.var.
51 inline cic:/CoRN/reals/Bridges_iso/is_Archimedes.var.
53 inline cic:/CoRN/reals/Bridges_iso/is_Archimedes'.con.
56 Section proofs_in_TCS.
59 inline cic:/CoRN/reals/Bridges_iso/leEq_geEq.con.
61 inline cic:/CoRN/reals/Bridges_iso/glbp.con.
67 inline cic:/CoRN/reals/Bridges_iso/P.var.
69 inline cic:/CoRN/reals/Bridges_iso/inequality1.con.
71 inline cic:/CoRN/reals/Bridges_iso/inequality2.con.
73 inline cic:/CoRN/reals/Bridges_iso/inequality3.con.
75 inline cic:/CoRN/reals/Bridges_iso/inequality4.con.
77 inline cic:/CoRN/reals/Bridges_iso/Hum.con.
79 inline cic:/CoRN/reals/Bridges_iso/bound_tk1.con.
81 inline cic:/CoRN/reals/Bridges_iso/bound_tk2.con.
83 inline cic:/CoRN/reals/Bridges_iso/trick.con.
85 inline cic:/CoRN/reals/Bridges_iso/trick'.con.
87 inline cic:/CoRN/reals/Bridges_iso/up_bound_for_n_element.con.
89 inline cic:/CoRN/reals/Bridges_iso/low_bound_for_n_element.con.
91 inline cic:/CoRN/reals/Bridges_iso/saghf.con.
93 inline cic:/CoRN/reals/Bridges_iso/Psaghf.con.
95 inline cic:/CoRN/reals/Bridges_iso/kaf.con.
97 inline cic:/CoRN/reals/Bridges_iso/Pkaf.con.
99 inline cic:/CoRN/reals/Bridges_iso/is_finite_P.var.
101 inline cic:/CoRN/reals/Bridges_iso/card.con.
103 inline cic:/CoRN/reals/Bridges_iso/Pcard1.con.
105 inline cic:/CoRN/reals/Bridges_iso/seq.con.
107 inline cic:/CoRN/reals/Bridges_iso/Pseq1.con.
109 inline cic:/CoRN/reals/Bridges_iso/Pseq1_unfolded.con.
111 inline cic:/CoRN/reals/Bridges_iso/indeks.con.
113 inline cic:/CoRN/reals/Bridges_iso/Pindeks.con.
115 inline cic:/CoRN/reals/Bridges_iso/is_onto_seq_P.var.
117 inline cic:/CoRN/reals/Bridges_iso/P_is_inhabited.con.
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)).
126 Cut (phi O)\/(psi O).
132 Rewrite <- (le_n_O_eq m H2).
148 Apply le_trans with m:=N.
157 Case (le_lt_eq_dec m (S N)).
161 Apply (lt_n_Sm_le m N).
181 Apply le_trans with m:=N.
188 inline cic:/CoRN/reals/Bridges_iso/bounded_quantifier_informative.con.
190 inline cic:/CoRN/reals/Bridges_iso/bridges_lemma1a.con.
192 inline cic:/CoRN/reals/Bridges_iso/P_is_strongly_extensional.var.
194 inline cic:/CoRN/reals/Bridges_iso/bridges_lemma1b.con.
200 (*#**********************************)
202 (*#**********************************)
204 (*#**********************************)
206 (*#**********************************)
209 Section Every_Cauchy_Sequence_is_bounded.
212 inline cic:/CoRN/reals/Bridges_iso/seq2set.con.
214 inline cic:/CoRN/reals/Bridges_iso/g.var.
216 inline cic:/CoRN/reals/Bridges_iso/g_.con.
218 inline cic:/CoRN/reals/Bridges_iso/pg.con.
220 inline cic:/CoRN/reals/Bridges_iso/P.con.
222 inline cic:/CoRN/reals/Bridges_iso/fin_is_fin.con.
224 inline cic:/CoRN/reals/Bridges_iso/card_fin.con.
226 inline cic:/CoRN/reals/Bridges_iso/finite_seq.con.
228 inline cic:/CoRN/reals/Bridges_iso/bridges_lemma2a.con.
230 inline cic:/CoRN/reals/Bridges_iso/sup.con.
232 inline cic:/CoRN/reals/Bridges_iso/Psup.con.
234 inline cic:/CoRN/reals/Bridges_iso/Psup_proj1.con.
236 inline cic:/CoRN/reals/Bridges_iso/Psup_unfolded1.con.
238 inline cic:/CoRN/reals/Bridges_iso/Psup_unfolded2.con.
240 inline cic:/CoRN/reals/Bridges_iso/bridges_lemma2b.con.
242 inline cic:/CoRN/reals/Bridges_iso/inf.con.
244 inline cic:/CoRN/reals/Bridges_iso/Pinf.con.
246 inline cic:/CoRN/reals/Bridges_iso/Pinf_proj1.con.
248 inline cic:/CoRN/reals/Bridges_iso/Pinf_unfolded1.con.
250 inline cic:/CoRN/reals/Bridges_iso/Pinf_unfolded2.con.
252 (* I tried very much not to mention this lemma! *)
254 inline cic:/CoRN/reals/Bridges_iso/sup_leEq.con.
256 inline cic:/CoRN/reals/Bridges_iso/inf_geEq.con.
258 inline cic:/CoRN/reals/Bridges_iso/tail_is_Cauchy.con.
260 inline cic:/CoRN/reals/Bridges_iso/tail_seq.con.
263 End Every_Cauchy_Sequence_is_bounded.
266 inline cic:/CoRN/reals/Bridges_iso/g.var.
268 inline cic:/CoRN/reals/Bridges_iso/g_.con.
270 inline cic:/CoRN/reals/Bridges_iso/pg.con.
272 inline cic:/CoRN/reals/Bridges_iso/sup_tail.con.
274 inline cic:/CoRN/reals/Bridges_iso/sup_tail_leEq.con.
276 inline cic:/CoRN/reals/Bridges_iso/sup_tail_is_Cauchy.con.
278 inline cic:/CoRN/reals/Bridges_iso/sup_tail_as_Cauchy.con.
280 inline cic:/CoRN/reals/Bridges_iso/L.con.
282 inline cic:/CoRN/reals/Bridges_iso/sup_tail_decrease.con.
284 inline cic:/CoRN/reals/Bridges_iso/L_less_sup_n.con.
286 inline cic:/CoRN/reals/Bridges_iso/Psup_unfolded2_informative.con.
288 inline cic:/CoRN/reals/Bridges_iso/Pinf_unfolded2_informative.con.
290 inline cic:/CoRN/reals/Bridges_iso/convergent_subseq.con.
292 (* very elegant proof almost as short as text version! *)
294 inline cic:/CoRN/reals/Bridges_iso/lubp_gives_Cauchy.con.
300 inline cic:/CoRN/reals/Bridges_iso/Bridges_R_is_CReals.con.
302 inline cic:/CoRN/reals/Bridges_iso/Bridges_R_as_CReals.con.
305 End bridges_axioms_imply_ours.
310 (*#* remove printing Q *)