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