helm/software/matita/contribs/procedural/CoRN/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 (* UNEXPORTED
  47 cic:/CoRN/ftc/PartInterval/Conversion/F.var
  48 *)
  49
  50 (* UNEXPORTED
  51 cic:/CoRN/ftc/PartInterval/Conversion/a.var
  52 *)
  53
  54 (* UNEXPORTED
  55 cic:/CoRN/ftc/PartInterval/Conversion/b.var
  56 *)
  57
  58 (* UNEXPORTED
  59 cic:/CoRN/ftc/PartInterval/Conversion/Hab.var
  60 *)
  61
  62 (* begin hide *)
  63
  64 inline procedural "cic:/CoRN/ftc/PartInterval/Conversion/I.con" "Conversion__" as definition.
  65
  66 (* end hide *)
  67
  68 (* UNEXPORTED
  69 cic:/CoRN/ftc/PartInterval/Conversion/Hf.var
  70 *)
  71
  72 inline procedural "cic:/CoRN/ftc/PartInterval/IntPartIR_strext.con" as lemma.
  73
  74 inline procedural "cic:/CoRN/ftc/PartInterval/IntPartIR.con" as definition.
  75
  76 (* UNEXPORTED
  77 End Conversion
  78 *)
  79
  80 (* UNEXPORTED
  81 Implicit Arguments IntPartIR [F a b Hab].
  82 *)
  83
  84 (* UNEXPORTED
  85 Section AntiConversion
  86 *)
  87
  88 (*#*
  89 To go the other way around, we simply take a setoid function [f] with
  90 domain [[a,b]] and build the corresponding partial function.
  91 *)
  92
  93 (* UNEXPORTED
  94 cic:/CoRN/ftc/PartInterval/AntiConversion/a.var
  95 *)
  96
  97 (* UNEXPORTED
  98 cic:/CoRN/ftc/PartInterval/AntiConversion/b.var
  99 *)
 100
 101 (* UNEXPORTED
 102 cic:/CoRN/ftc/PartInterval/AntiConversion/Hab.var
 103 *)
 104
 105 (* begin hide *)
 106
 107 inline procedural "cic:/CoRN/ftc/PartInterval/AntiConversion/I.con" "AntiConversion__" as definition.
 108
 109 (* end hide *)
 110
 111 (* UNEXPORTED
 112 cic:/CoRN/ftc/PartInterval/AntiConversion/f.var
 113 *)
 114
 115 inline procedural "cic:/CoRN/ftc/PartInterval/PartInt_strext.con" as lemma.
 116
 117 inline procedural "cic:/CoRN/ftc/PartInterval/PartInt.con" as definition.
 118
 119 (* UNEXPORTED
 120 End AntiConversion
 121 *)
 122
 123 (* UNEXPORTED
 124 Implicit Arguments PartInt [a b Hab].
 125 *)
 126
 127 (* UNEXPORTED
 128 Section Inverses
 129 *)
 130
 131 (*#*
 132 In one direction these operators are inverses.
 133 *)
 134
 135 inline procedural "cic:/CoRN/ftc/PartInterval/int_part_int.con" as lemma.
 136
 137 (* UNEXPORTED
 138 End Inverses
 139 *)
 140
 141 (* UNEXPORTED
 142 Section Equivalences
 143 *)
 144
 145 (*#* **Mappings Preserve Operations
 146
 147 We now prove that all the operations we have defined on both sets are
 148 preserved by [PartInt].
 149
 150 %\begin{convention}% Let [F,G] be partial functions and [a,b:IR] and
 151 denote by [I] the interval [[a,b]].  Let [f,g] be setoid functions of
 152 type [I->IR] equal respectively to [F] and [G] in [I].
 153 %\end{convention}%
 154 *)
 155
 156 (* UNEXPORTED
 157 cic:/CoRN/ftc/PartInterval/Equivalences/F.var
 158 *)
 159
 160 (* UNEXPORTED
 161 cic:/CoRN/ftc/PartInterval/Equivalences/G.var
 162 *)
 163
 164 (* UNEXPORTED
 165 cic:/CoRN/ftc/PartInterval/Equivalences/a.var
 166 *)
 167
 168 (* UNEXPORTED
 169 cic:/CoRN/ftc/PartInterval/Equivalences/b.var
 170 *)
 171
 172 (* UNEXPORTED
 173 cic:/CoRN/ftc/PartInterval/Equivalences/c.var
 174 *)
 175
 176 (* UNEXPORTED
 177 cic:/CoRN/ftc/PartInterval/Equivalences/Hab.var
 178 *)
 179
 180 (* begin hide *)
 181
 182 inline procedural "cic:/CoRN/ftc/PartInterval/Equivalences/I.con" "Equivalences__" as definition.
 183
 184 (* end hide *)
 185
 186 (* UNEXPORTED
 187 cic:/CoRN/ftc/PartInterval/Equivalences/f.var
 188 *)
 189
 190 (* UNEXPORTED
 191 cic:/CoRN/ftc/PartInterval/Equivalences/g.var
 192 *)
 193
 194 (* UNEXPORTED
 195 cic:/CoRN/ftc/PartInterval/Equivalences/Ff.var
 196 *)
 197
 198 (* UNEXPORTED
 199 cic:/CoRN/ftc/PartInterval/Equivalences/Gg.var
 200 *)
 201
 202 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_const.con" as lemma.
 203
 204 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_id.con" as lemma.
 205
 206 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_plus.con" as lemma.
 207
 208 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_inv.con" as lemma.
 209
 210 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_minus.con" as lemma.
 211
 212 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_mult.con" as lemma.
 213
 214 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_nth.con" as lemma.
 215
 216 (* begin show *)
 217
 218 (* UNEXPORTED
 219 cic:/CoRN/ftc/PartInterval/Equivalences/HG.var
 220 *)
 221
 222 (* UNEXPORTED
 223 cic:/CoRN/ftc/PartInterval/Equivalences/Hg.var
 224 *)
 225
 226 (* end show *)
 227
 228 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_recip.con" as lemma.
 229
 230 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_div.con" as lemma.
 231
 232 (* UNEXPORTED
 233 End Equivalences
 234 *)
 235