1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Qsec".
21 (* $Id: Qsec.v,v 1.7 2004/04/08 08:20:35 lcf Exp $ *)
23 (*#* printing Q %\ensuremath{\mathbb{Q}}% *)
25 (*#* printing QZERO %\ensuremath{0_\mathbb{Q}}% #0<sub>Q</sub># *)
27 (*#* printing QONE %\ensuremath{1_\mathbb{Q}}% #1<sub>Q</sub># *)
29 (*#* printing QTWO %\ensuremath{2_\mathbb{Q}}% #2<sub>Q</sub># *)
31 (*#* printing QFOUR %\ensuremath{4_\mathbb{Q}}% #4<sub>Q</sub># *)
33 include "algebra/CLogic.ma".
35 include "model/structures/Zsec.ma".
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$#⟨a,n⟩# with [a:Z] and
42 [n:positive]. Intuitively, $\langle a,n\rangle$#⟨a,n⟩#
43 represents the rational number [a[/]n]. Then there is the equality on
44 [Q]: $\langle a,m\rangle=\langle
45 b,n\rangle$#⟨a,m⟩=⟨b,n⟩# iff [an [=] bm]. We
46 also define apartness, order, addition, multiplication, opposite,
47 inverse an de constants 0 and 1. *)
53 inline "cic:/CoRN/model/structures/Qsec/Q.ind".
55 inline "cic:/CoRN/model/structures/Qsec/Qeq.con".
57 inline "cic:/CoRN/model/structures/Qsec/Qap.con".
59 inline "cic:/CoRN/model/structures/Qsec/Qlt.con".
61 inline "cic:/CoRN/model/structures/Qsec/Qplus.con".
63 inline "cic:/CoRN/model/structures/Qsec/Qmult.con".
65 inline "cic:/CoRN/model/structures/Qsec/Qopp.con".
67 inline "cic:/CoRN/model/structures/Qsec/QZERO.con".
69 inline "cic:/CoRN/model/structures/Qsec/QONE.con".
71 inline "cic:/CoRN/model/structures/Qsec/Qinv.con".
78 Infix "{=Q}" := Qeq (no associativity, at level 90).
82 Infix "{#Q}" := Qap (no associativity, at level 90).
86 Infix "{<Q}" := Qlt (no associativity, at level 90).
90 Infix "{+Q}" := Qplus (no associativity, at level 85).
94 Infix "{*Q}" := Qmult (no associativity, at level 80).
98 Notation "{-Q}" := Qopp (at level 1, left associativity).
104 inline "cic:/CoRN/model/structures/Qsec/QTWO.con".
106 inline "cic:/CoRN/model/structures/Qsec/QFOUR.con".
109 Here we prove that [QONE] is #<i>#%\emph{%not equal%}%#</i># to [QZERO]:
112 inline "cic:/CoRN/model/structures/Qsec/ONEQ_neq_ZEROQ.con".
114 inline "cic:/CoRN/model/structures/Qsec/refl_Qeq.con".
116 inline "cic:/CoRN/model/structures/Qsec/sym_Qeq.con".
118 inline "cic:/CoRN/model/structures/Qsec/trans_Qeq.con".
121 The equality is decidable:
124 inline "cic:/CoRN/model/structures/Qsec/dec_Qeq.con".
129 inline "cic:/CoRN/model/structures/Qsec/Q_non_zero.con".
131 inline "cic:/CoRN/model/structures/Qsec/ap_Q_irreflexive0.con".
133 inline "cic:/CoRN/model/structures/Qsec/ap_Q_symmetric0.con".
135 inline "cic:/CoRN/model/structures/Qsec/ap_Q_cotransitive0.con".
137 inline "cic:/CoRN/model/structures/Qsec/ap_Q_tight0.con".
142 inline "cic:/CoRN/model/structures/Qsec/Qplus_simpl.con".
145 Addition is associative:
148 inline "cic:/CoRN/model/structures/Qsec/Qplus_assoc.con".
151 [QZERO] as the neutral element for addition:
154 inline "cic:/CoRN/model/structures/Qsec/QZERO_right.con".
157 Commutativity of addition:
160 inline "cic:/CoRN/model/structures/Qsec/Qplus_sym.con".
162 inline "cic:/CoRN/model/structures/Qsec/Qplus_strext0.con".
164 inline "cic:/CoRN/model/structures/Qsec/ZEROQ_as_rht_unit0.con".
166 inline "cic:/CoRN/model/structures/Qsec/ZEROQ_as_lft_unit0.con".
168 inline "cic:/CoRN/model/structures/Qsec/Qplus_is_commut0.con".
171 [{-Q}] is a well defined unary operation:
174 inline "cic:/CoRN/model/structures/Qsec/Qopp_simpl.con".
177 The group equation for [{-Q}]
180 inline "cic:/CoRN/model/structures/Qsec/Qplus_inverse_r.con".
182 (*#* ***Multiplication
183 Next we shall prove the properties of multiplication. First we prove
184 that [{*Q}] is well-defined
187 inline "cic:/CoRN/model/structures/Qsec/Qmult_simpl.con".
190 and it is associative:
193 inline "cic:/CoRN/model/structures/Qsec/Qmult_assoc.con".
196 [QONE] is the neutral element for multiplication:
199 inline "cic:/CoRN/model/structures/Qsec/Qmult_n_1.con".
202 The commutativity for [{*Q}]:
205 inline "cic:/CoRN/model/structures/Qsec/Qmult_sym.con".
207 inline "cic:/CoRN/model/structures/Qsec/Qmult_plus_distr_r.con".
210 And a property of multiplication which says if [x [~=] Zero] and [xy [=] Zero] then [y [=] Zero]:
213 inline "cic:/CoRN/model/structures/Qsec/Qmult_eq.con".
215 inline "cic:/CoRN/model/structures/Qsec/Qmult_strext0.con".
217 inline "cic:/CoRN/model/structures/Qsec/nonZero.con".
222 inline "cic:/CoRN/model/structures/Qsec/Qinv_strext.con".
224 inline "cic:/CoRN/model/structures/Qsec/Qinv_is_inv.con".
229 inline "cic:/CoRN/model/structures/Qsec/Qlt_wd_right.con".
231 inline "cic:/CoRN/model/structures/Qsec/Qlt_wd_left.con".
233 inline "cic:/CoRN/model/structures/Qsec/Qlt_eq_gt_dec.con".
235 inline "cic:/CoRN/model/structures/Qsec/Qlt_is_transitive_unfolded.con".
237 inline "cic:/CoRN/model/structures/Qsec/Qlt_strext_unfolded.con".
239 inline "cic:/CoRN/model/structures/Qsec/Qlt_is_irreflexive_unfolded.con".
241 inline "cic:/CoRN/model/structures/Qsec/Qlt_is_antisymmetric_unfolded.con".
243 inline "cic:/CoRN/model/structures/Qsec/Qplus_resp_Qlt.con".
245 inline "cic:/CoRN/model/structures/Qsec/Qmult_resp_pos_Qlt.con".
247 inline "cic:/CoRN/model/structures/Qsec/Qlt_gives_apartness.con".
249 (*#* ***Miscellaneous
250 We consider the injection [inject_Z] from [Z] to [Q] as a coercion.
253 inline "cic:/CoRN/model/structures/Qsec/inject_Z.con".
255 coercion cic:/matita/CoRN-Decl/model/structures/Qsec/inject_Z.con 0 (* compounds *).
257 inline "cic:/CoRN/model/structures/Qsec/injz_plus.con".
259 inline "cic:/CoRN/model/structures/Qsec/injZ_One.con".
261 (*#* We can always find a natural number that is bigger than a given rational
265 inline "cic:/CoRN/model/structures/Qsec/Q_is_archemaedian0.con".