helm/software/matita/contribs/procedural/CoRN/model/structures/Qsec.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: Qsec.v,v 1.7 2004/04/08 08:20:35 lcf Exp $ *)
  20
  21 (*#* printing Q %\ensuremath{\mathbb{Q}}% *)
  22
  23 (*#* printing QZERO %\ensuremath{0_\mathbb{Q}}% #0<sub>Q</sub># *)
  24
  25 (*#* printing QONE %\ensuremath{1_\mathbb{Q}}% #1<sub>Q</sub># *)
  26
  27 (*#* printing QTWO %\ensuremath{2_\mathbb{Q}}% #2<sub>Q</sub># *)
  28
  29 (*#* printing QFOUR %\ensuremath{4_\mathbb{Q}}% #4<sub>Q</sub># *)
  30
  31 include "algebra/CLogic.ma".
  32
  33 include "model/structures/Zsec.ma".
  34
  35 (*#* *[Q]
  36 **About [Q]
  37 We define the structure of rational numbers as follows. First of all,
  38 it consists of the set of rational numbers, defined as the set of
  39 pairs $\langle a,n\rangle$#&lang;a,n&rang;# with [a:Z] and
  40 [n:positive]. Intuitively, $\langle a,n\rangle$#&lang;a,n&rang;#
  41 represents the rational number [a[/]n]. Then there is the equality on
  42 [Q]: $\langle a,m\rangle=\langle
  43 b,n\rangle$#&lang;a,m&rang;=&lang;b,n&rang;# iff [an [=] bm]. We
  44 also define apartness, order, addition, multiplication, opposite,
  45 inverse an de constants 0 and 1.  *)
  46
  47 (* UNEXPORTED
  48 Section Q
  49 *)
  50
  51 inline procedural "cic:/CoRN/model/structures/Qsec/Q.ind".
  52
  53 inline procedural "cic:/CoRN/model/structures/Qsec/Qeq.con" as definition.
  54
  55 inline procedural "cic:/CoRN/model/structures/Qsec/Qap.con" as definition.
  56
  57 inline procedural "cic:/CoRN/model/structures/Qsec/Qlt.con" as definition.
  58
  59 inline procedural "cic:/CoRN/model/structures/Qsec/Qplus.con" as definition.
  60
  61 inline procedural "cic:/CoRN/model/structures/Qsec/Qmult.con" as definition.
  62
  63 inline procedural "cic:/CoRN/model/structures/Qsec/Qopp.con" as definition.
  64
  65 inline procedural "cic:/CoRN/model/structures/Qsec/QZERO.con" as definition.
  66
  67 inline procedural "cic:/CoRN/model/structures/Qsec/QONE.con" as definition.
  68
  69 inline procedural "cic:/CoRN/model/structures/Qsec/Qinv.con" as definition.
  70
  71 (* UNEXPORTED
  72 End Q
  73 *)
  74
  75 (* NOTATION
  76 Infix "{=Q}" := Qeq (no associativity, at level 90).
  77 *)
  78
  79 (* NOTATION
  80 Infix "{#Q}" := Qap (no associativity, at level 90).
  81 *)
  82
  83 (* NOTATION
  84 Infix "{<Q}" := Qlt (no associativity, at level 90).
  85 *)
  86
  87 (* NOTATION
  88 Infix "{+Q}" := Qplus (no associativity, at level 85).
  89 *)
  90
  91 (* NOTATION
  92 Infix "{*Q}" := Qmult (no associativity, at level 80).
  93 *)
  94
  95 (* NOTATION
  96 Notation "{-Q}" := Qopp (at level 1, left associativity).
  97 *)
  98
  99 (*#* ***Constants
 100 *)
 101
 102 inline procedural "cic:/CoRN/model/structures/Qsec/QTWO.con" as definition.
 103
 104 inline procedural "cic:/CoRN/model/structures/Qsec/QFOUR.con" as definition.
 105
 106 (*#* ***Equality
 107 Here we prove that [QONE] is #<i>#%\emph{%not equal%}%#</i># to [QZERO]:
 108 *)
 109
 110 inline procedural "cic:/CoRN/model/structures/Qsec/ONEQ_neq_ZEROQ.con" as theorem.
 111
 112 inline procedural "cic:/CoRN/model/structures/Qsec/refl_Qeq.con" as theorem.
 113
 114 inline procedural "cic:/CoRN/model/structures/Qsec/sym_Qeq.con" as theorem.
 115
 116 inline procedural "cic:/CoRN/model/structures/Qsec/trans_Qeq.con" as theorem.
 117
 118 (*#*
 119  The equality is decidable:
 120 *)
 121
 122 inline procedural "cic:/CoRN/model/structures/Qsec/dec_Qeq.con" as theorem.
 123
 124 (*#* ***Apartness
 125 *)
 126
 127 inline procedural "cic:/CoRN/model/structures/Qsec/Q_non_zero.con" as lemma.
 128
 129 inline procedural "cic:/CoRN/model/structures/Qsec/ap_Q_irreflexive0.con" as lemma.
 130
 131 inline procedural "cic:/CoRN/model/structures/Qsec/ap_Q_symmetric0.con" as lemma.
 132
 133 inline procedural "cic:/CoRN/model/structures/Qsec/ap_Q_cotransitive0.con" as lemma.
 134
 135 inline procedural "cic:/CoRN/model/structures/Qsec/ap_Q_tight0.con" as lemma.
 136
 137 (*#* ***Addition
 138 *)
 139
 140 inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_simpl.con" as theorem.
 141
 142 (*#*
 143  Addition is associative:
 144 *)
 145
 146 inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_assoc.con" as theorem.
 147
 148 (*#*
 149  [QZERO] as the neutral element for addition:
 150 *)
 151
 152 inline procedural "cic:/CoRN/model/structures/Qsec/QZERO_right.con" as theorem.
 153
 154 (*#*
 155  Commutativity of addition:
 156 *)
 157
 158 inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_sym.con" as theorem.
 159
 160 inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_strext0.con" as lemma.
 161
 162 inline procedural "cic:/CoRN/model/structures/Qsec/ZEROQ_as_rht_unit0.con" as lemma.
 163
 164 inline procedural "cic:/CoRN/model/structures/Qsec/ZEROQ_as_lft_unit0.con" as lemma.
 165
 166 inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_is_commut0.con" as lemma.
 167
 168 (*#* ***Opposite
 169  [{-Q}] is a well defined unary operation:
 170 *)
 171
 172 inline procedural "cic:/CoRN/model/structures/Qsec/Qopp_simpl.con" as lemma.
 173
 174 (*#*
 175  The group equation for [{-Q}]
 176 *)
 177
 178 inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_inverse_r.con" as theorem.
 179
 180 (*#* ***Multiplication
 181 Next we shall prove the properties of multiplication. First we prove
 182 that [{*Q}] is well-defined
 183 *)
 184
 185 inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_simpl.con" as theorem.
 186
 187 (*#*
 188  and it is associative:
 189 *)
 190
 191 inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_assoc.con" as theorem.
 192
 193 (*#*
 194  [QONE] is the neutral element for multiplication:
 195 *)
 196
 197 inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_n_1.con" as theorem.
 198
 199 (*#*
 200  The commutativity for [{*Q}]:
 201 *)
 202
 203 inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_sym.con" as theorem.
 204
 205 inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_plus_distr_r.con" as theorem.
 206
 207 (*#*
 208  And a property of multiplication which says if [x [~=] Zero] and [xy [=] Zero] then [y [=] Zero]:
 209 *)
 210
 211 inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_eq.con" as theorem.
 212
 213 inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_strext0.con" as lemma.
 214
 215 inline procedural "cic:/CoRN/model/structures/Qsec/nonZero.con" as lemma.
 216
 217 (*#* ***Inverse
 218 *)
 219
 220 inline procedural "cic:/CoRN/model/structures/Qsec/Qinv_strext.con" as lemma.
 221
 222 inline procedural "cic:/CoRN/model/structures/Qsec/Qinv_is_inv.con" as lemma.
 223
 224 (*#* ***Less-than
 225 *)
 226
 227 inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_wd_right.con" as lemma.
 228
 229 inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_wd_left.con" as lemma.
 230
 231 inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_eq_gt_dec.con" as lemma.
 232
 233 inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_is_transitive_unfolded.con" as lemma.
 234
 235 inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_strext_unfolded.con" as lemma.
 236
 237 inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_is_irreflexive_unfolded.con" as lemma.
 238
 239 inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_is_antisymmetric_unfolded.con" as lemma.
 240
 241 inline procedural "cic:/CoRN/model/structures/Qsec/Qplus_resp_Qlt.con" as lemma.
 242
 243 inline procedural "cic:/CoRN/model/structures/Qsec/Qmult_resp_pos_Qlt.con" as lemma.
 244
 245 inline procedural "cic:/CoRN/model/structures/Qsec/Qlt_gives_apartness.con" as lemma.
 246
 247 (*#* ***Miscellaneous
 248 We consider the injection [inject_Z] from [Z] to [Q] as a coercion.
 249 *)
 250
 251 inline procedural "cic:/CoRN/model/structures/Qsec/inject_Z.con" as definition.
 252
 253 (* COERCION
 254 cic:/matita/CoRN-Procedural/model/structures/Qsec/inject_Z.con
 255 *)
 256
 257 inline procedural "cic:/CoRN/model/structures/Qsec/injz_plus.con" as lemma.
 258
 259 inline procedural "cic:/CoRN/model/structures/Qsec/injZ_One.con" as lemma.
 260
 261 (*#* We can always find a natural number that is bigger than a given rational
 262 number.
 263 *)
 264
 265 inline procedural "cic:/CoRN/model/structures/Qsec/Q_is_archemaedian0.con" as theorem.
 266