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 *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSetoidFun".
19 (* $Id: CSetoidFun.v,v 1.10 2004/04/23 10:00:53 lcf Exp $ *)
26 Section unary_function_composition.
29 (*#* ** Composition of Setoid functions
31 Let [S1], [S2] and [S3] be setoids, [f] a
32 setoid function from [S1] to [S2], and [g] from [S2]
33 to [S3] in the following definition of composition. *)
35 inline cic:/CoRN/algebra/CSetoidFun/S1.var.
37 inline cic:/CoRN/algebra/CSetoidFun/S2.var.
39 inline cic:/CoRN/algebra/CSetoidFun/S3.var.
41 inline cic:/CoRN/algebra/CSetoidFun/f.var.
43 inline cic:/CoRN/algebra/CSetoidFun/g.var.
45 inline cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_fun.con.
48 End unary_function_composition.
52 Section unary_and_binary_function_composition.
55 inline cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_un_fun.con.
57 inline cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_fun.con.
59 inline cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_un_bin_fun.con.
62 End unary_and_binary_function_composition.
69 Section function_projection.
72 inline cic:/CoRN/algebra/CSetoidFun/proj_bin_fun.con.
74 inline cic:/CoRN/algebra/CSetoidFun/projected_bin_fun.con.
77 End function_projection.
84 inline cic:/CoRN/algebra/CSetoidFun/S.var.
86 inline cic:/CoRN/algebra/CSetoidFun/binproj1.con.
88 inline cic:/CoRN/algebra/CSetoidFun/binproj1_strext.con.
90 inline cic:/CoRN/algebra/CSetoidFun/cs_binproj1.con.
96 (*#* **Combining operations
97 %\begin{convention}% Let [S1], [S2] and [S3] be setoids.
102 Section CombiningOperations.
105 inline cic:/CoRN/algebra/CSetoidFun/S1.var.
107 inline cic:/CoRN/algebra/CSetoidFun/S2.var.
109 inline cic:/CoRN/algebra/CSetoidFun/S3.var.
112 In the following definition, we assume [f] is a setoid function from
113 [S1] to [S2], and [op] is an unary operation on [S2].
114 Then [opOnFun] is the composition [op] after [f].
118 Section CombiningUnaryOperations.
121 inline cic:/CoRN/algebra/CSetoidFun/f.var.
123 inline cic:/CoRN/algebra/CSetoidFun/op.var.
125 inline cic:/CoRN/algebra/CSetoidFun/opOnFun.con.
128 End CombiningUnaryOperations.
132 End CombiningOperations.
135 (*#* **Partial Functions
137 In this section we define a concept of partial function for an
138 arbitrary setoid. Essentially, a partial function is what would be
139 expected---a predicate on the setoid in question and a total function
140 from the set of points satisfying that predicate to the setoid. There
141 is one important limitations to this approach: first, the record we
142 obtain has type [Type], meaning that we can't use, for instance,
143 elimination of existential quantifiers.
145 Furthermore, for reasons we will explain ahead, partial functions will
146 not be defined via the [CSetoid_fun] record, but the whole structure
147 will be incorporated in a new record.
149 Finally, notice that to be completely general the domains of the
150 functions have to be characterized by a [CProp]-valued predicate;
151 otherwise, the use you can make of a function will be %\emph{%#<i>#a
152 priori#</i>#%}% restricted at the moment it is defined.
154 Before we state our definitions we need to do some work on domains.
158 Section SubSets_of_G.
161 (*#* ***Subsets of Setoids
163 Subsets of a setoid will be identified with predicates from the
164 carrier set of the setoid into [CProp]. At this stage, we do not make
165 any assumptions about these predicates.
167 We will begin by defining elementary operations on predicates, along
168 with their basic properties. In particular, we will work with well
169 defined predicates, so we will prove that these operations preserve
172 %\begin{convention}% Let [S:CSetoid] and [P,Q:S->CProp].
176 inline cic:/CoRN/algebra/CSetoidFun/S.var.
182 inline cic:/CoRN/algebra/CSetoidFun/P.var.
184 inline cic:/CoRN/algebra/CSetoidFun/Q.var.
186 inline cic:/CoRN/algebra/CSetoidFun/conjP.con.
188 inline cic:/CoRN/algebra/CSetoidFun/prj1.con.
190 inline cic:/CoRN/algebra/CSetoidFun/prj2.con.
192 inline cic:/CoRN/algebra/CSetoidFun/conj_wd.con.
202 inline cic:/CoRN/algebra/CSetoidFun/P.var.
204 inline cic:/CoRN/algebra/CSetoidFun/Q.var.
207 Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets).
210 inline cic:/CoRN/algebra/CSetoidFun/disj.con.
212 inline cic:/CoRN/algebra/CSetoidFun/inj1.con.
214 inline cic:/CoRN/algebra/CSetoidFun/inj2.con.
216 inline cic:/CoRN/algebra/CSetoidFun/disj_wd.con.
227 The next definition is a bit tricky, and is useful for choosing among the elements that satisfy a predicate [P] those that also satisfy [R] in the case where [R] is only defined for elements satisfying [P]---consider [R] to be a condition on the image of an object via a function with domain [P]. We chose to call this operation [extension].
230 inline cic:/CoRN/algebra/CSetoidFun/P.var.
232 inline cic:/CoRN/algebra/CSetoidFun/R.var.
234 inline cic:/CoRN/algebra/CSetoidFun/extend.con.
236 inline cic:/CoRN/algebra/CSetoidFun/ext1.con.
238 inline cic:/CoRN/algebra/CSetoidFun/ext2_a.con.
240 inline cic:/CoRN/algebra/CSetoidFun/ext2.con.
242 inline cic:/CoRN/algebra/CSetoidFun/extension_wd.con.
253 Implicit Arguments disj [S].
257 Implicit Arguments extend [S].
261 Implicit Arguments ext1 [S P R x].
265 Implicit Arguments ext2 [S P R x].
270 We are now ready to define the concept of partial function between arbitrary setoids.
273 inline cic:/CoRN/algebra/CSetoidFun/BinPartFunct.ind.
276 Implicit Arguments bpfpfun [S1 S2].
280 The next lemma states that every partial function is well defined.
283 inline cic:/CoRN/algebra/CSetoidFun/bpfwdef.con.
285 (*#* Similar for automorphisms. *)
287 inline cic:/CoRN/algebra/CSetoidFun/PartFunct.ind.
290 Implicit Arguments pfpfun [S].
294 The next lemma states that every partial function is well defined.
297 inline cic:/CoRN/algebra/CSetoidFun/pfwdef.con.
300 A few characteristics of this definition should be explained:
301 - The domain of the partial function is characterized by a predicate
302 that is required to be well defined but not strongly extensional. The
303 motivation for this choice comes from two facts: first, one very
304 important subset of real numbers is the compact interval
305 [[a,b]]---characterized by the predicate [ fun x : IR => a [<=] x /\ x
306 [<=] b], which is not strongly extensional; on the other hand, if we
307 can apply a function to an element [s] of a setoid [S] it seems
308 reasonable (and at some point we do have to do it) to apply that same
309 function to any element [s'] which is equal to [s] from the point of
310 view of the setoid equality.
311 - The last two conditions state that [pfpfun] is really a subsetoid
312 function. The reason why we do not write it that way is the
313 following: when applying a partial function [f] to an element [s] of
314 [S] we also need a proof object [H]; with this definition the object
315 we get is [f(s,H)], where the proof is kept separate from the object.
316 Using subsetoid notation, we would get $f(\langle
317 s,H\rangle)$#f(⟨s,H⟩)#; from this we need to apply two
318 projections to get either the original object or the proof, and we
319 need to apply an extra constructor to get $f(\langle
320 s,H\rangle)$#f(⟨s,H⟩)# from [s] and [H]. This amounts
321 to spending more resources when actually working with these objects.
322 - This record has type [Type], which is very unfortunate, because it
323 means in particular that we cannot use the well behaved set
324 existential quantification over partial functions; however, later on
325 we will manage to avoid this problem in a way that also justifies that
326 we don't really need to use that kind of quantification. Another
327 approach to this definition that completely avoid this complication
328 would be to make [PartFunct] a dependent type, receiving the predicate
329 as an argument. This does work in that it allows us to give
330 [PartFunct] type [Set] and do some useful stuff with it; however, we
331 are not able to define something as simple as an operator that gets a
332 function and returns its domain (because of the restrictions in the
333 type elimination rules). This sounds very unnatural, and soon gets us
334 into strange problems that yield very unlikely definitions, which is
335 why we chose to altogether do away with this approach.
337 %\begin{convention}% All partial functions will henceforth be denoted by capital letters.
340 We now present some methods for defining partial functions.
344 Hint Resolve CI: core.
351 inline cic:/CoRN/algebra/CSetoidFun/S.var.
354 To begin with, we want to be able to ``see'' each total function as a partial function.
357 inline cic:/CoRN/algebra/CSetoidFun/total_eq_part.con.
360 Section Part_Function_Const.
364 In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:
366 %\begin{convention}% Let [c:S].
370 inline cic:/CoRN/algebra/CSetoidFun/c.var.
372 inline cic:/CoRN/algebra/CSetoidFun/Fconst.con.
375 End Part_Function_Const.
379 Section Part_Function_Id.
382 inline cic:/CoRN/algebra/CSetoidFun/Fid.con.
385 End Part_Function_Id.
389 (These happen to be always total functions, but that is more or less obvious, as we have no information on the setoid; however, we will be able to define partial functions just applying other operators to these ones.)
391 If we have two setoid functions [F] and [G] we can always compose them. The domain of our new function will be the set of points [s] in the domain of [F] for which [F(s)] is in the domain of [G]#. #%\footnote{%Notice that the use of extension here is essential.%}.% The inversion in the order of the variables is done to maintain uniformity with the usual mathematical notation.
393 %\begin{convention}% Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing their domains.
398 Section Part_Function_Composition.
401 inline cic:/CoRN/algebra/CSetoidFun/G.var.
403 inline cic:/CoRN/algebra/CSetoidFun/F.var.
407 inline cic:/CoRN/algebra/CSetoidFun/P.con.
409 inline cic:/CoRN/algebra/CSetoidFun/Q.con.
413 inline cic:/CoRN/algebra/CSetoidFun/R.con.
415 inline cic:/CoRN/algebra/CSetoidFun/part_function_comp_strext.con.
417 inline cic:/CoRN/algebra/CSetoidFun/part_function_comp_dom_wd.con.
419 inline cic:/CoRN/algebra/CSetoidFun/Fcomp.con.
422 End Part_Function_Composition.
430 %\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains.
435 Section BinPart_Function_Composition.
438 inline cic:/CoRN/algebra/CSetoidFun/S1.var.
440 inline cic:/CoRN/algebra/CSetoidFun/S2.var.
442 inline cic:/CoRN/algebra/CSetoidFun/S3.var.
444 inline cic:/CoRN/algebra/CSetoidFun/G.var.
446 inline cic:/CoRN/algebra/CSetoidFun/F.var.
450 inline cic:/CoRN/algebra/CSetoidFun/P.con.
452 inline cic:/CoRN/algebra/CSetoidFun/Q.con.
456 inline cic:/CoRN/algebra/CSetoidFun/R.con.
458 inline cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_strext.con.
460 inline cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_dom_wd.con.
462 inline cic:/CoRN/algebra/CSetoidFun/BinFcomp.con.
465 End BinPart_Function_Composition.
468 (* Different tokens for compatibility with coqdoc *)
471 Implicit Arguments Fconst [S].
475 Implicit Arguments Fcomp [S].
479 Hint Resolve pfwdef bpfwdef: algebra.
488 inline cic:/CoRN/algebra/CSetoidFun/injective.con.
490 inline cic:/CoRN/algebra/CSetoidFun/injective_weak.con.
492 inline cic:/CoRN/algebra/CSetoidFun/surjective.con.
495 Implicit Arguments injective [A B].
499 Implicit Arguments injective_weak [A B].
503 Implicit Arguments surjective [A B].
506 inline cic:/CoRN/algebra/CSetoidFun/injective_imp_injective_weak.con.
508 inline cic:/CoRN/algebra/CSetoidFun/bijective.con.
511 Implicit Arguments bijective [A B].
514 inline cic:/CoRN/algebra/CSetoidFun/id_is_bij.con.
516 inline cic:/CoRN/algebra/CSetoidFun/comp_resp_bij.con.
518 inline cic:/CoRN/algebra/CSetoidFun/inv.con.
521 Implicit Arguments inv [A B].
524 inline cic:/CoRN/algebra/CSetoidFun/invfun.con.
527 Implicit Arguments invfun [A B].
530 inline cic:/CoRN/algebra/CSetoidFun/inv1.con.
532 inline cic:/CoRN/algebra/CSetoidFun/inv2.con.
534 inline cic:/CoRN/algebra/CSetoidFun/inv_strext.con.
536 inline cic:/CoRN/algebra/CSetoidFun/Inv.con.
539 Implicit Arguments Inv [A B].
542 inline cic:/CoRN/algebra/CSetoidFun/Inv_bij.con.
549 Implicit Arguments bijective [A B].
553 Implicit Arguments injective [A B].
557 Implicit Arguments injective_weak [A B].
561 Implicit Arguments surjective [A B].
565 Implicit Arguments inv [A B].
569 Implicit Arguments invfun [A B].
573 Implicit Arguments Inv [A B].
577 Implicit Arguments conj_wd [S P Q].