X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCSetoidFun.ma;h=84c0c6c2672ff96e60d89d466bc47751685cb408;hb=52206fa1c090fcdc8386ec8d7e88beca089c7e39;hp=d183c70e8b8288e12e228fc1759aa74a636f2e3b;hpb=0e0d5c57eb154bf20d101f09e560401434156c1d;p=helm.git diff --git a/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma b/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma index d183c70e8..84c0c6c26 100644 --- a/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma +++ b/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma @@ -16,11 +16,11 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSetoidFun". +include "CoRN.ma". + (* $Id: CSetoidFun.v,v 1.10 2004/04/23 10:00:53 lcf Exp $ *) -(* INCLUDE -CSetoids -*) +include "algebra/CSetoids.ma". (* UNEXPORTED Section unary_function_composition. @@ -32,17 +32,17 @@ 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. *) -inline cic:/CoRN/algebra/CSetoidFun/S1.var. +inline "cic:/CoRN/algebra/CSetoidFun/S1.var". -inline cic:/CoRN/algebra/CSetoidFun/S2.var. +inline "cic:/CoRN/algebra/CSetoidFun/S2.var". -inline cic:/CoRN/algebra/CSetoidFun/S3.var. +inline "cic:/CoRN/algebra/CSetoidFun/S3.var". -inline cic:/CoRN/algebra/CSetoidFun/f.var. +inline "cic:/CoRN/algebra/CSetoidFun/f.var". -inline cic:/CoRN/algebra/CSetoidFun/g.var. +inline "cic:/CoRN/algebra/CSetoidFun/g.var". -inline cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_fun.con. +inline "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_fun.con". (* UNEXPORTED End unary_function_composition. @@ -52,11 +52,11 @@ End unary_function_composition. Section unary_and_binary_function_composition. *) -inline cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_un_fun.con. +inline "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_un_fun.con". -inline cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_fun.con. +inline "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_fun.con". -inline cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_un_bin_fun.con. +inline "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_un_bin_fun.con". (* UNEXPORTED End unary_and_binary_function_composition. @@ -69,9 +69,9 @@ End unary_and_binary_function_composition. Section function_projection. *) -inline cic:/CoRN/algebra/CSetoidFun/proj_bin_fun.con. +inline "cic:/CoRN/algebra/CSetoidFun/proj_bin_fun.con". -inline cic:/CoRN/algebra/CSetoidFun/projected_bin_fun.con. +inline "cic:/CoRN/algebra/CSetoidFun/projected_bin_fun.con". (* UNEXPORTED End function_projection. @@ -81,13 +81,13 @@ End function_projection. Section BinProj. *) -inline cic:/CoRN/algebra/CSetoidFun/S.var. +inline "cic:/CoRN/algebra/CSetoidFun/S.var". -inline cic:/CoRN/algebra/CSetoidFun/binproj1.con. +inline "cic:/CoRN/algebra/CSetoidFun/binproj1.con". -inline cic:/CoRN/algebra/CSetoidFun/binproj1_strext.con. +inline "cic:/CoRN/algebra/CSetoidFun/binproj1_strext.con". -inline cic:/CoRN/algebra/CSetoidFun/cs_binproj1.con. +inline "cic:/CoRN/algebra/CSetoidFun/cs_binproj1.con". (* UNEXPORTED End BinProj. @@ -102,11 +102,11 @@ End BinProj. Section CombiningOperations. *) -inline cic:/CoRN/algebra/CSetoidFun/S1.var. +inline "cic:/CoRN/algebra/CSetoidFun/S1.var". -inline cic:/CoRN/algebra/CSetoidFun/S2.var. +inline "cic:/CoRN/algebra/CSetoidFun/S2.var". -inline cic:/CoRN/algebra/CSetoidFun/S3.var. +inline "cic:/CoRN/algebra/CSetoidFun/S3.var". (*#* In the following definition, we assume [f] is a setoid function from @@ -118,11 +118,11 @@ Then [opOnFun] is the composition [op] after [f]. Section CombiningUnaryOperations. *) -inline cic:/CoRN/algebra/CSetoidFun/f.var. +inline "cic:/CoRN/algebra/CSetoidFun/f.var". -inline cic:/CoRN/algebra/CSetoidFun/op.var. +inline "cic:/CoRN/algebra/CSetoidFun/op.var". -inline cic:/CoRN/algebra/CSetoidFun/opOnFun.con. +inline "cic:/CoRN/algebra/CSetoidFun/opOnFun.con". (* UNEXPORTED End CombiningUnaryOperations. @@ -173,23 +173,23 @@ welldefinedness. %\end{convention}% *) -inline cic:/CoRN/algebra/CSetoidFun/S.var. +inline "cic:/CoRN/algebra/CSetoidFun/S.var". (* UNEXPORTED Section Conjunction. *) -inline cic:/CoRN/algebra/CSetoidFun/P.var. +inline "cic:/CoRN/algebra/CSetoidFun/P.var". -inline cic:/CoRN/algebra/CSetoidFun/Q.var. +inline "cic:/CoRN/algebra/CSetoidFun/Q.var". -inline cic:/CoRN/algebra/CSetoidFun/conjP.con. +inline "cic:/CoRN/algebra/CSetoidFun/conjP.con". -inline cic:/CoRN/algebra/CSetoidFun/prj1.con. +inline "cic:/CoRN/algebra/CSetoidFun/prj1.con". -inline cic:/CoRN/algebra/CSetoidFun/prj2.con. +inline "cic:/CoRN/algebra/CSetoidFun/prj2.con". -inline cic:/CoRN/algebra/CSetoidFun/conj_wd.con. +inline "cic:/CoRN/algebra/CSetoidFun/conj_wd.con". (* UNEXPORTED End Conjunction. @@ -199,21 +199,21 @@ End Conjunction. Section Disjunction. *) -inline cic:/CoRN/algebra/CSetoidFun/P.var. +inline "cic:/CoRN/algebra/CSetoidFun/P.var". -inline cic:/CoRN/algebra/CSetoidFun/Q.var. +inline "cic:/CoRN/algebra/CSetoidFun/Q.var". (*#* Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets). *) -inline cic:/CoRN/algebra/CSetoidFun/disj.con. +inline "cic:/CoRN/algebra/CSetoidFun/disj.con". -inline cic:/CoRN/algebra/CSetoidFun/inj1.con. +inline "cic:/CoRN/algebra/CSetoidFun/inj1.con". -inline cic:/CoRN/algebra/CSetoidFun/inj2.con. +inline "cic:/CoRN/algebra/CSetoidFun/inj2.con". -inline cic:/CoRN/algebra/CSetoidFun/disj_wd.con. +inline "cic:/CoRN/algebra/CSetoidFun/disj_wd.con". (* UNEXPORTED End Disjunction. @@ -227,19 +227,19 @@ 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]. *) -inline cic:/CoRN/algebra/CSetoidFun/P.var. +inline "cic:/CoRN/algebra/CSetoidFun/P.var". -inline cic:/CoRN/algebra/CSetoidFun/R.var. +inline "cic:/CoRN/algebra/CSetoidFun/R.var". -inline cic:/CoRN/algebra/CSetoidFun/extend.con. +inline "cic:/CoRN/algebra/CSetoidFun/extend.con". -inline cic:/CoRN/algebra/CSetoidFun/ext1.con. +inline "cic:/CoRN/algebra/CSetoidFun/ext1.con". -inline cic:/CoRN/algebra/CSetoidFun/ext2_a.con. +inline "cic:/CoRN/algebra/CSetoidFun/ext2_a.con". -inline cic:/CoRN/algebra/CSetoidFun/ext2.con. +inline "cic:/CoRN/algebra/CSetoidFun/ext2.con". -inline cic:/CoRN/algebra/CSetoidFun/extension_wd.con. +inline "cic:/CoRN/algebra/CSetoidFun/extension_wd.con". (* UNEXPORTED End Extension. @@ -249,6 +249,10 @@ End Extension. End SubSets_of_G. *) +(* NOTATION +Notation Conj := (conjP _). +*) + (* UNEXPORTED Implicit Arguments disj [S]. *) @@ -270,7 +274,13 @@ Implicit Arguments ext2 [S P R x]. We are now ready to define the concept of partial function between arbitrary setoids. *) -inline cic:/CoRN/algebra/CSetoidFun/BinPartFunct.ind. +inline "cic:/CoRN/algebra/CSetoidFun/BinPartFunct.ind". + +coercion cic:/matita/CoRN-Decl/algebra/CSetoidFun/bpfpfun.con 0 (* compounds *). + +(* NOTATION +Notation BDom := (bpfdom _ _). +*) (* UNEXPORTED Implicit Arguments bpfpfun [S1 S2]. @@ -280,11 +290,21 @@ Implicit Arguments bpfpfun [S1 S2]. The next lemma states that every partial function is well defined. *) -inline cic:/CoRN/algebra/CSetoidFun/bpfwdef.con. +inline "cic:/CoRN/algebra/CSetoidFun/bpfwdef.con". (*#* Similar for automorphisms. *) -inline cic:/CoRN/algebra/CSetoidFun/PartFunct.ind. +inline "cic:/CoRN/algebra/CSetoidFun/PartFunct.ind". + +coercion cic:/matita/CoRN-Decl/algebra/CSetoidFun/pfpfun.con 0 (* compounds *). + +(* NOTATION +Notation Dom := (pfdom _). +*) + +(* NOTATION +Notation Part := (pfpfun _). +*) (* UNEXPORTED Implicit Arguments pfpfun [S]. @@ -294,7 +314,7 @@ Implicit Arguments pfpfun [S]. The next lemma states that every partial function is well defined. *) -inline cic:/CoRN/algebra/CSetoidFun/pfwdef.con. +inline "cic:/CoRN/algebra/CSetoidFun/pfwdef.con". (*#* A few characteristics of this definition should be explained: @@ -348,13 +368,13 @@ Hint Resolve CI: core. Section CSetoid_Ops. *) -inline cic:/CoRN/algebra/CSetoidFun/S.var. +inline "cic:/CoRN/algebra/CSetoidFun/S.var". (*#* To begin with, we want to be able to ``see'' each total function as a partial function. *) -inline cic:/CoRN/algebra/CSetoidFun/total_eq_part.con. +inline "cic:/CoRN/algebra/CSetoidFun/total_eq_part.con". (* UNEXPORTED Section Part_Function_Const. @@ -367,9 +387,9 @@ In any setoid we can also define constant functions (one for each element of the %\end{convention}% *) -inline cic:/CoRN/algebra/CSetoidFun/c.var. +inline "cic:/CoRN/algebra/CSetoidFun/c.var". -inline cic:/CoRN/algebra/CSetoidFun/Fconst.con. +inline "cic:/CoRN/algebra/CSetoidFun/Fconst.con". (* UNEXPORTED End Part_Function_Const. @@ -379,7 +399,7 @@ End Part_Function_Const. Section Part_Function_Id. *) -inline cic:/CoRN/algebra/CSetoidFun/Fid.con. +inline "cic:/CoRN/algebra/CSetoidFun/Fid.con". (* UNEXPORTED End Part_Function_Id. @@ -398,25 +418,25 @@ If we have two setoid functions [F] and [G] we can always compose them. The dom Section Part_Function_Composition. *) -inline cic:/CoRN/algebra/CSetoidFun/G.var. +inline "cic:/CoRN/algebra/CSetoidFun/G.var". -inline cic:/CoRN/algebra/CSetoidFun/F.var. +inline "cic:/CoRN/algebra/CSetoidFun/F.var". (* begin hide *) -inline cic:/CoRN/algebra/CSetoidFun/P.con. +inline "cic:/CoRN/algebra/CSetoidFun/P.con". -inline cic:/CoRN/algebra/CSetoidFun/Q.con. +inline "cic:/CoRN/algebra/CSetoidFun/Q.con". (* end hide *) -inline cic:/CoRN/algebra/CSetoidFun/R.con. +inline "cic:/CoRN/algebra/CSetoidFun/R.con". -inline cic:/CoRN/algebra/CSetoidFun/part_function_comp_strext.con. +inline "cic:/CoRN/algebra/CSetoidFun/part_function_comp_strext.con". -inline cic:/CoRN/algebra/CSetoidFun/part_function_comp_dom_wd.con. +inline "cic:/CoRN/algebra/CSetoidFun/part_function_comp_dom_wd.con". -inline cic:/CoRN/algebra/CSetoidFun/Fcomp.con. +inline "cic:/CoRN/algebra/CSetoidFun/Fcomp.con". (* UNEXPORTED End Part_Function_Composition. @@ -435,31 +455,31 @@ End CSetoid_Ops. Section BinPart_Function_Composition. *) -inline cic:/CoRN/algebra/CSetoidFun/S1.var. +inline "cic:/CoRN/algebra/CSetoidFun/S1.var". -inline cic:/CoRN/algebra/CSetoidFun/S2.var. +inline "cic:/CoRN/algebra/CSetoidFun/S2.var". -inline cic:/CoRN/algebra/CSetoidFun/S3.var. +inline "cic:/CoRN/algebra/CSetoidFun/S3.var". -inline cic:/CoRN/algebra/CSetoidFun/G.var. +inline "cic:/CoRN/algebra/CSetoidFun/G.var". -inline cic:/CoRN/algebra/CSetoidFun/F.var. +inline "cic:/CoRN/algebra/CSetoidFun/F.var". (* begin hide *) -inline cic:/CoRN/algebra/CSetoidFun/P.con. +inline "cic:/CoRN/algebra/CSetoidFun/P.con". -inline cic:/CoRN/algebra/CSetoidFun/Q.con. +inline "cic:/CoRN/algebra/CSetoidFun/Q.con". (* end hide *) -inline cic:/CoRN/algebra/CSetoidFun/R.con. +inline "cic:/CoRN/algebra/CSetoidFun/R.con". -inline cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_strext.con. +inline "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_strext.con". -inline cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_dom_wd.con. +inline "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_dom_wd.con". -inline cic:/CoRN/algebra/CSetoidFun/BinFcomp.con. +inline "cic:/CoRN/algebra/CSetoidFun/BinFcomp.con". (* UNEXPORTED End BinPart_Function_Composition. @@ -471,10 +491,22 @@ End BinPart_Function_Composition. 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. *) @@ -485,11 +517,11 @@ Section bijections. (*#* **Bijections *) -inline cic:/CoRN/algebra/CSetoidFun/injective.con. +inline "cic:/CoRN/algebra/CSetoidFun/injective.con". -inline cic:/CoRN/algebra/CSetoidFun/injective_weak.con. +inline "cic:/CoRN/algebra/CSetoidFun/injective_weak.con". -inline cic:/CoRN/algebra/CSetoidFun/surjective.con. +inline "cic:/CoRN/algebra/CSetoidFun/surjective.con". (* UNEXPORTED Implicit Arguments injective [A B]. @@ -503,43 +535,43 @@ Implicit Arguments injective_weak [A B]. Implicit Arguments surjective [A B]. *) -inline cic:/CoRN/algebra/CSetoidFun/injective_imp_injective_weak.con. +inline "cic:/CoRN/algebra/CSetoidFun/injective_imp_injective_weak.con". -inline cic:/CoRN/algebra/CSetoidFun/bijective.con. +inline "cic:/CoRN/algebra/CSetoidFun/bijective.con". (* UNEXPORTED Implicit Arguments bijective [A B]. *) -inline cic:/CoRN/algebra/CSetoidFun/id_is_bij.con. +inline "cic:/CoRN/algebra/CSetoidFun/id_is_bij.con". -inline cic:/CoRN/algebra/CSetoidFun/comp_resp_bij.con. +inline "cic:/CoRN/algebra/CSetoidFun/comp_resp_bij.con". -inline cic:/CoRN/algebra/CSetoidFun/inv.con. +inline "cic:/CoRN/algebra/CSetoidFun/inv.con". (* UNEXPORTED Implicit Arguments inv [A B]. *) -inline cic:/CoRN/algebra/CSetoidFun/invfun.con. +inline "cic:/CoRN/algebra/CSetoidFun/invfun.con". (* UNEXPORTED Implicit Arguments invfun [A B]. *) -inline cic:/CoRN/algebra/CSetoidFun/inv1.con. +inline "cic:/CoRN/algebra/CSetoidFun/inv1.con". -inline cic:/CoRN/algebra/CSetoidFun/inv2.con. +inline "cic:/CoRN/algebra/CSetoidFun/inv2.con". -inline cic:/CoRN/algebra/CSetoidFun/inv_strext.con. +inline "cic:/CoRN/algebra/CSetoidFun/inv_strext.con". -inline cic:/CoRN/algebra/CSetoidFun/Inv.con. +inline "cic:/CoRN/algebra/CSetoidFun/Inv.con". (* UNEXPORTED Implicit Arguments Inv [A B]. *) -inline cic:/CoRN/algebra/CSetoidFun/Inv_bij.con. +inline "cic:/CoRN/algebra/CSetoidFun/Inv_bij.con". (* UNEXPORTED End bijections. @@ -577,3 +609,11 @@ Implicit Arguments Inv [A B]. Implicit Arguments conj_wd [S P Q]. *) +(* NOTATION +Notation Prj1 := (prj1 _ _ _ _). +*) + +(* NOTATION +Notation Prj2 := (prj2 _ _ _ _). +*) +