helm/software/matita/contribs/procedural/CoRN/model/setoids/Qpossetoid.mma

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