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