helm/software/matita/contribs/CoRN-Procedural/reals/Bridges_iso.mma

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