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. *)
34 cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S1.var
38 cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S2.var
42 cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S3.var
46 cic:/CoRN/algebra/CSetoidFun/unary_function_composition/f.var
50 cic:/CoRN/algebra/CSetoidFun/unary_function_composition/g.var
53 inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_fun.con" as definition.
56 End unary_function_composition
60 Section unary_and_binary_function_composition
63 inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_un_fun.con" as definition.
65 inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_fun.con" as definition.
67 inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_un_bin_fun.con" as definition.
70 End unary_and_binary_function_composition
77 Section function_projection
80 inline procedural "cic:/CoRN/algebra/CSetoidFun/proj_bin_fun.con" as lemma.
82 inline procedural "cic:/CoRN/algebra/CSetoidFun/projected_bin_fun.con" as definition.
85 End function_projection
93 cic:/CoRN/algebra/CSetoidFun/BinProj/S.var
96 inline procedural "cic:/CoRN/algebra/CSetoidFun/binproj1.con" as definition.
98 inline procedural "cic:/CoRN/algebra/CSetoidFun/binproj1_strext.con" as lemma.
100 inline procedural "cic:/CoRN/algebra/CSetoidFun/cs_binproj1.con" as definition.
106 (*#* **Combining operations
107 %\begin{convention}% Let [S1], [S2] and [S3] be setoids.
112 Section CombiningOperations
116 cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S1.var
120 cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S2.var
124 cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S3.var
128 In the following definition, we assume [f] is a setoid function from
129 [S1] to [S2], and [op] is an unary operation on [S2].
130 Then [opOnFun] is the composition [op] after [f].
134 Section CombiningUnaryOperations
138 cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/f.var
142 cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/op.var
145 inline procedural "cic:/CoRN/algebra/CSetoidFun/opOnFun.con" as definition.
148 End CombiningUnaryOperations
152 End CombiningOperations
155 (*#* **Partial Functions
157 In this section we define a concept of partial function for an
158 arbitrary setoid. Essentially, a partial function is what would be
159 expected---a predicate on the setoid in question and a total function
160 from the set of points satisfying that predicate to the setoid. There
161 is one important limitations to this approach: first, the record we
162 obtain has type [Type], meaning that we can't use, for instance,
163 elimination of existential quantifiers.
165 Furthermore, for reasons we will explain ahead, partial functions will
166 not be defined via the [CSetoid_fun] record, but the whole structure
167 will be incorporated in a new record.
169 Finally, notice that to be completely general the domains of the
170 functions have to be characterized by a [CProp]-valued predicate;
171 otherwise, the use you can make of a function will be %\emph{%#<i>#a
172 priori#</i>#%}% restricted at the moment it is defined.
174 Before we state our definitions we need to do some work on domains.
181 (*#* ***Subsets of Setoids
183 Subsets of a setoid will be identified with predicates from the
184 carrier set of the setoid into [CProp]. At this stage, we do not make
185 any assumptions about these predicates.
187 We will begin by defining elementary operations on predicates, along
188 with their basic properties. In particular, we will work with well
189 defined predicates, so we will prove that these operations preserve
192 %\begin{convention}% Let [S:CSetoid] and [P,Q:S->CProp].
197 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/S.var
205 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/P.var
209 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/Q.var
212 inline procedural "cic:/CoRN/algebra/CSetoidFun/conjP.con" as definition.
214 inline procedural "cic:/CoRN/algebra/CSetoidFun/prj1.con" as lemma.
216 inline procedural "cic:/CoRN/algebra/CSetoidFun/prj2.con" as lemma.
218 inline procedural "cic:/CoRN/algebra/CSetoidFun/conj_wd.con" as lemma.
229 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/P.var
233 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/Q.var
237 Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets).
240 inline procedural "cic:/CoRN/algebra/CSetoidFun/disj.con" as definition.
242 inline procedural "cic:/CoRN/algebra/CSetoidFun/inj1.con" as lemma.
244 inline procedural "cic:/CoRN/algebra/CSetoidFun/inj2.con" as lemma.
246 inline procedural "cic:/CoRN/algebra/CSetoidFun/disj_wd.con" as lemma.
257 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].
261 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/P.var
265 cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/R.var
268 inline procedural "cic:/CoRN/algebra/CSetoidFun/extend.con" as definition.
270 inline procedural "cic:/CoRN/algebra/CSetoidFun/ext1.con" as lemma.
272 inline procedural "cic:/CoRN/algebra/CSetoidFun/ext2_a.con" as lemma.
274 inline procedural "cic:/CoRN/algebra/CSetoidFun/ext2.con" as lemma.
276 inline procedural "cic:/CoRN/algebra/CSetoidFun/extension_wd.con" as lemma.
287 Notation Conj := (conjP _).
291 Implicit Arguments disj [S].
295 Implicit Arguments extend [S].
299 Implicit Arguments ext1 [S P R x].
303 Implicit Arguments ext2 [S P R x].
308 We are now ready to define the concept of partial function between arbitrary setoids.
311 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPartFunct.ind".
314 cic:/matita/CoRN-Procedural/algebra/CSetoidFun/bpfpfun.con
318 Notation BDom := (bpfdom _ _).
322 Implicit Arguments bpfpfun [S1 S2].
326 The next lemma states that every partial function is well defined.
329 inline procedural "cic:/CoRN/algebra/CSetoidFun/bpfwdef.con" as lemma.
331 (*#* Similar for automorphisms. *)
333 inline procedural "cic:/CoRN/algebra/CSetoidFun/PartFunct.ind".
336 cic:/matita/CoRN-Procedural/algebra/CSetoidFun/pfpfun.con
340 Notation Dom := (pfdom _).
344 Notation Part := (pfpfun _).
348 Implicit Arguments pfpfun [S].
352 The next lemma states that every partial function is well defined.
355 inline procedural "cic:/CoRN/algebra/CSetoidFun/pfwdef.con" as lemma.
358 A few characteristics of this definition should be explained:
359 - The domain of the partial function is characterized by a predicate
360 that is required to be well defined but not strongly extensional. The
361 motivation for this choice comes from two facts: first, one very
362 important subset of real numbers is the compact interval
363 [[a,b]]---characterized by the predicate [ fun x : IR => a [<=] x /\ x
364 [<=] b], which is not strongly extensional; on the other hand, if we
365 can apply a function to an element [s] of a setoid [S] it seems
366 reasonable (and at some point we do have to do it) to apply that same
367 function to any element [s'] which is equal to [s] from the point of
368 view of the setoid equality.
369 - The last two conditions state that [pfpfun] is really a subsetoid
370 function. The reason why we do not write it that way is the
371 following: when applying a partial function [f] to an element [s] of
372 [S] we also need a proof object [H]; with this definition the object
373 we get is [f(s,H)], where the proof is kept separate from the object.
374 Using subsetoid notation, we would get $f(\langle
375 s,H\rangle)$#f(⟨s,H⟩)#; from this we need to apply two
376 projections to get either the original object or the proof, and we
377 need to apply an extra constructor to get $f(\langle
378 s,H\rangle)$#f(⟨s,H⟩)# from [s] and [H]. This amounts
379 to spending more resources when actually working with these objects.
380 - This record has type [Type], which is very unfortunate, because it
381 means in particular that we cannot use the well behaved set
382 existential quantification over partial functions; however, later on
383 we will manage to avoid this problem in a way that also justifies that
384 we don't really need to use that kind of quantification. Another
385 approach to this definition that completely avoid this complication
386 would be to make [PartFunct] a dependent type, receiving the predicate
387 as an argument. This does work in that it allows us to give
388 [PartFunct] type [Set] and do some useful stuff with it; however, we
389 are not able to define something as simple as an operator that gets a
390 function and returns its domain (because of the restrictions in the
391 type elimination rules). This sounds very unnatural, and soon gets us
392 into strange problems that yield very unlikely definitions, which is
393 why we chose to altogether do away with this approach.
395 %\begin{convention}% All partial functions will henceforth be denoted by capital letters.
398 We now present some methods for defining partial functions.
402 Hint Resolve CI: core.
410 cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/S.var
414 To begin with, we want to be able to ``see'' each total function as a partial function.
417 inline procedural "cic:/CoRN/algebra/CSetoidFun/total_eq_part.con" as definition.
420 Section Part_Function_Const
424 In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:
426 %\begin{convention}% Let [c:S].
431 cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Const/c.var
434 inline procedural "cic:/CoRN/algebra/CSetoidFun/Fconst.con" as definition.
437 End Part_Function_Const
441 Section Part_Function_Id
444 inline procedural "cic:/CoRN/algebra/CSetoidFun/Fid.con" as definition.
451 (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.)
453 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.
455 %\begin{convention}% Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing their domains.
460 Section Part_Function_Composition
464 cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/G.var
468 cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/F.var
473 inline procedural "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/P.con" "CSetoid_Ops__Part_Function_Composition__" as definition.
475 inline procedural "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/Q.con" "CSetoid_Ops__Part_Function_Composition__" as definition.
479 inline procedural "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/R.con" "CSetoid_Ops__Part_Function_Composition__" as definition.
481 inline procedural "cic:/CoRN/algebra/CSetoidFun/part_function_comp_strext.con" as lemma.
483 inline procedural "cic:/CoRN/algebra/CSetoidFun/part_function_comp_dom_wd.con" as lemma.
485 inline procedural "cic:/CoRN/algebra/CSetoidFun/Fcomp.con" as definition.
488 End Part_Function_Composition
496 %\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains.
501 Section BinPart_Function_Composition
505 cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S1.var
509 cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S2.var
513 cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S3.var
517 cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/G.var
521 cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/F.var
526 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/P.con" "BinPart_Function_Composition__" as definition.
528 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/Q.con" "BinPart_Function_Composition__" as definition.
532 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/R.con" "BinPart_Function_Composition__" as definition.
534 inline procedural "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_strext.con" as lemma.
536 inline procedural "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_dom_wd.con" as lemma.
538 inline procedural "cic:/CoRN/algebra/CSetoidFun/BinFcomp.con" as definition.
541 End BinPart_Function_Composition
544 (* Different tokens for compatibility with coqdoc *)
547 Implicit Arguments Fconst [S].
551 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
555 Notation FId := (Fid _).
559 Implicit Arguments Fcomp [S].
563 Infix "[o]" := Fcomp (at level 65, no associativity).
567 Hint Resolve pfwdef bpfwdef: algebra.
576 inline procedural "cic:/CoRN/algebra/CSetoidFun/injective.con" as definition.
578 inline procedural "cic:/CoRN/algebra/CSetoidFun/injective_weak.con" as definition.
580 inline procedural "cic:/CoRN/algebra/CSetoidFun/surjective.con" as definition.
583 Implicit Arguments injective [A B].
587 Implicit Arguments injective_weak [A B].
591 Implicit Arguments surjective [A B].
594 inline procedural "cic:/CoRN/algebra/CSetoidFun/injective_imp_injective_weak.con" as lemma.
596 inline procedural "cic:/CoRN/algebra/CSetoidFun/bijective.con" as definition.
599 Implicit Arguments bijective [A B].
602 inline procedural "cic:/CoRN/algebra/CSetoidFun/id_is_bij.con" as lemma.
604 inline procedural "cic:/CoRN/algebra/CSetoidFun/comp_resp_bij.con" as lemma.
606 inline procedural "cic:/CoRN/algebra/CSetoidFun/inv.con" as lemma.
609 Implicit Arguments inv [A B].
612 inline procedural "cic:/CoRN/algebra/CSetoidFun/invfun.con" as definition.
615 Implicit Arguments invfun [A B].
618 inline procedural "cic:/CoRN/algebra/CSetoidFun/inv1.con" as lemma.
620 inline procedural "cic:/CoRN/algebra/CSetoidFun/inv2.con" as lemma.
622 inline procedural "cic:/CoRN/algebra/CSetoidFun/inv_strext.con" as lemma.
624 inline procedural "cic:/CoRN/algebra/CSetoidFun/Inv.con" as definition.
627 Implicit Arguments Inv [A B].
630 inline procedural "cic:/CoRN/algebra/CSetoidFun/Inv_bij.con" as definition.
637 Implicit Arguments bijective [A B].
641 Implicit Arguments injective [A B].
645 Implicit Arguments injective_weak [A B].
649 Implicit Arguments surjective [A B].
653 Implicit Arguments inv [A B].
657 Implicit Arguments invfun [A B].
661 Implicit Arguments Inv [A B].
665 Implicit Arguments conj_wd [S P Q].
669 Notation Prj1 := (prj1 _ _ _ _).
673 Notation Prj2 := (prj2 _ _ _ _).