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 *********************)
19 (* $Id: Qpossetoid.v,v 1.4 2004/04/06 15:46:05 lcf Exp $ *)
21 include "model/setoids/Qsetoid.ma".
23 include "algebra/CSetoidFun.ma".
25 include "model/structures/Qpossec.ma".
27 (*#* **Example of a setoid: [Qpos]
29 We will examine the subsetoid of positive rationals of the setoid of
33 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/Qpos.con" as definition.
35 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/QposP.con" as definition.
37 (*#* One, two and four are elements of it.
40 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/QONEpos.con" as definition.
42 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/QTWOpos.con" as definition.
44 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/QFOURpos.con" as definition.
46 (*#* ***Multiplication
47 As we have seen, multiplication preserves positivity, so we can restrict it
48 to the positive rationals. We see that this restricted multiplication has some
52 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/Qmult_pres_pos1.con" as lemma.
54 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/Qpos_mult.con" as definition.
56 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/associative_Qpos_mult.con" as lemma.
59 We restrict the domain of the inverse to the set of positive rationals.
62 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/Qpos_inv.con" as definition.
64 (*#* The restricted inverse preserves positivity.
67 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/inv_pres_pos1.con" as lemma.
69 (*#* Now, we can also restrict the co-domain.
72 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/Qpos_Qpos_inv.con" as definition.
74 (*#* This restricted inverse map appears a setoid function.
77 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/Qpos_Qpos_inv_strong_ext.con" as lemma.
79 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/Qpos_Qpos_inv_op.con" as definition.
81 (*#* ***Special multiplication and inverse
82 We define [multdiv2]: $(x,y) \mapsto xy/2$ #(x,y) ↦ xy/2#.
85 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/Qpos_div2.con" as definition.
87 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/multdiv2.con" as definition.
89 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/associative_multdiv2.con" as lemma.
91 (*#* And its inverse [multdiv4]: $x \mapsto 4/x$ #x ↦ 4/x#.
94 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/mult4.con" as definition.
96 inline procedural "cic:/CoRN/model/setoids/Qpossetoid/divmult4.con" as definition.