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