helm/software/matita/contribs/procedural/CoRN/algebra/Cauchy_COF.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 (* $Id: Cauchy_COF.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
  20
  21 include "algebra/COrdCauchy.ma".
  22
  23 include "tactics/RingReflection.ma".
  24
  25 (*#*
  26 * The Field of Cauchy Sequences
  27
  28 In this chapter we will prove that whenever we start from an ordered
  29 field [F], we can define a new ordered field of Cauchy sequences over [F].
  30
  31 %\begin{convention}% Let [F] be an ordered field.
  32 %\end{convention}%
  33 *)
  34
  35 (* UNEXPORTED
  36 Section Structure
  37 *)
  38
  39 (* UNEXPORTED
  40 cic:/CoRN/algebra/Cauchy_COF/Structure/F.var
  41 *)
  42
  43 (*#*
  44 ** Setoid Structure
  45
  46 [R_Set] is the setoid of Cauchy sequences over [F]; given two sequences
  47 [x,y] over [F], we say that [x] is smaller than [y] if from some point
  48 onwards [(y n) [-] (x n)] is greater than some fixed, positive
  49 [e].  Apartness of two sequences means that one of them is smaller
  50 than the other, equality is the negation of the apartness.
  51 *)
  52
  53 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_Set.con" as definition.
  54
  55 (* UNEXPORTED
  56 Section CSetoid_Structure
  57 *)
  58
  59 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_lt.con" as definition.
  60
  61 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap.con" as definition.
  62
  63 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_eq.con" as definition.
  64
  65 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_lt_cotrans.con" as lemma.
  66
  67 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_cotrans.con" as lemma.
  68
  69 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_symmetric.con" as lemma.
  70
  71 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_lt_irreflexive.con" as lemma.
  72
  73 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_irreflexive.con" as lemma.
  74
  75 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_eq_tight.con" as lemma.
  76
  77 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_CSetoid.con" as definition.
  78
  79 (* UNEXPORTED
  80 End CSetoid_Structure
  81 *)
  82
  83 (* UNEXPORTED
  84 Section Group_Structure
  85 *)
  86
  87 (*#*
  88 ** Group Structure
  89 The group structure is just the expected one; the lemmas which
  90 are specifically proved are just the necessary ones to get the group axioms.
  91 *)
  92
  93 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus.con" as definition.
  94
  95 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_zero.con" as definition.
  96
  97 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus_lft_ext.con" as lemma.
  98
  99 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus_assoc.con" as lemma.
 100
 101 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_zero_lft_unit.con" as lemma.
 102
 103 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus_comm.con" as lemma.
 104
 105 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_inv.con" as definition.
 106
 107 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_inv_is_inv.con" as lemma.
 108
 109 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_inv_ext.con" as lemma.
 110
 111 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rinv.con" as definition.
 112
 113 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_CAbGroup.con" as definition.
 114
 115 (* UNEXPORTED
 116 End Group_Structure
 117 *)
 118
 119 (* UNEXPORTED
 120 Section Ring_Structure
 121 *)
 122
 123 (*#* ** Ring Structure
 124 Same comments as previously.
 125 *)
 126
 127 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult.con" as definition.
 128
 129 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_one.con" as definition.
 130
 131 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_one_ap_zero.con" as lemma.
 132
 133 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_plus.con" as lemma.
 134
 135 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_dist_minus.con" as lemma.
 136
 137 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_one_rht_unit.con" as lemma.
 138
 139 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_comm.con" as lemma.
 140
 141 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_ap_zero'.con" as lemma.
 142
 143 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_lft_ext.con" as lemma.
 144
 145 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_rht_ext.con" as lemma.
 146
 147 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_strext.con" as lemma.
 148
 149 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rmult.con" as definition.
 150
 151 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_assoc.con" as lemma.
 152
 153 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_one_lft_unit.con" as lemma.
 154
 155 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_CRing.con" as definition.
 156
 157 (* UNEXPORTED
 158 End Ring_Structure
 159 *)
 160
 161 (* UNEXPORTED
 162 Section Field_Structure
 163 *)
 164
 165 (*#* ** Field Structure
 166 For the field structure, it is technically easier to first prove
 167 that our ring is actually an integral domain.  The rest then follows
 168 quite straightforwardly.
 169 *)
 170
 171 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_integral_domain.con" as lemma.
 172
 173 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_recip.con" as definition.
 174
 175 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse.con" as lemma.
 176
 177 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_recip_strext.con" as lemma.
 178
 179 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_recip_inverse'.con" as lemma.
 180
 181 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_CField.con" as definition.
 182
 183 (* UNEXPORTED
 184 End Field_Structure
 185 *)
 186
 187 (* UNEXPORTED
 188 Section Order
 189 *)
 190
 191 (*#* ** Order Structure
 192 Finally, we extend the field structure with the ordering we
 193 defined at the beginning.
 194 *)
 195
 196 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_lt_strext.con" as lemma.
 197
 198 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt.con" as definition.
 199
 200 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt_transitive.con" as lemma.
 201
 202 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt_strict.con" as lemma.
 203
 204 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_plus_resp_lt.con" as lemma.
 205
 206 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_mult_resp_lt.con" as lemma.
 207
 208 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_COrdField.con" as definition.
 209
 210 (* UNEXPORTED
 211 End Order
 212 *)
 213
 214 (*#*
 215 ** Other Results
 216 Auxiliary characterizations of the main relations on [R_Set].
 217 *)
 218
 219 (* UNEXPORTED
 220 Section Auxiliary
 221 *)
 222
 223 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_1.con" as lemma.
 224
 225 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Rlt_alt_2.con" as lemma.
 226
 227 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_1.con" as lemma.
 228
 229 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_1.con" as lemma.
 230
 231 inline procedural "cic:/CoRN/algebra/Cauchy_COF/R_ap_alt_2.con" as lemma.
 232
 233 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_1.con" as lemma.
 234
 235 inline procedural "cic:/CoRN/algebra/Cauchy_COF/Eq_alt_2_2.con" as lemma.
 236
 237 (* UNEXPORTED
 238 End Auxiliary
 239 *)
 240
 241 (* UNEXPORTED
 242 End Structure
 243 *)
 244