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