(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) (* This file was automatically generated: do not edit *********************) include "CoRN.ma". (* $Id: CSetoidFun.v,v 1.10 2004/04/23 10:00:53 lcf Exp $ *) include "algebra/CSetoids.ma". (* UNEXPORTED Section unary_function_composition *) (*#* ** Composition of Setoid functions Let [S1], [S2] and [S3] be setoids, [f] a setoid function from [S1] to [S2], and [g] from [S2] to [S3] in the following definition of composition. *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S1.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S2.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S3.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/unary_function_composition/f.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/unary_function_composition/g.var *) inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_fun.con" as definition. (* UNEXPORTED End unary_function_composition *) (* UNEXPORTED Section unary_and_binary_function_composition *) inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_un_fun.con" as definition. inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_fun.con" as definition. inline procedural "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_un_bin_fun.con" as definition. (* UNEXPORTED End unary_and_binary_function_composition *) (*#* ***Projections *) (* UNEXPORTED Section function_projection *) inline procedural "cic:/CoRN/algebra/CSetoidFun/proj_bin_fun.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/projected_bin_fun.con" as definition. (* UNEXPORTED End function_projection *) (* UNEXPORTED Section BinProj *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/BinProj/S.var *) inline procedural "cic:/CoRN/algebra/CSetoidFun/binproj1.con" as definition. inline procedural "cic:/CoRN/algebra/CSetoidFun/binproj1_strext.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/cs_binproj1.con" as definition. (* UNEXPORTED End BinProj *) (*#* **Combining operations %\begin{convention}% Let [S1], [S2] and [S3] be setoids. %\end{convention}% *) (* UNEXPORTED Section CombiningOperations *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S1.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S2.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S3.var *) (*#* In the following definition, we assume [f] is a setoid function from [S1] to [S2], and [op] is an unary operation on [S2]. Then [opOnFun] is the composition [op] after [f]. *) (* UNEXPORTED Section CombiningUnaryOperations *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/f.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/op.var *) inline procedural "cic:/CoRN/algebra/CSetoidFun/opOnFun.con" as definition. (* UNEXPORTED End CombiningUnaryOperations *) (* UNEXPORTED End CombiningOperations *) (*#* **Partial Functions In this section we define a concept of partial function for an arbitrary setoid. Essentially, a partial function is what would be expected---a predicate on the setoid in question and a total function from the set of points satisfying that predicate to the setoid. There is one important limitations to this approach: first, the record we obtain has type [Type], meaning that we can't use, for instance, elimination of existential quantifiers. Furthermore, for reasons we will explain ahead, partial functions will not be defined via the [CSetoid_fun] record, but the whole structure will be incorporated in a new record. Finally, notice that to be completely general the domains of the functions have to be characterized by a [CProp]-valued predicate; otherwise, the use you can make of a function will be %\emph{%##a priori##%}% restricted at the moment it is defined. Before we state our definitions we need to do some work on domains. *) (* UNEXPORTED Section SubSets_of_G *) (*#* ***Subsets of Setoids Subsets of a setoid will be identified with predicates from the carrier set of the setoid into [CProp]. At this stage, we do not make any assumptions about these predicates. We will begin by defining elementary operations on predicates, along with their basic properties. In particular, we will work with well defined predicates, so we will prove that these operations preserve welldefinedness. %\begin{convention}% Let [S:CSetoid] and [P,Q:S->CProp]. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/S.var *) (* UNEXPORTED Section Conjunction *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/P.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/Q.var *) inline procedural "cic:/CoRN/algebra/CSetoidFun/conjP.con" as definition. inline procedural "cic:/CoRN/algebra/CSetoidFun/prj1.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/prj2.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/conj_wd.con" as lemma. (* UNEXPORTED End Conjunction *) (* UNEXPORTED Section Disjunction *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/P.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/Q.var *) (*#* Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets). *) inline procedural "cic:/CoRN/algebra/CSetoidFun/disj.con" as definition. inline procedural "cic:/CoRN/algebra/CSetoidFun/inj1.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/inj2.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/disj_wd.con" as lemma. (* UNEXPORTED End Disjunction *) (* UNEXPORTED Section Extension *) (*#* 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]. *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/P.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/R.var *) inline procedural "cic:/CoRN/algebra/CSetoidFun/extend.con" as definition. inline procedural "cic:/CoRN/algebra/CSetoidFun/ext1.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/ext2_a.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/ext2.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/extension_wd.con" as lemma. (* UNEXPORTED End Extension *) (* UNEXPORTED End SubSets_of_G *) (* NOTATION Notation Conj := (conjP _). *) (* UNEXPORTED Implicit Arguments disj [S]. *) (* UNEXPORTED Implicit Arguments extend [S]. *) (* UNEXPORTED Implicit Arguments ext1 [S P R x]. *) (* UNEXPORTED Implicit Arguments ext2 [S P R x]. *) (*#* ***Operations We are now ready to define the concept of partial function between arbitrary setoids. *) inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPartFunct.ind". (* COERCION cic:/matita/CoRN-Procedural/algebra/CSetoidFun/bpfpfun.con *) (* NOTATION Notation BDom := (bpfdom _ _). *) (* UNEXPORTED Implicit Arguments bpfpfun [S1 S2]. *) (*#* The next lemma states that every partial function is well defined. *) inline procedural "cic:/CoRN/algebra/CSetoidFun/bpfwdef.con" as lemma. (*#* Similar for automorphisms. *) inline procedural "cic:/CoRN/algebra/CSetoidFun/PartFunct.ind". (* COERCION cic:/matita/CoRN-Procedural/algebra/CSetoidFun/pfpfun.con *) (* NOTATION Notation Dom := (pfdom _). *) (* NOTATION Notation Part := (pfpfun _). *) (* UNEXPORTED Implicit Arguments pfpfun [S]. *) (*#* The next lemma states that every partial function is well defined. *) inline procedural "cic:/CoRN/algebra/CSetoidFun/pfwdef.con" as lemma. (*#* A few characteristics of this definition should be explained: - The domain of the partial function is characterized by a predicate that is required to be well defined but not strongly extensional. The motivation for this choice comes from two facts: first, one very important subset of real numbers is the compact interval [[a,b]]---characterized by the predicate [ fun x : IR => a [<=] x /\ x [<=] b], which is not strongly extensional; on the other hand, if we can apply a function to an element [s] of a setoid [S] it seems reasonable (and at some point we do have to do it) to apply that same function to any element [s'] which is equal to [s] from the point of view of the setoid equality. - The last two conditions state that [pfpfun] is really a subsetoid function. The reason why we do not write it that way is the following: when applying a partial function [f] to an element [s] of [S] we also need a proof object [H]; with this definition the object we get is [f(s,H)], where the proof is kept separate from the object. Using subsetoid notation, we would get $f(\langle s,H\rangle)$#f(⟨s,H⟩)#; from this we need to apply two projections to get either the original object or the proof, and we need to apply an extra constructor to get $f(\langle s,H\rangle)$#f(⟨s,H⟩)# from [s] and [H]. This amounts to spending more resources when actually working with these objects. - This record has type [Type], which is very unfortunate, because it means in particular that we cannot use the well behaved set existential quantification over partial functions; however, later on we will manage to avoid this problem in a way that also justifies that we don't really need to use that kind of quantification. Another approach to this definition that completely avoid this complication would be to make [PartFunct] a dependent type, receiving the predicate as an argument. This does work in that it allows us to give [PartFunct] type [Set] and do some useful stuff with it; however, we are not able to define something as simple as an operator that gets a function and returns its domain (because of the restrictions in the type elimination rules). This sounds very unnatural, and soon gets us into strange problems that yield very unlikely definitions, which is why we chose to altogether do away with this approach. %\begin{convention}% All partial functions will henceforth be denoted by capital letters. %\end{convention}% We now present some methods for defining partial functions. *) (* UNEXPORTED Hint Resolve CI: core. *) (* UNEXPORTED Section CSetoid_Ops *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/S.var *) (*#* To begin with, we want to be able to ``see'' each total function as a partial function. *) inline procedural "cic:/CoRN/algebra/CSetoidFun/total_eq_part.con" as definition. (* UNEXPORTED Section Part_Function_Const *) (*#* In any setoid we can also define constant functions (one for each element of the setoid) and an identity function: %\begin{convention}% Let [c:S]. %\end{convention}% *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Const/c.var *) inline procedural "cic:/CoRN/algebra/CSetoidFun/Fconst.con" as definition. (* UNEXPORTED End Part_Function_Const *) (* UNEXPORTED Section Part_Function_Id *) inline procedural "cic:/CoRN/algebra/CSetoidFun/Fid.con" as definition. (* UNEXPORTED End Part_Function_Id *) (*#* (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.) 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. %\begin{convention}% Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing their domains. %\end{convention}% *) (* UNEXPORTED Section Part_Function_Composition *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/G.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/F.var *) (* begin hide *) inline procedural "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/P.con" "CSetoid_Ops__Part_Function_Composition__" as definition. inline procedural "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/Q.con" "CSetoid_Ops__Part_Function_Composition__" as definition. (* end hide *) inline procedural "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/R.con" "CSetoid_Ops__Part_Function_Composition__" as definition. inline procedural "cic:/CoRN/algebra/CSetoidFun/part_function_comp_strext.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/part_function_comp_dom_wd.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/Fcomp.con" as definition. (* UNEXPORTED End Part_Function_Composition *) (* UNEXPORTED End CSetoid_Ops *) (*#* %\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains. %\end{convention}% *) (* UNEXPORTED Section BinPart_Function_Composition *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S1.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S2.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S3.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/G.var *) (* UNEXPORTED cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/F.var *) (* begin hide *) inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/P.con" "BinPart_Function_Composition__" as definition. inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/Q.con" "BinPart_Function_Composition__" as definition. (* end hide *) inline procedural "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/R.con" "BinPart_Function_Composition__" as definition. inline procedural "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_strext.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_dom_wd.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/BinFcomp.con" as definition. (* UNEXPORTED End BinPart_Function_Composition *) (* Different tokens for compatibility with coqdoc *) (* UNEXPORTED Implicit Arguments Fconst [S]. *) (* NOTATION Notation "[-C-] x" := (Fconst x) (at level 2, right associativity). *) (* NOTATION Notation FId := (Fid _). *) (* UNEXPORTED Implicit Arguments Fcomp [S]. *) (* NOTATION Infix "[o]" := Fcomp (at level 65, no associativity). *) (* UNEXPORTED Hint Resolve pfwdef bpfwdef: algebra. *) (* UNEXPORTED Section bijections *) (*#* **Bijections *) inline procedural "cic:/CoRN/algebra/CSetoidFun/injective.con" as definition. inline procedural "cic:/CoRN/algebra/CSetoidFun/injective_weak.con" as definition. inline procedural "cic:/CoRN/algebra/CSetoidFun/surjective.con" as definition. (* UNEXPORTED Implicit Arguments injective [A B]. *) (* UNEXPORTED Implicit Arguments injective_weak [A B]. *) (* UNEXPORTED Implicit Arguments surjective [A B]. *) inline procedural "cic:/CoRN/algebra/CSetoidFun/injective_imp_injective_weak.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/bijective.con" as definition. (* UNEXPORTED Implicit Arguments bijective [A B]. *) inline procedural "cic:/CoRN/algebra/CSetoidFun/id_is_bij.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/comp_resp_bij.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/inv.con" as lemma. (* UNEXPORTED Implicit Arguments inv [A B]. *) inline procedural "cic:/CoRN/algebra/CSetoidFun/invfun.con" as definition. (* UNEXPORTED Implicit Arguments invfun [A B]. *) inline procedural "cic:/CoRN/algebra/CSetoidFun/inv1.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/inv2.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/inv_strext.con" as lemma. inline procedural "cic:/CoRN/algebra/CSetoidFun/Inv.con" as definition. (* UNEXPORTED Implicit Arguments Inv [A B]. *) inline procedural "cic:/CoRN/algebra/CSetoidFun/Inv_bij.con" as definition. (* UNEXPORTED End bijections *) (* UNEXPORTED Implicit Arguments bijective [A B]. *) (* UNEXPORTED Implicit Arguments injective [A B]. *) (* UNEXPORTED Implicit Arguments injective_weak [A B]. *) (* UNEXPORTED Implicit Arguments surjective [A B]. *) (* UNEXPORTED Implicit Arguments inv [A B]. *) (* UNEXPORTED Implicit Arguments invfun [A B]. *) (* UNEXPORTED Implicit Arguments Inv [A B]. *) (* UNEXPORTED Implicit Arguments conj_wd [S P Q]. *) (* NOTATION Notation Prj1 := (prj1 _ _ _ _). *) (* NOTATION Notation Prj2 := (prj2 _ _ _ _). *)