helm/software/matita/contribs/CoRN-Procedural/ftc/PartInterval.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: PartInterval.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *)
  20
  21 include "ftc/IntervalFunct.ma".
  22
  23 (* UNEXPORTED
  24 Section Conversion
  25 *)
  26
  27 (*#* *Correspondence
  28
  29 In this file we prove that there are mappings going in both ways
  30 between the set of partial functions whose domain contains
  31 [[a,b]] and the set of real-valued functions with domain on
  32 that interval.  These mappings form an adjunction, and thus they have
  33 all the good properties for preservation results.
  34
  35 **Mappings
  36
  37 We begin by defining the map from partial functions to setoid
  38 functions as simply being the restriction of the partial function to
  39 the interval [[a,b]].
  40
  41 %\begin{convention}% Let [F] be a partial function and [a,b:IR] such
  42 that [I [=] [a,b]] is included in the domain of [F].
  43 %\end{convention}%
  44 *)
  45
  46 alias id "F" = "cic:/CoRN/ftc/PartInterval/Conversion/F.var".
  47
  48 alias id "a" = "cic:/CoRN/ftc/PartInterval/Conversion/a.var".
  49
  50 alias id "b" = "cic:/CoRN/ftc/PartInterval/Conversion/b.var".
  51
  52 alias id "Hab" = "cic:/CoRN/ftc/PartInterval/Conversion/Hab.var".
  53
  54 (* begin hide *)
  55
  56 inline procedural "cic:/CoRN/ftc/PartInterval/Conversion/I.con" "Conversion__".
  57
  58 (* end hide *)
  59
  60 alias id "Hf" = "cic:/CoRN/ftc/PartInterval/Conversion/Hf.var".
  61
  62 inline procedural "cic:/CoRN/ftc/PartInterval/IntPartIR_strext.con".
  63
  64 inline procedural "cic:/CoRN/ftc/PartInterval/IntPartIR.con".
  65
  66 (* UNEXPORTED
  67 End Conversion
  68 *)
  69
  70 (* UNEXPORTED
  71 Implicit Arguments IntPartIR [F a b Hab].
  72 *)
  73
  74 (* UNEXPORTED
  75 Section AntiConversion
  76 *)
  77
  78 (*#*
  79 To go the other way around, we simply take a setoid function [f] with
  80 domain [[a,b]] and build the corresponding partial function.
  81 *)
  82
  83 alias id "a" = "cic:/CoRN/ftc/PartInterval/AntiConversion/a.var".
  84
  85 alias id "b" = "cic:/CoRN/ftc/PartInterval/AntiConversion/b.var".
  86
  87 alias id "Hab" = "cic:/CoRN/ftc/PartInterval/AntiConversion/Hab.var".
  88
  89 (* begin hide *)
  90
  91 inline procedural "cic:/CoRN/ftc/PartInterval/AntiConversion/I.con" "AntiConversion__".
  92
  93 (* end hide *)
  94
  95 alias id "f" = "cic:/CoRN/ftc/PartInterval/AntiConversion/f.var".
  96
  97 inline procedural "cic:/CoRN/ftc/PartInterval/PartInt_strext.con".
  98
  99 inline procedural "cic:/CoRN/ftc/PartInterval/PartInt.con".
 100
 101 (* UNEXPORTED
 102 End AntiConversion
 103 *)
 104
 105 (* UNEXPORTED
 106 Implicit Arguments PartInt [a b Hab].
 107 *)
 108
 109 (* UNEXPORTED
 110 Section Inverses
 111 *)
 112
 113 (*#*
 114 In one direction these operators are inverses.
 115 *)
 116
 117 inline procedural "cic:/CoRN/ftc/PartInterval/int_part_int.con".
 118
 119 (* UNEXPORTED
 120 End Inverses
 121 *)
 122
 123 (* UNEXPORTED
 124 Section Equivalences
 125 *)
 126
 127 (*#* **Mappings Preserve Operations
 128
 129 We now prove that all the operations we have defined on both sets are
 130 preserved by [PartInt].
 131
 132 %\begin{convention}% Let [F,G] be partial functions and [a,b:IR] and
 133 denote by [I] the interval [[a,b]].  Let [f,g] be setoid functions of
 134 type [I->IR] equal respectively to [F] and [G] in [I].
 135 %\end{convention}%
 136 *)
 137
 138 alias id "F" = "cic:/CoRN/ftc/PartInterval/Equivalences/F.var".
 139
 140 alias id "G" = "cic:/CoRN/ftc/PartInterval/Equivalences/G.var".
 141
 142 alias id "a" = "cic:/CoRN/ftc/PartInterval/Equivalences/a.var".
 143
 144 alias id "b" = "cic:/CoRN/ftc/PartInterval/Equivalences/b.var".
 145
 146 alias id "c" = "cic:/CoRN/ftc/PartInterval/Equivalences/c.var".
 147
 148 alias id "Hab" = "cic:/CoRN/ftc/PartInterval/Equivalences/Hab.var".
 149
 150 (* begin hide *)
 151
 152 inline procedural "cic:/CoRN/ftc/PartInterval/Equivalences/I.con" "Equivalences__".
 153
 154 (* end hide *)
 155
 156 alias id "f" = "cic:/CoRN/ftc/PartInterval/Equivalences/f.var".
 157
 158 alias id "g" = "cic:/CoRN/ftc/PartInterval/Equivalences/g.var".
 159
 160 alias id "Ff" = "cic:/CoRN/ftc/PartInterval/Equivalences/Ff.var".
 161
 162 alias id "Gg" = "cic:/CoRN/ftc/PartInterval/Equivalences/Gg.var".
 163
 164 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_const.con".
 165
 166 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_id.con".
 167
 168 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_plus.con".
 169
 170 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_inv.con".
 171
 172 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_minus.con".
 173
 174 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_mult.con".
 175
 176 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_nth.con".
 177
 178 (* begin show *)
 179
 180 alias id "HG" = "cic:/CoRN/ftc/PartInterval/Equivalences/HG.var".
 181
 182 alias id "Hg" = "cic:/CoRN/ftc/PartInterval/Equivalences/Hg.var".
 183
 184 (* end show *)
 185
 186 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_recip.con".
 187
 188 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_div.con".
 189
 190 (* UNEXPORTED
 191 End Equivalences
 192 *)
 193