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: CSetoidFun.v,v 1.10 2004/04/23 10:00:53 lcf Exp $ *)
21 include "algebra/CSetoids.ma".
24 Section unary_function_composition
27 (*#* ** Composition of Setoid functions
29 Let [S1], [S2] and [S3] be setoids, [f] a
30 setoid function from [S1] to [S2], and [g] from [S2]
31 to [S3] in the following definition of composition. *)
33 alias id "S1" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S1.var".
35 alias id "S2" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S2.var".
37 alias id "S3" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S3.var".
39 alias id "f" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/f.var".
41 alias id "g" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/g.var".
43 inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_fun.con" as definition.
46 End unary_function_composition
50 Section unary_and_binary_function_composition
53 inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_un_fun.con" as definition.
55 inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_fun.con" as definition.
57 inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_un_bin_fun.con" as definition.
60 End unary_and_binary_function_composition
67 Section function_projection
70 inline procedural "cic:/CoRN/algebra/CSetoidFun/proj_bin_fun.con" as lemma.
72 inline procedural "cic:/CoRN/algebra/CSetoidFun/projected_bin_fun.con" as definition.
75 End function_projection
82 alias id "S" = "cic:/CoRN/algebra/CSetoidFun/BinProj/S.var".
84 inline procedural "cic:/CoRN/algebra/CSetoidFun/binproj1.con" as definition.
86 inline procedural "cic:/CoRN/algebra/CSetoidFun/binproj1_strext.con" as lemma.
88 inline procedural "cic:/CoRN/algebra/CSetoidFun/cs_binproj1.con" as definition.
94 (*#* **Combining operations
95 %\begin{convention}% Let [S1], [S2] and [S3] be setoids.
100 Section CombiningOperations
103 alias id "S1" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S1.var".
105 alias id "S2" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S2.var".
107 alias id "S3" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S3.var".
110 In the following definition, we assume [f] is a setoid function from
111 [S1] to [S2], and [op] is an unary operation on [S2].
112 Then [opOnFun] is the composition [op] after [f].
116 Section CombiningUnaryOperations
119 alias id "f" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/f.var".
121 alias id "op" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/op.var".
123 inline procedural "cic:/CoRN/algebra/CSetoidFun/opOnFun.con" as definition.
126 End CombiningUnaryOperations
130 End CombiningOperations
133 (*#* **Partial Functions
135 In this section we define a concept of partial function for an
136 arbitrary setoid. Essentially, a partial function is what would be
137 expected---a predicate on the setoid in question and a total function
138 from the set of points satisfying that predicate to the setoid. There
139 is one important limitations to this approach: first, the record we
140 obtain has type [Type], meaning that we can't use, for instance,
141 elimination of existential quantifiers.
143 Furthermore, for reasons we will explain ahead, partial functions will
144 not be defined via the [CSetoid_fun] record, but the whole structure
145 will be incorporated in a new record.
147 Finally, notice that to be completely general the domains of the
148 functions have to be characterized by a [CProp]-valued predicate;
149 otherwise, the use you can make of a function will be %\emph{%#<i>#a
150 priori#</i>#%}% restricted at the moment it is defined.
152 Before we state our definitions we need to do some work on domains.
159 (*#* ***Subsets of Setoids
161 Subsets of a setoid will be identified with predicates from the
162 carrier set of the setoid into [CProp]. At this stage, we do not make
163 any assumptions about these predicates.
165 We will begin by defining elementary operations on predicates, along
166 with their basic properties. In particular, we will work with well
167 defined predicates, so we will prove that these operations preserve
170 %\begin{convention}% Let [S:CSetoid] and [P,Q:S->CProp].
174 alias id "S" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/S.var".
180 alias id "P" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/P.var".
182 alias id "Q" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/Q.var".
184 inline procedural "cic:/CoRN/algebra/CSetoidFun/conjP.con" as definition.
186 inline procedural "cic:/CoRN/algebra/CSetoidFun/prj1.con" as lemma.
188 inline procedural "cic:/CoRN/algebra/CSetoidFun/prj2.con" as lemma.
190 inline procedural "cic:/CoRN/algebra/CSetoidFun/conj_wd.con" as lemma.
200 alias id "P" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/P.var".
202 alias id "Q" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/Q.var".
205 Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets).
208 inline procedural "cic:/CoRN/algebra/CSetoidFun/disj.con" as definition.
210 inline procedural "cic:/CoRN/algebra/CSetoidFun/inj1.con" as lemma.
212 inline procedural "cic:/CoRN/algebra/CSetoidFun/inj2.con" as lemma.
214 inline procedural "cic:/CoRN/algebra/CSetoidFun/disj_wd.con" as lemma.
225 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].
228 alias id "P" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/P.var".
230 alias id "R" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/R.var".
232 inline procedural "cic:/CoRN/algebra/CSetoidFun/extend.con" as definition.
234 inline procedural "cic:/CoRN/algebra/CSetoidFun/ext1.con" as lemma.
236 inline procedural "cic:/CoRN/algebra/CSetoidFun/ext2_a.con" as lemma.
238 inline procedural "cic:/CoRN/algebra/CSetoidFun/ext2.con" as lemma.
240 inline procedural "cic:/CoRN/algebra/CSetoidFun/extension_wd.con" as lemma.
251 Notation Conj := (conjP _).
255 Implicit Arguments disj [S].
259 Implicit Arguments extend [S].
263 Implicit Arguments ext1 [S P R x].
267 Implicit Arguments ext2 [S P R x].
272 We are now ready to define the concept of partial function between arbitrary setoids.
275 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPartFunct.ind".
278 cic:/matita/CoRN-Procedural/algebra/CSetoidFun/bpfpfun.con
282 Notation BDom := (bpfdom _ _).
286 Implicit Arguments bpfpfun [S1 S2].
290 The next lemma states that every partial function is well defined.
293 inline procedural "cic:/CoRN/algebra/CSetoidFun/bpfwdef.con" as lemma.
295 (*#* Similar for automorphisms. *)
297 inline procedural "cic:/CoRN/algebra/CSetoidFun/PartFunct.ind".
300 cic:/matita/CoRN-Procedural/algebra/CSetoidFun/pfpfun.con
304 Notation Dom := (pfdom _).
308 Notation Part := (pfpfun _).
312 Implicit Arguments pfpfun [S].
316 The next lemma states that every partial function is well defined.
319 inline procedural "cic:/CoRN/algebra/CSetoidFun/pfwdef.con" as lemma.
322 A few characteristics of this definition should be explained:
323 - The domain of the partial function is characterized by a predicate
324 that is required to be well defined but not strongly extensional. The
325 motivation for this choice comes from two facts: first, one very
326 important subset of real numbers is the compact interval
327 [[a,b]]---characterized by the predicate [ fun x : IR => a [<=] x /\ x
328 [<=] b], which is not strongly extensional; on the other hand, if we
329 can apply a function to an element [s] of a setoid [S] it seems
330 reasonable (and at some point we do have to do it) to apply that same
331 function to any element [s'] which is equal to [s] from the point of
332 view of the setoid equality.
333 - The last two conditions state that [pfpfun] is really a subsetoid
334 function. The reason why we do not write it that way is the
335 following: when applying a partial function [f] to an element [s] of
336 [S] we also need a proof object [H]; with this definition the object
337 we get is [f(s,H)], where the proof is kept separate from the object.
338 Using subsetoid notation, we would get $f(\langle
339 s,H\rangle)$#f(⟨s,H⟩)#; from this we need to apply two
340 projections to get either the original object or the proof, and we
341 need to apply an extra constructor to get $f(\langle
342 s,H\rangle)$#f(⟨s,H⟩)# from [s] and [H]. This amounts
343 to spending more resources when actually working with these objects.
344 - This record has type [Type], which is very unfortunate, because it
345 means in particular that we cannot use the well behaved set
346 existential quantification over partial functions; however, later on
347 we will manage to avoid this problem in a way that also justifies that
348 we don't really need to use that kind of quantification. Another
349 approach to this definition that completely avoid this complication
350 would be to make [PartFunct] a dependent type, receiving the predicate
351 as an argument. This does work in that it allows us to give
352 [PartFunct] type [Set] and do some useful stuff with it; however, we
353 are not able to define something as simple as an operator that gets a
354 function and returns its domain (because of the restrictions in the
355 type elimination rules). This sounds very unnatural, and soon gets us
356 into strange problems that yield very unlikely definitions, which is
357 why we chose to altogether do away with this approach.
359 %\begin{convention}% All partial functions will henceforth be denoted by capital letters.
362 We now present some methods for defining partial functions.
366 Hint Resolve CI: core.
373 alias id "S" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/S.var".
376 To begin with, we want to be able to ``see'' each total function as a partial function.
379 inline procedural "cic:/CoRN/algebra/CSetoidFun/total_eq_part.con" as definition.
382 Section Part_Function_Const
386 In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:
388 %\begin{convention}% Let [c:S].
392 alias id "c" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Const/c.var".
394 inline procedural "cic:/CoRN/algebra/CSetoidFun/Fconst.con" as definition.
397 End Part_Function_Const
401 Section Part_Function_Id
404 inline procedural "cic:/CoRN/algebra/CSetoidFun/Fid.con" as definition.
411 (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.)
413 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.
415 %\begin{convention}% Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing their domains.
420 Section Part_Function_Composition
423 alias id "G" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/G.var".
425 alias id "F" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/F.var".
429 inline procedural "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/P.con" "CSetoid_Ops__Part_Function_Composition__" as definition.
431 inline procedural "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/Q.con" "CSetoid_Ops__Part_Function_Composition__" as definition.
435 inline procedural "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/R.con" "CSetoid_Ops__Part_Function_Composition__" as definition.
437 inline procedural "cic:/CoRN/algebra/CSetoidFun/part_function_comp_strext.con" as lemma.
439 inline procedural "cic:/CoRN/algebra/CSetoidFun/part_function_comp_dom_wd.con" as lemma.
441 inline procedural "cic:/CoRN/algebra/CSetoidFun/Fcomp.con" as definition.
444 End Part_Function_Composition
452 %\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains.
457 Section BinPart_Function_Composition
460 alias id "S1" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S1.var".
462 alias id "S2" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S2.var".
464 alias id "S3" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S3.var".
466 alias id "G" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/G.var".
468 alias id "F" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/F.var".
472 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/P.con" "BinPart_Function_Composition__" as definition.
474 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/Q.con" "BinPart_Function_Composition__" as definition.
478 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/R.con" "BinPart_Function_Composition__" as definition.
480 inline procedural "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_strext.con" as lemma.
482 inline procedural "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_dom_wd.con" as lemma.
484 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinFcomp.con" as definition.
487 End BinPart_Function_Composition
490 (* Different tokens for compatibility with coqdoc *)
493 Implicit Arguments Fconst [S].
497 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
501 Notation FId := (Fid _).
505 Implicit Arguments Fcomp [S].
509 Infix "[o]" := Fcomp (at level 65, no associativity).
513 Hint Resolve pfwdef bpfwdef: algebra.
522 inline procedural "cic:/CoRN/algebra/CSetoidFun/injective.con" as definition.
524 inline procedural "cic:/CoRN/algebra/CSetoidFun/injective_weak.con" as definition.
526 inline procedural "cic:/CoRN/algebra/CSetoidFun/surjective.con" as definition.
529 Implicit Arguments injective [A B].
533 Implicit Arguments injective_weak [A B].
537 Implicit Arguments surjective [A B].
540 inline procedural "cic:/CoRN/algebra/CSetoidFun/injective_imp_injective_weak.con" as lemma.
542 inline procedural "cic:/CoRN/algebra/CSetoidFun/bijective.con" as definition.
545 Implicit Arguments bijective [A B].
548 inline procedural "cic:/CoRN/algebra/CSetoidFun/id_is_bij.con" as lemma.
550 inline procedural "cic:/CoRN/algebra/CSetoidFun/comp_resp_bij.con" as lemma.
552 inline procedural "cic:/CoRN/algebra/CSetoidFun/inv.con" as lemma.
555 Implicit Arguments inv [A B].
558 inline procedural "cic:/CoRN/algebra/CSetoidFun/invfun.con" as definition.
561 Implicit Arguments invfun [A B].
564 inline procedural "cic:/CoRN/algebra/CSetoidFun/inv1.con" as lemma.
566 inline procedural "cic:/CoRN/algebra/CSetoidFun/inv2.con" as lemma.
568 inline procedural "cic:/CoRN/algebra/CSetoidFun/inv_strext.con" as lemma.
570 inline procedural "cic:/CoRN/algebra/CSetoidFun/Inv.con" as definition.
573 Implicit Arguments Inv [A B].
576 inline procedural "cic:/CoRN/algebra/CSetoidFun/Inv_bij.con" as definition.
583 Implicit Arguments bijective [A B].
587 Implicit Arguments injective [A B].
591 Implicit Arguments injective_weak [A B].
595 Implicit Arguments surjective [A B].
599 Implicit Arguments inv [A B].
603 Implicit Arguments invfun [A B].
607 Implicit Arguments Inv [A B].
611 Implicit Arguments conj_wd [S P Q].
615 Notation Prj1 := (prj1 _ _ _ _).
619 Notation Prj2 := (prj2 _ _ _ _).