helm/software/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 (*#* ***Constants
  78 *)
  79
  80 inline "cic:/CoRN/model/structures/Qsec/QTWO.con".
  81
  82 inline "cic:/CoRN/model/structures/Qsec/QFOUR.con".
  83
  84 (*#* ***Equality
  85 Here we prove that [QONE] is #<i>#%\emph{%not equal%}%#</i># to [QZERO]:
  86 *)
  87
  88 inline "cic:/CoRN/model/structures/Qsec/ONEQ_neq_ZEROQ.con".
  89
  90 inline "cic:/CoRN/model/structures/Qsec/refl_Qeq.con".
  91
  92 inline "cic:/CoRN/model/structures/Qsec/sym_Qeq.con".
  93
  94 inline "cic:/CoRN/model/structures/Qsec/trans_Qeq.con".
  95
  96 (*#*
  97  The equality is decidable:
  98 *)
  99
 100 inline "cic:/CoRN/model/structures/Qsec/dec_Qeq.con".
 101
 102 (*#* ***Apartness
 103 *)
 104
 105 inline "cic:/CoRN/model/structures/Qsec/Q_non_zero.con".
 106
 107 inline "cic:/CoRN/model/structures/Qsec/ap_Q_irreflexive0.con".
 108
 109 inline "cic:/CoRN/model/structures/Qsec/ap_Q_symmetric0.con".
 110
 111 inline "cic:/CoRN/model/structures/Qsec/ap_Q_cotransitive0.con".
 112
 113 inline "cic:/CoRN/model/structures/Qsec/ap_Q_tight0.con".
 114
 115 (*#* ***Addition
 116 *)
 117
 118 inline "cic:/CoRN/model/structures/Qsec/Qplus_simpl.con".
 119
 120 (*#*
 121  Addition is associative:
 122 *)
 123
 124 inline "cic:/CoRN/model/structures/Qsec/Qplus_assoc.con".
 125
 126 (*#*
 127  [QZERO] as the neutral element for addition:
 128 *)
 129
 130 inline "cic:/CoRN/model/structures/Qsec/QZERO_right.con".
 131
 132 (*#*
 133  Commutativity of addition:
 134 *)
 135
 136 inline "cic:/CoRN/model/structures/Qsec/Qplus_sym.con".
 137
 138 inline "cic:/CoRN/model/structures/Qsec/Qplus_strext0.con".
 139
 140 inline "cic:/CoRN/model/structures/Qsec/ZEROQ_as_rht_unit0.con".
 141
 142 inline "cic:/CoRN/model/structures/Qsec/ZEROQ_as_lft_unit0.con".
 143
 144 inline "cic:/CoRN/model/structures/Qsec/Qplus_is_commut0.con".
 145
 146 (*#* ***Opposite
 147  [{-Q}] is a well defined unary operation:
 148 *)
 149
 150 inline "cic:/CoRN/model/structures/Qsec/Qopp_simpl.con".
 151
 152 (*#*
 153  The group equation for [{-Q}]
 154 *)
 155
 156 inline "cic:/CoRN/model/structures/Qsec/Qplus_inverse_r.con".
 157
 158 (*#* ***Multiplication
 159 Next we shall prove the properties of multiplication. First we prove
 160 that [{*Q}] is well-defined
 161 *)
 162
 163 inline "cic:/CoRN/model/structures/Qsec/Qmult_simpl.con".
 164
 165 (*#*
 166  and it is associative:
 167 *)
 168
 169 inline "cic:/CoRN/model/structures/Qsec/Qmult_assoc.con".
 170
 171 (*#*
 172  [QONE] is the neutral element for multiplication:
 173 *)
 174
 175 inline "cic:/CoRN/model/structures/Qsec/Qmult_n_1.con".
 176
 177 (*#*
 178  The commutativity for [{*Q}]:
 179 *)
 180
 181 inline "cic:/CoRN/model/structures/Qsec/Qmult_sym.con".
 182
 183 inline "cic:/CoRN/model/structures/Qsec/Qmult_plus_distr_r.con".
 184
 185 (*#*
 186  And a property of multiplication which says if [x [~=] Zero] and [xy [=] Zero] then [y [=] Zero]:
 187 *)
 188
 189 inline "cic:/CoRN/model/structures/Qsec/Qmult_eq.con".
 190
 191 inline "cic:/CoRN/model/structures/Qsec/Qmult_strext0.con".
 192
 193 inline "cic:/CoRN/model/structures/Qsec/nonZero.con".
 194
 195 (*#* ***Inverse
 196 *)
 197
 198 inline "cic:/CoRN/model/structures/Qsec/Qinv_strext.con".
 199
 200 inline "cic:/CoRN/model/structures/Qsec/Qinv_is_inv.con".
 201
 202 (*#* ***Less-than
 203 *)
 204
 205 inline "cic:/CoRN/model/structures/Qsec/Qlt_wd_right.con".
 206
 207 inline "cic:/CoRN/model/structures/Qsec/Qlt_wd_left.con".
 208
 209 inline "cic:/CoRN/model/structures/Qsec/Qlt_eq_gt_dec.con".
 210
 211 inline "cic:/CoRN/model/structures/Qsec/Qlt_is_transitive_unfolded.con".
 212
 213 inline "cic:/CoRN/model/structures/Qsec/Qlt_strext_unfolded.con".
 214
 215 inline "cic:/CoRN/model/structures/Qsec/Qlt_is_irreflexive_unfolded.con".
 216
 217 inline "cic:/CoRN/model/structures/Qsec/Qlt_is_antisymmetric_unfolded.con".
 218
 219 inline "cic:/CoRN/model/structures/Qsec/Qplus_resp_Qlt.con".
 220
 221 inline "cic:/CoRN/model/structures/Qsec/Qmult_resp_pos_Qlt.con".
 222
 223 inline "cic:/CoRN/model/structures/Qsec/Qlt_gives_apartness.con".
 224
 225 (*#* ***Miscellaneous
 226 We consider the injection [inject_Z] from [Z] to [Q] as a coercion.
 227 *)
 228
 229 inline "cic:/CoRN/model/structures/Qsec/inject_Z.con".
 230
 231 coercion "cic:/matita/CoRN-Decl/model/structures/Qsec/inject_Z.con" 0 (* compounds *).
 232
 233 inline "cic:/CoRN/model/structures/Qsec/injz_plus.con".
 234
 235 inline "cic:/CoRN/model/structures/Qsec/injZ_One.con".
 236
 237 (*#* We can always find a natural number that is bigger than a given rational
 238 number.
 239 *)
 240
 241 inline "cic:/CoRN/model/structures/Qsec/Q_is_archemaedian0.con".
 242