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 (* begin hide *)
  20
  21 (* file        : bridges_gives_our.v                               *)
  22
  23 (* version     : 1.50 - 09/05/2001                                 *)
  24
  25 (* version     : 1.00 - 09/03/2001                                 *)
  26
  27 (* author      : Milad Niqui                                       *)
  28
  29 (* language    : coq7.0bet26feb                                    *)
  30
  31 (* dependency  : least_upper_bound_principle                       *)
  32
  33 (* description : Bridges' proof of Cauchy completeness in TCS-219  *)
  34
  35 (* INCLUDE
  36 Bridges_LUB
  37 *)
  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 inline cic:/CoRN/reals/Bridges_iso/OF.var.
  48
  49 inline cic:/CoRN/reals/Bridges_iso/lubp.var.
  50
  51 inline cic:/CoRN/reals/Bridges_iso/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 inline cic:/CoRN/reals/Bridges_iso/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 inline cic:/CoRN/reals/Bridges_iso/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 inline cic:/CoRN/reals/Bridges_iso/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 inline cic:/CoRN/reals/Bridges_iso/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 inline cic:/CoRN/reals/Bridges_iso/g.var.
 215
 216 inline cic:/CoRN/reals/Bridges_iso/g_.con.
 217
 218 inline cic:/CoRN/reals/Bridges_iso/pg.con.
 219
 220 inline cic:/CoRN/reals/Bridges_iso/P.con.
 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 inline cic:/CoRN/reals/Bridges_iso/g.var.
 267
 268 inline cic:/CoRN/reals/Bridges_iso/g_.con.
 269
 270 inline cic:/CoRN/reals/Bridges_iso/pg.con.
 271
 272 inline cic:/CoRN/reals/Bridges_iso/sup_tail.con.
 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/L.con.
 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