1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (* $Id: PartInterval.v,v 1.6 2004/04/23 10:01:00 lcf Exp $ *)
21 include "ftc/IntervalFunct.ma".
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.
37 We begin by defining the map from partial functions to setoid
38 functions as simply being the restriction of the partial function to
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].
46 alias id "F" = "cic:/CoRN/ftc/PartInterval/Conversion/F.var".
48 alias id "a" = "cic:/CoRN/ftc/PartInterval/Conversion/a.var".
50 alias id "b" = "cic:/CoRN/ftc/PartInterval/Conversion/b.var".
52 alias id "Hab" = "cic:/CoRN/ftc/PartInterval/Conversion/Hab.var".
56 inline procedural "cic:/CoRN/ftc/PartInterval/Conversion/I.con" "Conversion__" as definition.
60 alias id "Hf" = "cic:/CoRN/ftc/PartInterval/Conversion/Hf.var".
62 inline procedural "cic:/CoRN/ftc/PartInterval/IntPartIR_strext.con" as lemma.
64 inline procedural "cic:/CoRN/ftc/PartInterval/IntPartIR.con" as definition.
71 Implicit Arguments IntPartIR [F a b Hab].
75 Section AntiConversion
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.
83 alias id "a" = "cic:/CoRN/ftc/PartInterval/AntiConversion/a.var".
85 alias id "b" = "cic:/CoRN/ftc/PartInterval/AntiConversion/b.var".
87 alias id "Hab" = "cic:/CoRN/ftc/PartInterval/AntiConversion/Hab.var".
91 inline procedural "cic:/CoRN/ftc/PartInterval/AntiConversion/I.con" "AntiConversion__" as definition.
95 alias id "f" = "cic:/CoRN/ftc/PartInterval/AntiConversion/f.var".
97 inline procedural "cic:/CoRN/ftc/PartInterval/PartInt_strext.con" as lemma.
99 inline procedural "cic:/CoRN/ftc/PartInterval/PartInt.con" as definition.
106 Implicit Arguments PartInt [a b Hab].
114 In one direction these operators are inverses.
117 inline procedural "cic:/CoRN/ftc/PartInterval/int_part_int.con" as lemma.
127 (*#* **Mappings Preserve Operations
129 We now prove that all the operations we have defined on both sets are
130 preserved by [PartInt].
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].
138 alias id "F" = "cic:/CoRN/ftc/PartInterval/Equivalences/F.var".
140 alias id "G" = "cic:/CoRN/ftc/PartInterval/Equivalences/G.var".
142 alias id "a" = "cic:/CoRN/ftc/PartInterval/Equivalences/a.var".
144 alias id "b" = "cic:/CoRN/ftc/PartInterval/Equivalences/b.var".
146 alias id "c" = "cic:/CoRN/ftc/PartInterval/Equivalences/c.var".
148 alias id "Hab" = "cic:/CoRN/ftc/PartInterval/Equivalences/Hab.var".
152 inline procedural "cic:/CoRN/ftc/PartInterval/Equivalences/I.con" "Equivalences__" as definition.
156 alias id "f" = "cic:/CoRN/ftc/PartInterval/Equivalences/f.var".
158 alias id "g" = "cic:/CoRN/ftc/PartInterval/Equivalences/g.var".
160 alias id "Ff" = "cic:/CoRN/ftc/PartInterval/Equivalences/Ff.var".
162 alias id "Gg" = "cic:/CoRN/ftc/PartInterval/Equivalences/Gg.var".
164 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_const.con" as lemma.
166 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_id.con" as lemma.
168 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_plus.con" as lemma.
170 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_inv.con" as lemma.
172 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_minus.con" as lemma.
174 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_mult.con" as lemma.
176 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_nth.con" as lemma.
180 alias id "HG" = "cic:/CoRN/ftc/PartInterval/Equivalences/HG.var".
182 alias id "Hg" = "cic:/CoRN/ftc/PartInterval/Equivalences/Hg.var".
186 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_recip.con" as lemma.
188 inline procedural "cic:/CoRN/ftc/PartInterval/part_int_div.con" as lemma.