helm_registry: added the pair unmarshaller

[helm.git] / matita / contribs / CoRN-Decl / algebra / CSetoidFun.ma

diff --git a/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma b/matita/contribs/CoRN-Decl/algebra/CSetoidFun.ma
index d183c70e8b8288e12e228fc1759aa74a636f2e3b..84c0c6c2672ff96e60d89d466bc47751685cb408 100644 (file)
--- 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 _ _ _ _).
+*)
+