matita/contribs/CoRN-Decl/model/setoids/Qpossetoid.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/setoids/Qpossetoid".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: Qpossetoid.v,v 1.4 2004/04/06 15:46:05 lcf Exp $ *)
  22
  23 include "model/setoids/Qsetoid.ma".
  24
  25 include "algebra/CSetoidFun.ma".
  26
  27 include "model/structures/Qpossec.ma".
  28
  29 (*#* **Example of a setoid: [Qpos]
  30 ***Setoid
  31 We will examine the subsetoid of positive rationals of the setoid of
  32 rational numbers.
  33 *)
  34
  35 inline "cic:/CoRN/model/setoids/Qpossetoid/Qpos.con".
  36
  37 inline "cic:/CoRN/model/setoids/Qpossetoid/QposP.con".
  38
  39 (*#* One, two and four are elements of it.
  40 *)
  41
  42 inline "cic:/CoRN/model/setoids/Qpossetoid/QONEpos.con".
  43
  44 inline "cic:/CoRN/model/setoids/Qpossetoid/QTWOpos.con".
  45
  46 inline "cic:/CoRN/model/setoids/Qpossetoid/QFOURpos.con".
  47
  48 (*#* ***Multiplication
  49 As we have seen, multiplication preserves positivity, so we can restrict it
  50  to the positive rationals. We see that this restricted multiplication has some
  51  nice properties.
  52 *)
  53
  54 inline "cic:/CoRN/model/setoids/Qpossetoid/Qmult_pres_pos1.con".
  55
  56 inline "cic:/CoRN/model/setoids/Qpossetoid/Qpos_mult.con".
  57
  58 inline "cic:/CoRN/model/setoids/Qpossetoid/associative_Qpos_mult.con".
  59
  60 (*#* ***Inverse
  61 We restrict the domain of the inverse to the set of positive rationals.
  62 *)
  63
  64 inline "cic:/CoRN/model/setoids/Qpossetoid/Qpos_inv.con".
  65
  66 (*#* The restricted inverse preserves positivity.
  67 *)
  68
  69 inline "cic:/CoRN/model/setoids/Qpossetoid/inv_pres_pos1.con".
  70
  71 (*#* Now, we can also restrict the co-domain.
  72 *)
  73
  74 inline "cic:/CoRN/model/setoids/Qpossetoid/Qpos_Qpos_inv.con".
  75
  76 (*#* This restricted inverse map appears a setoid function.
  77 *)
  78
  79 inline "cic:/CoRN/model/setoids/Qpossetoid/Qpos_Qpos_inv_strong_ext.con".
  80
  81 inline "cic:/CoRN/model/setoids/Qpossetoid/Qpos_Qpos_inv_op.con".
  82
  83 (*#* ***Special multiplication and inverse
  84 We define [multdiv2]: $(x,y) \mapsto xy/2$ #(x,y) &#x21A6; xy/2#.
  85 *)
  86
  87 inline "cic:/CoRN/model/setoids/Qpossetoid/Qpos_div2.con".
  88
  89 inline "cic:/CoRN/model/setoids/Qpossetoid/multdiv2.con".
  90
  91 inline "cic:/CoRN/model/setoids/Qpossetoid/associative_multdiv2.con".
  92
  93 (*#* And its inverse [multdiv4]: $x \mapsto 4/x$ #x &#x21A6; 4/x#.
  94 *)
  95
  96 inline "cic:/CoRN/model/setoids/Qpossetoid/mult4.con".
  97
  98 inline "cic:/CoRN/model/setoids/Qpossetoid/divmult4.con".
  99