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".
19 (* $Id: Qsec.v,v 1.7 2004/04/08 08:20:35 lcf Exp $ *)
21 (*#* printing Q %\ensuremath{\mathbb{Q}}% *)
23 (*#* printing QZERO %\ensuremath{0_\mathbb{Q}}% #0<sub>Q</sub># *)
25 (*#* printing QONE %\ensuremath{1_\mathbb{Q}}% #1<sub>Q</sub># *)
27 (*#* printing QTWO %\ensuremath{2_\mathbb{Q}}% #2<sub>Q</sub># *)
29 (*#* printing QFOUR %\ensuremath{4_\mathbb{Q}}% #4<sub>Q</sub># *)
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$#⟨a,n⟩# with [a:Z] and
52 [n:positive]. Intuitively, $\langle a,n\rangle$#⟨a,n⟩#
53 represents the rational number [a[/]n]. Then there is the equality on
54 [Q]: $\langle a,m\rangle=\langle
55 b,n\rangle$#⟨a,m⟩=⟨b,n⟩# iff [an [=] bm]. We
56 also define apartness, order, addition, multiplication, opposite,
57 inverse an de constants 0 and 1. *)
63 inline cic:/CoRN/model/structures/Qsec/Q.ind.
65 inline cic:/CoRN/model/structures/Qsec/Qeq.con.
67 inline cic:/CoRN/model/structures/Qsec/Qap.con.
69 inline cic:/CoRN/model/structures/Qsec/Qlt.con.
71 inline cic:/CoRN/model/structures/Qsec/Qplus.con.
73 inline cic:/CoRN/model/structures/Qsec/Qmult.con.
75 inline cic:/CoRN/model/structures/Qsec/Qopp.con.
77 inline cic:/CoRN/model/structures/Qsec/QZERO.con.
79 inline cic:/CoRN/model/structures/Qsec/QONE.con.
81 inline cic:/CoRN/model/structures/Qsec/Qinv.con.
90 inline cic:/CoRN/model/structures/Qsec/QTWO.con.
92 inline cic:/CoRN/model/structures/Qsec/QFOUR.con.
95 Here we prove that [QONE] is #<i>#%\emph{%not equal%}%#</i># to [QZERO]:
98 inline cic:/CoRN/model/structures/Qsec/ONEQ_neq_ZEROQ.con.
100 inline cic:/CoRN/model/structures/Qsec/refl_Qeq.con.
102 inline cic:/CoRN/model/structures/Qsec/sym_Qeq.con.
104 inline cic:/CoRN/model/structures/Qsec/trans_Qeq.con.
107 The equality is decidable:
110 inline cic:/CoRN/model/structures/Qsec/dec_Qeq.con.
115 inline cic:/CoRN/model/structures/Qsec/Q_non_zero.con.
117 inline cic:/CoRN/model/structures/Qsec/ap_Q_irreflexive0.con.
119 inline cic:/CoRN/model/structures/Qsec/ap_Q_symmetric0.con.
121 inline cic:/CoRN/model/structures/Qsec/ap_Q_cotransitive0.con.
123 inline cic:/CoRN/model/structures/Qsec/ap_Q_tight0.con.
128 inline cic:/CoRN/model/structures/Qsec/Qplus_simpl.con.
131 Addition is associative:
134 inline cic:/CoRN/model/structures/Qsec/Qplus_assoc.con.
137 [QZERO] as the neutral element for addition:
140 inline cic:/CoRN/model/structures/Qsec/QZERO_right.con.
143 Commutativity of addition:
146 inline cic:/CoRN/model/structures/Qsec/Qplus_sym.con.
148 inline cic:/CoRN/model/structures/Qsec/Qplus_strext0.con.
150 inline cic:/CoRN/model/structures/Qsec/ZEROQ_as_rht_unit0.con.
152 inline cic:/CoRN/model/structures/Qsec/ZEROQ_as_lft_unit0.con.
154 inline cic:/CoRN/model/structures/Qsec/Qplus_is_commut0.con.
157 [{-Q}] is a well defined unary operation:
160 inline cic:/CoRN/model/structures/Qsec/Qopp_simpl.con.
163 The group equation for [{-Q}]
166 inline cic:/CoRN/model/structures/Qsec/Qplus_inverse_r.con.
168 (*#* ***Multiplication
169 Next we shall prove the properties of multiplication. First we prove
170 that [{*Q}] is well-defined
173 inline cic:/CoRN/model/structures/Qsec/Qmult_simpl.con.
176 and it is associative:
179 inline cic:/CoRN/model/structures/Qsec/Qmult_assoc.con.
182 [QONE] is the neutral element for multiplication:
185 inline cic:/CoRN/model/structures/Qsec/Qmult_n_1.con.
188 The commutativity for [{*Q}]:
191 inline cic:/CoRN/model/structures/Qsec/Qmult_sym.con.
193 inline cic:/CoRN/model/structures/Qsec/Qmult_plus_distr_r.con.
196 And a property of multiplication which says if [x [~=] Zero] and [xy [=] Zero] then [y [=] Zero]:
199 inline cic:/CoRN/model/structures/Qsec/Qmult_eq.con.
201 inline cic:/CoRN/model/structures/Qsec/Qmult_strext0.con.
203 inline cic:/CoRN/model/structures/Qsec/nonZero.con.
208 inline cic:/CoRN/model/structures/Qsec/Qinv_strext.con.
210 inline cic:/CoRN/model/structures/Qsec/Qinv_is_inv.con.
215 inline cic:/CoRN/model/structures/Qsec/Qlt_wd_right.con.
217 inline cic:/CoRN/model/structures/Qsec/Qlt_wd_left.con.
219 inline cic:/CoRN/model/structures/Qsec/Qlt_eq_gt_dec.con.
221 inline cic:/CoRN/model/structures/Qsec/Qlt_is_transitive_unfolded.con.
223 inline cic:/CoRN/model/structures/Qsec/Qlt_strext_unfolded.con.
225 inline cic:/CoRN/model/structures/Qsec/Qlt_is_irreflexive_unfolded.con.
227 inline cic:/CoRN/model/structures/Qsec/Qlt_is_antisymmetric_unfolded.con.
229 inline cic:/CoRN/model/structures/Qsec/Qplus_resp_Qlt.con.
231 inline cic:/CoRN/model/structures/Qsec/Qmult_resp_pos_Qlt.con.
233 inline cic:/CoRN/model/structures/Qsec/Qlt_gives_apartness.con.
235 (*#* ***Miscellaneous
236 We consider the injection [inject_Z] from [Z] to [Q] as a coercion.
239 inline cic:/CoRN/model/structures/Qsec/inject_Z.con.
241 inline cic:/CoRN/model/structures/Qsec/injz_plus.con.
243 inline cic:/CoRN/model/structures/Qsec/injZ_One.con.
245 (*#* We can always find a natural number that is bigger than a given rational
249 inline cic:/CoRN/model/structures/Qsec/Q_is_archemaedian0.con.