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