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".
21 (* $Id: CSetoidFun.v,v 1.10 2004/04/23 10:00:53 lcf Exp $ *)
23 include "algebra/CSetoids.ma".
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 alias id "S1" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S1.var".
37 alias id "S2" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S2.var".
39 alias id "S3" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S3.var".
41 alias id "f" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/f.var".
43 alias id "g" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/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 alias id "S" = "cic:/CoRN/algebra/CSetoidFun/BinProj/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 alias id "S1" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S1.var".
107 alias id "S2" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S2.var".
109 alias id "S3" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/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 alias id "f" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/f.var".
123 alias id "op" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/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.
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 alias id "S" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/S.var".
182 alias id "P" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/P.var".
184 alias id "Q" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/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 alias id "P" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/P.var".
204 alias id "Q" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/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 alias id "P" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/P.var".
232 alias id "R" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/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 Notation Conj := (conjP _).
257 Implicit Arguments disj [S].
261 Implicit Arguments extend [S].
265 Implicit Arguments ext1 [S P R x].
269 Implicit Arguments ext2 [S P R x].
274 We are now ready to define the concept of partial function between arbitrary setoids.
277 inline "cic:/CoRN/algebra/CSetoidFun/BinPartFunct.ind".
279 coercion cic:/matita/CoRN-Decl/algebra/CSetoidFun/bpfpfun.con 0 (* compounds *).
282 Notation BDom := (bpfdom _ _).
286 Implicit Arguments bpfpfun [S1 S2].
290 The next lemma states that every partial function is well defined.
293 inline "cic:/CoRN/algebra/CSetoidFun/bpfwdef.con".
295 (*#* Similar for automorphisms. *)
297 inline "cic:/CoRN/algebra/CSetoidFun/PartFunct.ind".
299 coercion cic:/matita/CoRN-Decl/algebra/CSetoidFun/pfpfun.con 0 (* compounds *).
302 Notation Dom := (pfdom _).
306 Notation Part := (pfpfun _).
310 Implicit Arguments pfpfun [S].
314 The next lemma states that every partial function is well defined.
317 inline "cic:/CoRN/algebra/CSetoidFun/pfwdef.con".
320 A few characteristics of this definition should be explained:
321 - The domain of the partial function is characterized by a predicate
322 that is required to be well defined but not strongly extensional. The
323 motivation for this choice comes from two facts: first, one very
324 important subset of real numbers is the compact interval
325 [[a,b]]---characterized by the predicate [ fun x : IR => a [<=] x /\ x
326 [<=] b], which is not strongly extensional; on the other hand, if we
327 can apply a function to an element [s] of a setoid [S] it seems
328 reasonable (and at some point we do have to do it) to apply that same
329 function to any element [s'] which is equal to [s] from the point of
330 view of the setoid equality.
331 - The last two conditions state that [pfpfun] is really a subsetoid
332 function. The reason why we do not write it that way is the
333 following: when applying a partial function [f] to an element [s] of
334 [S] we also need a proof object [H]; with this definition the object
335 we get is [f(s,H)], where the proof is kept separate from the object.
336 Using subsetoid notation, we would get $f(\langle
337 s,H\rangle)$#f(⟨s,H⟩)#; from this we need to apply two
338 projections to get either the original object or the proof, and we
339 need to apply an extra constructor to get $f(\langle
340 s,H\rangle)$#f(⟨s,H⟩)# from [s] and [H]. This amounts
341 to spending more resources when actually working with these objects.
342 - This record has type [Type], which is very unfortunate, because it
343 means in particular that we cannot use the well behaved set
344 existential quantification over partial functions; however, later on
345 we will manage to avoid this problem in a way that also justifies that
346 we don't really need to use that kind of quantification. Another
347 approach to this definition that completely avoid this complication
348 would be to make [PartFunct] a dependent type, receiving the predicate
349 as an argument. This does work in that it allows us to give
350 [PartFunct] type [Set] and do some useful stuff with it; however, we
351 are not able to define something as simple as an operator that gets a
352 function and returns its domain (because of the restrictions in the
353 type elimination rules). This sounds very unnatural, and soon gets us
354 into strange problems that yield very unlikely definitions, which is
355 why we chose to altogether do away with this approach.
357 %\begin{convention}% All partial functions will henceforth be denoted by capital letters.
360 We now present some methods for defining partial functions.
364 Hint Resolve CI: core.
371 alias id "S" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/S.var".
374 To begin with, we want to be able to ``see'' each total function as a partial function.
377 inline "cic:/CoRN/algebra/CSetoidFun/total_eq_part.con".
380 Section Part_Function_Const
384 In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:
386 %\begin{convention}% Let [c:S].
390 alias id "c" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Const/c.var".
392 inline "cic:/CoRN/algebra/CSetoidFun/Fconst.con".
395 End Part_Function_Const
399 Section Part_Function_Id
402 inline "cic:/CoRN/algebra/CSetoidFun/Fid.con".
409 (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.)
411 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.
413 %\begin{convention}% Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing their domains.
418 Section Part_Function_Composition
421 alias id "G" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/G.var".
423 alias id "F" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/F.var".
427 inline "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/P.con" "CSetoid_Ops__Part_Function_Composition__".
429 inline "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/Q.con" "CSetoid_Ops__Part_Function_Composition__".
433 inline "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/R.con" "CSetoid_Ops__Part_Function_Composition__".
435 inline "cic:/CoRN/algebra/CSetoidFun/part_function_comp_strext.con".
437 inline "cic:/CoRN/algebra/CSetoidFun/part_function_comp_dom_wd.con".
439 inline "cic:/CoRN/algebra/CSetoidFun/Fcomp.con".
442 End Part_Function_Composition
450 %\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains.
455 Section BinPart_Function_Composition
458 alias id "S1" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S1.var".
460 alias id "S2" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S2.var".
462 alias id "S3" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S3.var".
464 alias id "G" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/G.var".
466 alias id "F" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/F.var".
470 inline "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/P.con" "BinPart_Function_Composition__".
472 inline "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/Q.con" "BinPart_Function_Composition__".
476 inline "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/R.con" "BinPart_Function_Composition__".
478 inline "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_strext.con".
480 inline "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_dom_wd.con".
482 inline "cic:/CoRN/algebra/CSetoidFun/BinFcomp.con".
485 End BinPart_Function_Composition
488 (* Different tokens for compatibility with coqdoc *)
491 Implicit Arguments Fconst [S].
495 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
499 Notation FId := (Fid _).
503 Implicit Arguments Fcomp [S].
507 Infix "[o]" := Fcomp (at level 65, no associativity).
511 Hint Resolve pfwdef bpfwdef: algebra.
520 inline "cic:/CoRN/algebra/CSetoidFun/injective.con".
522 inline "cic:/CoRN/algebra/CSetoidFun/injective_weak.con".
524 inline "cic:/CoRN/algebra/CSetoidFun/surjective.con".
527 Implicit Arguments injective [A B].
531 Implicit Arguments injective_weak [A B].
535 Implicit Arguments surjective [A B].
538 inline "cic:/CoRN/algebra/CSetoidFun/injective_imp_injective_weak.con".
540 inline "cic:/CoRN/algebra/CSetoidFun/bijective.con".
543 Implicit Arguments bijective [A B].
546 inline "cic:/CoRN/algebra/CSetoidFun/id_is_bij.con".
548 inline "cic:/CoRN/algebra/CSetoidFun/comp_resp_bij.con".
550 inline "cic:/CoRN/algebra/CSetoidFun/inv.con".
553 Implicit Arguments inv [A B].
556 inline "cic:/CoRN/algebra/CSetoidFun/invfun.con".
559 Implicit Arguments invfun [A B].
562 inline "cic:/CoRN/algebra/CSetoidFun/inv1.con".
564 inline "cic:/CoRN/algebra/CSetoidFun/inv2.con".
566 inline "cic:/CoRN/algebra/CSetoidFun/inv_strext.con".
568 inline "cic:/CoRN/algebra/CSetoidFun/Inv.con".
571 Implicit Arguments Inv [A B].
574 inline "cic:/CoRN/algebra/CSetoidFun/Inv_bij.con".
581 Implicit Arguments bijective [A B].
585 Implicit Arguments injective [A B].
589 Implicit Arguments injective_weak [A B].
593 Implicit Arguments surjective [A B].
597 Implicit Arguments inv [A B].
601 Implicit Arguments invfun [A B].
605 Implicit Arguments Inv [A B].
609 Implicit Arguments conj_wd [S P Q].
613 Notation Prj1 := (prj1 _ _ _ _).
617 Notation Prj2 := (prj2 _ _ _ _).