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