]> matita.cs.unibo.it Git - helm.git/commitdiff
Some CoRN files.
authorAndrea Asperti <andrea.asperti@unibo.it>
Tue, 16 Jan 2007 12:08:31 +0000 (12:08 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Tue, 16 Jan 2007 12:08:31 +0000 (12:08 +0000)
helm/software/matita/library/algebra/CoRN/SemiGroups.ma [new file with mode: 0644]
helm/software/matita/library/algebra/CoRN/SetoidFun.ma
helm/software/matita/library/algebra/CoRN/Setoids.ma

diff --git a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma
new file mode 100644 (file)
index 0000000..3d20909
--- /dev/null
@@ -0,0 +1,400 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* $Id: CSemiGroups.v,v 1.10 2004/09/24 15:30:34 loeb Exp $ *)
+(* printing [+] %\ensuremath+% #+# *)
+(* printing {+} %\ensuremath+% #+# *)
+
+(* Require Export CSetoidInc. *)
+
+(* Begin_SpecReals *)
+
+set "baseuri" "cic:/matita/algebra/CoRN/CSemiGroups".
+include "algebra/CoRN/SetoidInc.ma".
+
+(*------------------------------------------------------------------*)
+(* Semigroups - Definition of the notion of Constructive Semigroup  *)
+(*------------------------------------------------------------------*)
+
+definition is_CSemiGroup : \forall A : CSetoid. \forall op: CSetoid_bin_op A. Prop \def 
+\lambda A : CSetoid. \lambda op: CSetoid_bin_op A. CSassociative A (csbf_fun A A A op).
+
+record CSemiGroup : Type \def 
+  {csg_crr   :> CSetoid;
+   csg_op    :  CSetoid_bin_op csg_crr;
+   csg_proof :  is_CSemiGroup csg_crr csg_op}.
+
+(*
+Implicit Arguments csg_op [c].
+Infix "[+]" := csg_op (at level 50, left associativity).
+End_SpecReals *)
+
+
+
+(*--------------------------------------------------------------*) 
+(*  Semigroup axioms - The axiomatic properties of a semi group *)
+(*--------------------------------------------------------------*)
+(* Variable G : CSemiGroup. *)
+
+lemma CSemiGroup_is_CSemiGroup : \forall G : CSemiGroup. is_CSemiGroup (csg_crr G) (csg_op G).
+intro.
+elim G. simplify. exact H.
+qed.
+(* CoRN 
+Lemma CSemiGroup_is_CSemiGroup : is_CSemiGroup G csg_op.*)
+
+lemma plus_assoc : \forall G : CSemiGroup. 
+CSassociative G (csbf_fun G G G (csg_op G)).
+exact CSemiGroup_is_CSemiGroup.
+qed.
+
+(*--------------------------------------------------------------*) 
+(*                          Semigroup basics                    *)
+(*--------------------------------------------------------------*)
+
+lemma plus_assoc_unfolded : \forall G : CSemiGroup. \forall x,y,z : ?.
+ (csbf_fun G G G (csg_op G) x (csbf_fun G G G (csg_op G) y z)) = 
+    (csbf_fun G G G (csg_op G) (csbf_fun G G G  (csg_op G) x y) z).
+  intros.
+  apply plus_assoc.
+qed.
+
+(* Section p71R1. *)
+
+(* Morphism
+%\begin{convention}%
+Let [S1 S2:CSemiGroup].
+%\end{convention}%
+*)
+
+(* Variable S1:CSemiGroup.
+Variable S2:CSemiGroup. *)
+
+definition morphism_of_CSemiGroups: \forall S1,S2: CSemiGroup. \forall f: CSetoid_fun S1 S2. 
+  Prop \def
+  \lambda S1,S2: CSemiGroup. \lambda f: CSetoid_fun S1 S2. 
+  (\forall a,b:S1. (csf_fun S1 S2 f (csbf_fun ? ? ? (csg_op ?) a b)) =
+    (csbf_fun ? ? ? (csg_op ?) (csf_fun S1 S2 f a) (csf_fun S1 S2  f b))).
+
+(* End p71R1. *)
+
+(* About the unit *)
+
+(* Zero ?????  *)
+
+definition is_rht_unit: \forall S: CSemiGroup. \forall op : CSetoid_bin_op S. \forall  Zero: ?. Prop  
+  \def 
+  \lambda S: CSemiGroup. \lambda op : CSetoid_bin_op S. \lambda  Zero: ?.
+  \forall x:?. (csbf_fun ? ? ? op x Zero) = x.
+
+(* Definition is_rht_unit S (op : CSetoid_bin_op S) Zero : Prop := forall x, op x Zero [=] x. *)
+
+(* End_SpecReals *)
+
+definition is_lft_unit: \forall S: CSemiGroup. \forall op : CSetoid_bin_op S. \forall  Zero: ?. Prop 
+  \def 
+  \lambda S: CSemiGroup. \lambda op : CSetoid_bin_op S. \lambda  Zero: ?.
+   \forall x:?. (csbf_fun ? ? ? op Zero x) = x.
+
+
+(* Implicit Arguments is_lft_unit [S]. *)
+
+(* Begin_SpecReals *)
+
+(* Implicit Arguments is_rht_unit [S]. *)
+
+(* An alternative definition:
+*)
+
+definition is_unit: \forall S:CSemiGroup.  S \to Prop \def
+\lambda S:CSemiGroup.
+\lambda e. (\forall (a:S). (csbf_fun ? ? ? (csg_op ?) e a) = a \and (csbf_fun ? ? ? (csg_op ?) a e) 
+ = a).
+
+lemma cs_unique_unit : \forall S:CSemiGroup. \forall e,f:S. 
+(is_unit S e) \and (is_unit S f) \to e = f.
+intros 3 (S e f).
+unfold is_unit.
+intro H.
+elim H 0.
+clear H.
+intros (H0 H1).
+elim (H0 f) 0.
+clear H0.
+intros (H2 H3).
+elim (H1 e) 0.
+clear H1.
+intros (H4 H5).
+auto new.
+qed.
+(*
+astepr (e[+]f). 
+astepl (e[+]f).
+apply eq_reflexive.
+Qed.
+*)
+
+(* End_SpecReals *)
+
+(* Hint Resolve plus_assoc_unfolded: algebra. *)
+
+(* Functional operations
+We can also define a similar addition operator, which will be denoted by [{+}], on partial functions.
+
+%\begin{convention}% Whenever possible, we will denote the functional construction corresponding to an algebraic operation by the same symbol enclosed in curly braces.
+%\end{convention}%
+
+At this stage, we will always consider automorphisms; we %{\em %could%}% treat this in a more general setting, but we feel that it wouldn't really be a useful effort.
+
+%\begin{convention}% Let [G:CSemiGroup] and [F,F':(PartFunct G)] and denote by [P] and [Q], respectively, the predicates characterizing their domains.
+%\end{convention}%
+*)
+
+(* Section Part_Function_Plus. *)
+
+(* Variable G : CSemiGroup.
+Variables F F' : PartFunct G. *)
+
+(* begin hide *)
+(*Let P := Dom F.
+Let Q := Dom F'.*)
+(* end hide *)
+definition NP : \forall G:CSemiGroup. \forall F,F': PartFunct G. ? \def
+   \lambda G:CSemiGroup. \lambda F,F': PartFunct G.
+   pfdom ? F.
+definition NQ : \forall G:CSemiGroup. \forall F,F': PartFunct G. ? \def
+   \lambda G:CSemiGroup. \lambda F,F': PartFunct G.
+   pfdom ? F'.
+   
+lemma part_function_plus_strext :  \forall G:CSemiGroup. \forall F,F': PartFunct G. 
+\forall x, y:G. \forall Hx : conjP G (pfdom G F) (pfdom G F') x. 
+\forall Hy : conjP G (pfdom G F) (pfdom G F') y.
+(csbf_fun ? ? ? (csg_op G) (pfpfun ? F x (prj1 G (pfdom G F) (pfdom G F') x Hx)) 
+  (pfpfun ? F' x (prj2 G (pfdom G F) (pfdom G F') x Hx))) 
+  \neq (csbf_fun ? ? ? (csg_op G) (pfpfun ? F y (prj1 G (pfdom G F) (pfdom G F') y Hy)) 
+    (pfpfun ? F' y (prj2 G (pfdom G F) (pfdom G F') y Hy))) 
+  \to x \neq y.
+intros (G F F' x y Hx Hy H).
+elim (bin_op_strext_unfolded ? ? ? ? ? ? H)[
+apply pfstrx[apply F|elim Hx.apply t|elim Hy.apply t|exact H1]|
+apply pfstrx[apply F'|elim Hx.apply t1|elim Hy.apply t1|exact H1]]
+qed.
+
+definition Fplus : \forall G:CSemiGroup. \forall F,F': PartFunct G. ? \def 
+  \lambda G:CSemiGroup. \lambda F,F': PartFunct G.
+mk_PartFunct G ? (conj_wd ? ? ? (dom_wd ? F) (dom_wd ? F'))
+  (\lambda x,Hx. (csbf_fun ? ? ? (csg_op ?) 
+            (pfpfun ? F x (prj1 ? ? ? ? Hx))  (pfpfun ? F' x (prj2 ? ? ? ? Hx)))) 
+  (part_function_plus_strext G F F').
+
+(*
+%\begin{convention}% Let [R:G->CProp].
+%\end{convention}%
+*)
+
+(* Variable R : G -> CProp. *)
+
+lemma included_FPlus :  \forall G:CSemiGroup.  \forall R : G \to Type. \forall F,F': PartFunct G. 
+included ? R (NP G F F' ) -> included ? R (NQ G F F') \to included ? R (pfdom ? (Fplus G F F')).
+intros; unfold Fplus;simplify. apply included_conj; assumption.
+qed.
+
+lemma included_FPlus' : \forall G:CSemiGroup.  \forall R : G \to Type. \forall F,F': PartFunct G. 
+  included ? R (pfdom ? (Fplus G F F')) \to included ? R (NP G F F').
+intros. unfold Fplus in i. simplify in i; unfold NP.
+  apply (included_conj_lft ? ? ? ? i); apply H.
+qed.
+
+lemma included_FPlus'' : \forall G:CSemiGroup.  \forall R : G \to Type. \forall F,F': PartFunct G.
+   included ? R (pfdom ? (Fplus G F F')) -> included ? R (NQ G F F').
+intros (G R F F'H); unfold Fplus in H. simplify in H;
+unfold NQ. apply (included_conj_rht ? (pfdom G F)); apply H.
+qed.
+
+(* End Part_Function_Plus. *)
+
+(* Implicit Arguments Fplus [G].
+Infix "{+}" := Fplus (at level 50, left associativity).
+
+Hint Resolve included_FPlus : included.
+
+Hint Immediate included_FPlus' included_FPlus'' : included.
+*) 
+
+(* Subsemigroups
+%\begin{convention}%
+Let [csg] a semi-group and [P] a non-empty
+predicate on the semi-group which is preserved by [[+]].
+%\end{convention}%
+*)
+
+(* Section SubCSemiGroups. *)
+
+(* Variable csg : CSemiGroup.
+   Variable P : csg -> CProp.
+   Variable op_pres_P : bin_op_pres_pred _ P csg_op. *) 
+
+definition subcrr : \forall csg: CSemiGroup. \forall P : csg -> Prop. CSetoid \def 
+  \lambda csg: CSemiGroup. \lambda P : csg -> Prop.
+  mk_SubCSetoid ? P.
+definition mk_SubCSemiGroup :\forall csg: CSemiGroup. \forall P : csg -> Prop.
+    \forall op_pres_P : bin_op_pres_pred csg P (csg_op csg). CSemiGroup \def
+  \lambda csg: CSemiGroup. \lambda P : csg -> Prop. 
+    \lambda op_pres_P : bin_op_pres_pred csg P (csg_op csg).
+   mk_CSemiGroup (subcrr csg P) (mk_SubCSetoid_bin_op ? ? ? op_pres_P )
+ (restr_f_assoc csg P ? op_pres_P  (plus_assoc csg)).
+(* Section D9S. *)
+
+(* Direct Product
+%\begin{convention}%
+Let [M1 M2:CSemiGroup]
+%\end{convention}%
+*)
+
+(* Variable M1 M2: CSemiGroup. *)
+
+definition dprod: \forall M1,M2:CSemiGroup. \forall x:ProdCSetoid (csg_crr M1) (csg_crr M2).
+  \forall y:ProdCSetoid (csg_crr M1) (csg_crr M2). (ProdCSetoid (csg_crr M1) (csg_crr M2)) \def
+  \lambda M1,M2:CSemiGroup. \lambda x:ProdCSetoid (csg_crr M1) (csg_crr M2).
+  \lambda y:ProdCSetoid (csg_crr M1) (csg_crr M2).
+  match x with 
+    [pairT (x1: (cs_crr (csg_crr M1))) (x2: (cs_crr (csg_crr M2))) \Rightarrow 
+     match y with 
+       [pairT (y1: (cs_crr (csg_crr M1))) (y2: (cs_crr (csg_crr M2))) \Rightarrow 
+          pairT (cs_crr (csg_crr M1)) (cs_crr (csg_crr M2))
+(csbf_fun ? ? ? (csg_op M1) x1 y1) (csbf_fun ? ? ? (csg_op M2) x2 y2)]].
+
+lemma dprod_strext: \forall M1,M2:CSemiGroup.
+(bin_fun_strext (ProdCSetoid M1 M2)(ProdCSetoid M1 M2)
+  (ProdCSetoid M1 M2) (dprod M1 M2)).
+unfold bin_fun_strext.
+intros 6 (M1 M2 x1 x2 y1 y2).
+unfold dprod.
+elim x1 0.
+intros 2 (a1 a2).
+elim x2 0.
+intros 2 (b1 b2).
+elim y1 0.
+intros 2 (c1 c2).
+elim y2 0.
+intros 2 (d1 d2).
+simplify.
+intro H.
+elim H 0[simplify.
+clear H.
+intro H.
+cut (a1 \neq b1 \lor c1 \neq d1).
+elim Hcut[left.left.assumption|right.left.assumption]
+|intros.simplify in H1.
+clear H.
+cut (a2 \neq b2 \lor c2 \neq d2).
+elim Hcut [left.right.assumption|right.right.assumption]
+][
+letin H0 \def (csg_op M1).
+unfold csg_op in H0.
+unfold CSetoid_bin_op in H0.
+letin H1 \def (csbf_strext M1 M1 M1 H0).
+unfold csbf_strext in H1.
+unfold bin_fun_strext in H1.
+apply H1.
+exact H|
+letin H0 \def (csg_op M2).
+unfold csg_op in H0.
+unfold CSetoid_bin_op in H0.
+letin H2 \def (csbf_strext M2 M2 M2 H0).
+unfold csbf_strext in H2.
+unfold bin_fun_strext in H2.
+apply H2.
+exact H1]
+qed.
+
+definition dprod_as_csb_fun: \forall M1,M2:CSemiGroup. 
+  CSetoid_bin_fun (ProdCSetoid M1 M2) (ProdCSetoid M1 M2)(ProdCSetoid M1 M2)\def
+  \lambda M1,M2:CSemiGroup.
+  mk_CSetoid_bin_fun (ProdCSetoid M1 M2)(ProdCSetoid M1 M2)
+  (ProdCSetoid M1 M2) (dprod M1 M2) (dprod_strext M1 M2).
+
+lemma direct_product_is_CSemiGroup: \forall M1,M2:CSemiGroup. 
+  (is_CSemiGroup (ProdCSetoid M1 M2) (dprod_as_csb_fun M1 M2)).
+  intros.
+unfold is_CSemiGroup.
+unfold CSassociative.
+intros (x y z).
+elim x 0.
+intros (x1 x2).
+elim y 0.
+intros (y1 y2).
+elim z 0.
+intros (z1 z2).
+split[unfold dprod_as_csb_fun. simplify.apply CSemiGroup_is_CSemiGroup|
+      unfold dprod_as_csb_fun. simplify.apply CSemiGroup_is_CSemiGroup].
+qed.
+
+definition direct_product_as_CSemiGroup : \forall M1,M2:CSemiGroup. ? \def
+  \lambda M1,M2: CSemiGroup.
+  mk_CSemiGroup (ProdCSetoid M1 M2) (dprod_as_csb_fun M1 M2) 
+  (direct_product_is_CSemiGroup M1 M2).
+
+(* End D9S. *)
+
+(* The SemiGroup of Setoid functions *)
+
+lemma FS_is_CSemiGroup:\forall X:CSetoid.
+  is_CSemiGroup (FS_as_CSetoid X X) (comp_as_bin_op  X ).
+  intro.
+unfold is_CSemiGroup.
+apply assoc_comp.
+qed.
+
+definition FS_as_CSemiGroup : \forall A : CSetoid. ? \def \lambda A:CSetoid.
+  mk_CSemiGroup (FS_as_CSetoid A A) (comp_as_bin_op A) (assoc_comp A).
+
+(* Section p66E2b4. *)
+
+(* The Free SemiGroup
+%\begin{convention}% Let [A:CSetoid].
+%\end{convention}%
+*)
+
+(* Variable A:CSetoid. *)
+
+lemma Astar_is_CSemiGroup: \forall A:CSetoid. 
+  (is_CSemiGroup (free_csetoid_as_csetoid A) (app_as_csb_fun A)).
+  intro.
+unfold is_CSemiGroup.
+unfold CSassociative.
+intro x.
+unfold app_as_csb_fun.
+simplify.
+elim x 0.
+simplify.
+intros (x y).
+elim x.
+simplify.
+apply eq_reflexive_unfolded.
+simplify. left. apply eq_reflexive_unfolded.assumption.
+
+simplify.
+intros.unfold appA in H.
+generalize in match (H y z).intros.unfold appA in H1.left. 
+apply eq_reflexive_unfolded.
+assumption.
+qed.
+
+definition Astar_as_CSemiGroup: \forall A:CSetoid. ? \def
+  \lambda A:CSetoid. 
+  mk_CSemiGroup (free_csetoid_as_csetoid A) (app_as_csb_fun A) 
+   (Astar_is_CSemiGroup A).
+
+(* End p66E2b4. *)
index a90960a2c46337841e1641f31615c3e32e8d5320..00e75ab1d503d3c909fbb568c9791ba92a5a8f22 100644 (file)
@@ -16,7 +16,7 @@
 
 set "baseuri" "cic:/matita/algebra/CoRN/SetoidFun".
 include "algebra/CoRN/Setoids.ma".
-
+include "higher_order_defs/relations.ma".
 
 definition ap_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def
 \lambda A,B : CSetoid. \lambda f,g : CSetoid_fun A B.
@@ -39,104 +39,1264 @@ unfold.
 intro.
 elim H.
 cut (csf_fun A B f a = csf_fun A B f a)
-[ 
- apply eq_imp_not_ap.
- apply A.
- assumption. 
- assumption.
- auto. 
- auto 
-|
- apply eq_reflexive_unfolded 
+[ apply (eq_imp_not_ap A)
+ [
+  assumption|assumption|apply eq_reflexive_unfolded|
+  apply (csf_strext_unfolded A B f).
+  exact H1
+ ]
+|apply eq_reflexive_unfolded 
 ]
 qed.
 
-(*
-Lemma irrefl_apfun : forall A B : CSetoid, irreflexive (ap_fun A B).
-intros A B.
-unfold irreflexive in |- *.
-intros f.
-unfold ap_fun in |- *.
-red in |- *.
-intro H.
-elim H.
-intros a H0.
-set (H1 := ap_irreflexive_unfolded B (f a)) in *.
-intuition.
-Qed.
-*)
-
-
-(*
 lemma cotrans_apfun : \forall A,B : CSetoid. cotransitive (CSetoid_fun A B) (ap_fun A B).
 intros (A B).
 unfold.
 unfold ap_fun.
 intros (f g H h).
-decompose.
-apply ap_cotransitive.
-apply (ap_imp_neq B (csf_fun A B x a) (csf_fun A B y a) H1).
-(* letin foo \def (\exist a:A.csf_fun A B x a\neq csf_fun A B z a). *)
+elim H.
+lapply (ap_cotransitive ? ? ? H1 (csf_fun A B h a)).
+elim Hletin.
+left.
+apply (ex_intro ? ? a H2).
+right.
+apply (ex_intro ? ? a H2).
+qed.
+
+lemma ta_apfun : \forall A, B : CSetoid. tight_apart (CSetoid_fun A B) (eq_fun A B) (ap_fun A B).
+unfold tight_apart.
+intros (A B f g).
+unfold ap_fun.
+unfold eq_fun.
+split
+[ intros. apply not_ap_imp_eq.
+unfold.intro.apply H.
+apply (ex_intro ? ? a).assumption.
+ | intros.unfold.intro.
+   elim H1.
+   apply (eq_imp_not_ap ? ? ? ? H2).
+   apply H.
+]
+qed.
 
+lemma sym_apfun : \forall A, B : CSetoid. symmetric ? (ap_fun A B).
+unfold symmetric.
+unfold ap_fun.
+intros 5 (A B f g H).
+elim H 0.
+clear H.
+intros 2 (a H).
+apply (ex_intro ? ? a).
+apply ap_symmetric_unfolded.
+exact H.
+qed.
 
-apply (ap_cotransitive B ? ? H1 ?).
+definition FS_is_CSetoid : \forall A, B : CSetoid. ? \def
+  \lambda A, B : CSetoid.
+    mk_is_CSetoid (CSetoid_fun A B) (eq_fun A B) (ap_fun A B)
+    (irrefl_apfun A B) (sym_apfun A B) (cotrans_apfun A B) (ta_apfun A B).
 
-split.
-left.
-elim H.
+definition FS_as_CSetoid : \forall A, B : CSetoid. ? \def
+  \lambda A, B : CSetoid.
+    mk_CSetoid (CSetoid_fun A B) (eq_fun A B) (ap_fun A B) 
+    (FS_is_CSetoid A B).
+
+(* Nullary and n-ary operations *)
+
+definition is_nullary_operation : \forall S:CSetoid. \forall s:S. Prop \def 
+\lambda S:CSetoid. \lambda s:S. True.
+
+let rec n_ary_operation (n:nat) (V:CSetoid) on n : CSetoid \def
+match n with
+[ O \Rightarrow V
+|(S m) \Rightarrow (FS_as_CSetoid V (n_ary_operation m V))].
+
+
+(* 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.  *)
+
+(* Variables S1 S2 S3 : CSetoid.
+Variable f : CSetoid_fun S1 S2.
+Variable g : CSetoid_fun S2 S3. *)
+
+
+definition compose_CSetoid_fun : \forall S1,S2,S3 :CSetoid. \forall f: (CSetoid_fun S1 S2). \forall g: (CSetoid_fun S2 S3). 
+CSetoid_fun S1 S3.
+intros (S1 S2 S3 f g).
+apply (mk_CSetoid_fun ? ? (\lambda x :cs_crr S1. csf_fun S2 S3 g (csf_fun S1 S2 f x))).
+unfold fun_strext.
+intros (x y H).
+apply (csf_strext ? ? f).
+apply (csf_strext ? ? g).
+assumption.
+qed.
+
+(* End unary_function_composition. *)
+
+(* Composition as operation *)
+definition comp : \forall A, B, C : CSetoid.
+FS_as_CSetoid A B \to FS_as_CSetoid B C \to FS_as_CSetoid A C.
+intros (A B C f g).
+letin H \def (compose_CSetoid_fun A B C f g).
+exact H.
+qed.
+
+definition comp_as_bin_op : \forall A:CSetoid.  CSetoid_bin_op (FS_as_CSetoid A A).
+intro A.
+unfold CSetoid_bin_op.
+apply (mk_CSetoid_bin_fun ? ? ? (comp A A A)).
+unfold bin_fun_strext.
+unfold comp.
+intros  4 (f1 f2 g1 g2).
+simplify.
+unfold compose_CSetoid_fun.
+simplify.
+elim f1 0.
+unfold fun_strext.
+clear f1.
+intros 2 (f1 Hf1).
+elim f2 0.
+unfold fun_strext.
+clear f2.
+intros 2 (f2 Hf2).
+elim g1 0.
+unfold fun_strext.
+clear g1.
+intros 2 (g1 Hg1).
+elim g2 0.
+unfold fun_strext.
+clear g2.
+intros 2 (g2 Hg2).
+simplify.
+intro H.
+elim H 0. 
 clear H.
-intros a H.
-set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *.
-elim H1.
-clear H1.
-intros H1.
+intros 2 (a H).
+letin H0 \def (ap_cotransitive A (g1 (f1 a)) (g2 (f2 a)) H (g2 (f1 a))).
+elim H0 0.
+clear H0.
+intro H0.
+right.
+exists.
+apply (f1 a).
+exact H0.
+
+clear H0.
+intro H0.
 left.
-exists a.
-exact H1.
+exists.
+apply a.
+apply Hg2.
+exact H0.
+qed.
+
+
+(* Questa coercion composta non e' stata generata automaticamente *)
+lemma mycor: ∀S. CSetoid_bin_op S → (S → S → S).
+ intros;
+ unfold in c;
+ apply (c c1 c2).
+qed.
+coercion cic:/matita/algebra/CoRN/SetoidFun/mycor.con 2.
+
+(* Mettendola a mano con una beta-espansione funzionerebbe *)
+(*lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (\lambda e.mycor ? (comp_as_bin_op A) e)).*)
+(* Questo sarebbe anche meglio: senza beta-espansione *)
+(*lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (mycor ? (comp_as_bin_op A))).*)
+(* QUESTO E' QUELLO ORIGINALE MA NON FUNZIONANTE *)
+(* lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (comp_as_bin_op A)). *)
+lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (mycor ? (comp_as_bin_op A))).
+unfold CSassociative.
+unfold comp_as_bin_op.
+intros 4 (A f g h).
+simplify.
+elim f.
+elim g.
+elim h.
+whd.intros.
+simplify.
+apply eq_reflexive_unfolded.
+qed.
+
+definition compose_CSetoid_bin_un_fun: \forall A,B,C : CSetoid. 
+\forall f : CSetoid_bin_fun B B C. \forall g : CSetoid_fun A B.  
+CSetoid_bin_fun A A C.
+intros 5 (A B C f g).
+apply (mk_CSetoid_bin_fun A A C (\lambda a0,a1 : cs_crr A. f (csf_fun ? ? g a0) (csf_fun ? ? g a1))).
+unfold.
+intros 5 (x1 x2 y1 y2 H0).
+letin H10 \def (csbf_strext B B C f).
+unfold in H10.
+letin H40 \def (csf_strext A B g).
+unfold in H40.
+elim (H10 (csf_fun ? ? g x1) (csf_fun ? ? g x2) (csf_fun ? ? g y1) (csf_fun ? ? g y2) H0); 
+[left | right]; auto.
+qed.
+
+definition compose_CSetoid_bin_fun: \forall A, B, C : CSetoid. 
+\forall f,g : CSetoid_fun A B.\forall h : CSetoid_bin_fun B B C.
+CSetoid_fun A C.
+intros (A B C f g h).
+apply (mk_CSetoid_fun A C (λa : cs_crr A. csbf_fun ? ? ? h (csf_fun ? ? f a) (csf_fun ? ? g a))).
+unfold.
+intros (x y H).
+elim (csbf_strext ? ? ? ? ? ? ? ? H)[
+ apply (csf_strext A B f).exact H1
+ |apply (csf_strext A B g).exact H1]
+qed.
+
+definition compose_CSetoid_un_bin_fun: \forall A,B,C :CSetoid. \forall f : CSetoid_bin_fun B B C.
+ ∀ g : CSetoid_fun C A. CSetoid_bin_fun B B A.
+intros (A0 B0 C f g).
+apply (mk_CSetoid_bin_fun ? ? ? (\lambda x,y : B0. csf_fun ? ? g (f x y))).
+unfold.
+intros 4 (x1 x2 y1 y2).
+elim f 0.
+unfold bin_fun_strext.
+elim g 0.
+unfold fun_strext.
+intros 5 (gu gstrext fu fstrext H).
+apply fstrext.
+apply gstrext.
+exact H.
+qed.
+
+(* End unary_and_binary_function_composition.*)
+
+(*Projections*)
+
+(*Section function_projection.*)
+
+lemma proj_bin_fun : \forall A, B, C: CSetoid. 
+\forall f : CSetoid_bin_fun A B C. \forall a: ?. 
+fun_strext ? ? (f a).
+intros (A B C f a).
+unfold.
+elim f 0.
+intro fo.
+simplify.
+intros 4 (csbf_strext0 x y H).
+elim (csbf_strext0 ? ? ? ? H) 0; intro H0.
+ elim (ap_irreflexive_unfolded ? ? H0).
+exact H0.
+qed.
+
+
+definition projected_bin_fun: \forall A,B,C : CSetoid. \forall f : CSetoid_bin_fun A B C.
+\forall a : A. ? \def
+\lambda A,B,C : CSetoid. \lambda f : CSetoid_bin_fun A B C.
+\lambda a : A.
+ mk_CSetoid_fun B C (f a) (proj_bin_fun A B C f a).
+
+(* End function_projection. *)
+
+(* Section BinProj. *)
+
+(* Variable S : CSetoid. *)
+
+definition binproj1 : \forall S: CSetoid. \forall x,y:S. ? \def
+\lambda S:CSetoid. \lambda x,y:S.
+ x.
+lemma binproj1_strext :\forall S:CSetoid. bin_fun_strext ? ? ? (binproj1 S).
+intro.unfold;
+intros 4.unfold binproj1.intros.left.exact H.
+qed.
+
+definition cs_binproj1 :\forall S:CSetoid. CSetoid_bin_op S.
+intro.
+unfold.
+apply (mk_CSetoid_bin_op ? (binproj1 S)).
+apply binproj1_strext.
+qed.
+
+(* End BinProj. *)
+
+(*Combining operations
+%\begin{convention}% Let [S1], [S2] and [S3] be setoids.
+%\end{convention}%
+*)
 
+(* Section CombiningOperations.
+Variables S1 S2 S3 : CSetoid.*)
+
+(*
+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].
+*)
+
+(* Section CombiningUnaryOperations.
+Variable f : CSetoid_fun S1 S2.
+Variable op : CSetoid_un_op S2. *)
+
+definition opOnFun : \forall S1,S2,S3 :CSetoid. \forall f : CSetoid_fun S1 S2.
+  \forall op : CSetoid_un_op S2.
+  CSetoid_fun S1 S2.
+intros (S1 S2 S3 f op).
+apply (mk_CSetoid_fun S1 S2 (\lambda x :  cs_crr S1. csf_fun ? ? op (csf_fun ? ? f x))).
+unfold fun_strext; intros (x y H).
+apply (csf_strext ? ? f x y).
+apply (csf_strext ? ? op ? ? H).
+qed.
+(*
+End CombiningUnaryOperations.
+
+End CombiningOperations.
+
+Section p66E2b4.
+*)
+(* The Free Setoid
+%\begin{convention}% Let [A:CSetoid].
+%\end{convention}%
+*)
+
+(* Variable A:CSetoid. *)
+
+(* TODO from listtype.ma!!!!!!!! *)
+inductive Tlist (A : Type) : Type \def
+    Tnil : Tlist A
+  | Tcons : A \to Tlist A  \to Tlist A.
+
+definition Astar: \forall A: CSetoid. ? \def
+\lambda A:CSetoid.
+ Tlist A.
+
+
+definition empty_word : \forall A: Type. ? \def
+\lambda A:Type. (Tnil A).
+
+(* from listtype.ma!!!!!!!! *)
+let rec Tapp (A:Type) (l,m: Tlist A) on l \def
+  match l with
+  [ Tnil \Rightarrow m
+  | (Tcons a l1) \Rightarrow (Tcons  A a (Tapp A l1 m))].
+
+definition appA : \forall A: CSetoid. ? \def
+\lambda A:CSetoid.
+   (Tapp A).
+
+let rec eq_fm (A:CSetoid) (m:Astar A) (k:Astar A) on m : Prop \def
+match m with
+[ Tnil ⇒ match k with
+        [ Tnil ⇒ True
+        | (Tcons  a l) ⇒ False]
+| (Tcons  b n) ⇒ match k with
+        [Tnil ⇒ False
+        |(Tcons  a l) ⇒ b=a ∧ (eq_fm A n l)]
+].                                 
+
+let rec CSap_fm (A:CSetoid)(m:Astar A)(k:Astar A) on m: Prop \def
+match m with
+[Tnil ⇒ match k with
+        [Tnil ⇒ False
+        |(Tcons a l) ⇒ True]
+|(Tcons b n) ⇒ match k with
+        [Tnil ⇒ True  
+        |(Tcons a l) ⇒ b ≠ a ∨ (CSap_fm A n l)]
+].
+
+lemma ap_fm_irreflexive: \forall A:CSetoid. (irreflexive (Astar A) (CSap_fm A) ).
+unfold irreflexive.
+intros 2 (A x).
+elim x[
+simplify.
+unfold.
+intro Hy.
+exact Hy|
+simplify.
+unfold.
+intro H1.
+apply H.
+elim H1[
 clear H1.
+generalize in match (ap_irreflexive A).
+unfold irreflexive.
+unfold Not.
+intro.
+unfold in H.
+apply False_ind.
+apply H1.apply t.
+exact H2|exact H2]
+]
+qed.
+
+lemma ap_fm_symmetric: \forall A:CSetoid. (symmetric  (Astar A) (CSap_fm A)).
+intro A.
+unfold symmetric.
+intro x.
+elim x 0 [
+intro y.
+  elim y 0[
+  simplify.
+  intro.
+  exact H|
+  simplify.
+  intros.
+  exact H1]|
+  intros 4 (t t1 H y).
+  elim y 0[
+    simplify.
+    intro.
+    exact H1|
+  simplify.
+  intros.
+  elim H2 0 [
+  generalize in match (ap_symmetric A).
+  unfold symmetric.
+  intros.
+  left.
+  apply ap_symmetric.exact H4|
+  intro.
+  right.
+  apply H.
+  exact H3]
+  ]
+ ]
+qed.
+
+lemma ap_fm_cotransitive : \forall A:CSetoid. (cotransitive (Astar A) (CSap_fm A)).
+intro A.
+unfold cotransitive.
+intro x.
+elim x 0 [
+intro y.
+elim y 0 [
+intro.simplify in H.intro.elim z.simplify.left. exact H|intros (c l H1 H z).
+elim z 0[ 
+simplify.
+right. apply I|intros (a at).simplify. left. apply I]]
+simplify.
+left.
+auto new|intros 2 (c l).
+intros 2 (Hy).
+elim y 0[
+intros 2 (H z).
+elim z 0 [simplify. left.apply I|
+intros  2 ( a at).
 intro H1.
+simplify.
+right. apply I]|
+intros (a at bo H z).
+elim z 0[
+simplify.left.
+apply I|
+intros 2 (c0 l0).
+elim H 0 [
+clear H.
+intro.intro Hn.simplify.
+generalize in match (ap_cotransitive A c a H c0).
+intros.elim H1 0[intros.left. left.exact H2|
+intro.right.left.exact H2]|intros.
+simplify.
+generalize in match (Hy at H1 l0).
+intros.
+elim H3[
+left.right.exact H4|
+right.right.exact H4]]]]]
+qed.
+
+lemma ap_fm_tight : \forall A:CSetoid.  (tight_apart (Astar A) (eq_fm A) (CSap_fm A)).
+intro A.
+unfold tight_apart.
+intro x.
+unfold Not.
+elim x 0[
+  intro y.
+  elim y 0[
+    split[simplify.intro.auto new|simplify.intros.exact H1]|
+intros (a at).
+simplify.
+split[intro.auto new|intros. exact H1]
+]
+|
+intros (a at IHx).
+elim y 0[simplify.
+  split[intro.auto new|intros.exact H]
+  |
+intros 2 (c l).
+generalize in match (IHx l).
+intro H0.
+elim H0. 
+split.
+intro H3.
+split.
+generalize in match (ap_tight A a c).
+intros.
+elim H4.
+clear H4.apply H5.
+unfold.intro.simplify in H3.
+apply H3.left.exact H4.
+intros.elim H2.
+apply H.intro.apply H3.simplify. right. exact H6.
+intro H3.
+elim H3 0.
+clear H3.
+intros.
+elim H5.
+generalize in match (ap_tight A a c).
+intro.
+elim H7.clear H7.
+unfold Not in H9.simplify in H5.
+apply H9.
+exact H3.exact H6.
+apply H1.
+exact H4.exact H6.]]
+qed.
+
+definition free_csetoid_is_CSetoid: \forall A:CSetoid.
+  (is_CSetoid (Astar A) (eq_fm A) (CSap_fm A)) \def
+  \lambda A:CSetoid.
+  (mk_is_CSetoid (Astar A) (eq_fm A) (CSap_fm A) (ap_fm_irreflexive A) (ap_fm_symmetric A) 
+  (ap_fm_cotransitive A) (ap_fm_tight A )).
+
+definition free_csetoid_as_csetoid: \forall A:CSetoid. CSetoid \def
+\lambda A:CSetoid.
+(mk_CSetoid (Astar A) (eq_fm A) (CSap_fm A) (free_csetoid_is_CSetoid A)).
+
+lemma app_strext: \forall A:CSetoid.
+ (bin_fun_strext  (free_csetoid_as_csetoid A) (free_csetoid_as_csetoid A) 
+   (free_csetoid_as_csetoid A) (appA A)).
+intro A.
+unfold bin_fun_strext.
+intro x1.
+elim x1 0[simplify.intro x2.
+  elim x2 0[simplify.intros.right.exact H|simplify.intros.left.left]
+  |intros 6 (a at IHx1 x2 y1 y2).
+  simplify.
+    elim x2 0 [
+      elim y2 0 [simplify.intros.left.exact H|intros.left.left]
+      |elim y2 0[simplify.simplify in IHx1.
+        intros (c l H).
+        elim H1 0 [intros.left.left.exact H2| clear H1.
+          generalize in match (IHx1 l y1 (Tnil A)).
+          simplify.intros.elim H1 0 [intros.left.right.exact H3|
+            intros.right.exact H3|exact H2]
+          ]
+        |simplify.
+        intros (c l H c0 l0).
+      elim H2 0 [intros.left.left.exact H3|
+      generalize in match (IHx1 l0 y1 (Tcons A c l)).intros.
+        elim H3 0 [intros.left.right.exact H5|intros.right.exact H5|exact H4]
+      ]
+    ]
+  ]
+]
+qed.
+
+definition app_as_csb_fun: \forall A:CSetoid. 
+(CSetoid_bin_fun (free_csetoid_as_csetoid A) (free_csetoid_as_csetoid A)
+  (free_csetoid_as_csetoid A)) \def 
+  \lambda A:CSetoid.
+  (mk_CSetoid_bin_fun (free_csetoid_as_csetoid A) (free_csetoid_as_csetoid A) 
+   (free_csetoid_as_csetoid A) (appA A) (app_strext A)).
+
+(* TODO : Can't qed 
+lemma eq_fm_reflexive: \forall A:CSetoid. \forall (x:Astar A). (eq_fm A x x).
+intros (A x).
+elim x.
+simplify.left.
+simplify. left. apply eq_reflexive_unfolded.assumption.
+qed.
+*)
+(* End p66E2b4. *)
+
+(* 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{%#<i>#a
+priori#</i>#%}% restricted at the moment it is defined.
+
+Before we state our definitions we need to do some work on domains.
+*)
+
+(* 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}%
+*)
+
+(* Variable S : CSetoid.
+
+Section Conjunction.
+
+Variables P Q : S -> CProp.
+*)
+
+(* From CLogic.v *)
+inductive CAnd (A,B : Type): Type \def 
+|CAnd_intro : A \to B \to CAnd A B.
+
+definition conjP : \forall S:CSetoid. \forall P,Q: S \to Type. \forall x : S. Type 
+\def
+\lambda S:CSetoid. \lambda P,Q: S \to Type. \lambda x : S.
+ CAnd (P x)  (Q x).
+
+lemma prj1 : \forall S:CSetoid. \forall P,Q : S \to Type. \forall x : S.
+ (conjP S P Q x) \to (P x).
+intros;elim c.assumption.
+qed.
+
+lemma prj2 : \forall S:CSetoid. \forall P,Q : S \to Type. \forall x : S.
+   conjP S P Q x \to Q x.
+intros. elim c. assumption.
+qed.
+
+lemma conj_wd : \forall S:CSetoid. \forall P,Q : S \to Type. 
+  pred_wd ? P \to pred_wd ? Q \to pred_wd ? (conjP S P Q).
+  intros 3.
+  unfold pred_wd.
+  unfold conjP.
+  intros.elim c.
+  split [ apply (f x ? t).assumption|apply (f1 x ? t1). assumption]
+qed.
+
+(* End Conjunction. *)
+
+(* Section Disjunction. *)
+(* Variables P Q : S -> CProp.*)
+
+(*
+Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets).
+*)
+
+definition disj : \forall S:CSetoid. \forall P,Q : S \to Prop. \forall x : S.
+  Prop \def 
+  \lambda S:CSetoid. \lambda P,Q : S \to Prop. \lambda x : S.
+  P x \lor Q x.
+  
+lemma inj1 : \forall S:CSetoid. \forall P,Q : S \to Prop. \forall x : S. 
+  P x \to (disj S P Q x).
+intros.
+left. 
+assumption.
+qed.
+
+lemma inj2 : \forall S:CSetoid. \forall P,Q : S \to Prop. \forall x : S.
+  Q x \to disj S P Q x.
+intros. 
 right.
-exists a.
-exact H1.
-Qed.
+assumption.
+qed.
+
+lemma disj_wd : \forall S:CSetoid. \forall P,Q : S \to Prop. 
+  pred_wd ? P \to pred_wd ? Q \to pred_wd ? (disj S P Q).
+intros 3.
+unfold pred_wd.
+unfold disj.
+intros.
+elim H2 [left; apply (H x ); assumption|
+  right; apply (H1 x). assumption. exact H3]
+qed.
+(* End Disjunction. *)
+
+(* 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].
 *)
 
 (*
-Lemma cotrans_apfun : forall A B : CSetoid, cotransitive (ap_fun A B).
-intros A B.
-unfold cotransitive in |- *.
-unfold ap_fun in |- *.
-intros f g H h.
+Variable P : S -> CProp.
+Variable R : forall x : S, P x -> CProp.
+*)
+
+definition extend : \forall S:CSetoid. \forall P: S \to Type. 
+  \forall R : (\forall x:S. P x \to Type). \forall x : S. ? 
+  \def
+     \lambda S:CSetoid. \lambda P: S \to Type. 
+      \lambda R : (\forall x:S. P x \to Type). \lambda x : S.
+     CAnd (P x)  (\forall H : P x. (R  x  H) ).
+lemma ext1 : \forall S:CSetoid. \forall P: S \to Prop. 
+  \forall R : (\forall x:S. P x \to Prop). \forall x : S. 
+   extend S P R x \to P x.
+intros.
+elim e. 
+assumption.
+qed.
+
+inductive sigT (A:Type) (P:A -> Type) : Type \def
+    |existT : \forall x:A. P x \to sigT A P.
+
+lemma ext2_a : \forall S:CSetoid. \forall P: S \to Prop. 
+  \forall R : (\forall x:S. P x \to Prop). \forall x : S.
+  extend S P R x \to (sigT ? (λH : P x. R x H)).
+intros.
+elim e.
+apply (existT).assumption.
+apply (t1 t).
+qed.
+
+(*
+lemma ext2_a : \forall S:CSetoid. \forall P: S \to Prop. 
+  \forall R : (\forall x:S. P x \to Prop). \forall x : S.
+  extend S P R x \to (ex ? (λH : P x. R x H)).
+intros.
 elim H.
-clear H.
-intros a H.
-set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *.
-elim H1.
-clear H1.
-intros H1.
-left.
-exists a.
-exact H1.
+apply (ex_intro).
+exact H1.apply H2.
+qed.
+*)
+definition proj1_sigT: \forall A : Type. \forall P : A \to Type.
+ \forall e : sigT A P. ? \def
+  \lambda A : Type. \lambda P : A \to Type.
+  \lambda e : sigT A P.
+  match e with
+   [existT a b \Rightarrow a].
+   
+(* original def in CLogic.v 
+Definition proj1_sigT (A : Type) (P : A -> CProp) (e : sigT P) :=
+  match e with
+  | existT a b => a
+  end.
+*)
+(* _ *)
+definition proj2_sigTm : \forall A : Type. \forall P : A \to Type.
+ \forall e : sigT A P. ? \def
+ \lambda A : Type. \lambda P : A \to Type.
+  \lambda e : sigT A P.
+  match e return \lambda s:sigT A P. P (proj1_sigT A P s) with
+  [ existT a b \Rightarrow b].
+  
+definition projT1: \forall A: Type. \forall P: A \to Type.\forall H: sigT A P. A \def
+   \lambda A: Type. \lambda P: A \to Type.\lambda H: sigT A P.
+   match H with
+   [existT x b \Rightarrow x].
+    
+definition projT2m :  \forall A: Type. \forall P: A \to Type. \forall x:sigT A P.
+    P (projT1 A P x) \def
+    \lambda A: Type. \lambda P: A \to Type. 
+   (\lambda H:sigT A P.match H return \lambda s:sigT A P. P (projT1 A P s) with
+ [existT (x:A) (h:(P x))\Rightarrow h]).
+
+lemma ext2 : \forall S:CSetoid. \forall P: S \to Prop. 
+\forall R : (\forall x:S. P x \to Prop).
+\forall x: S.
+ \forall Hx:extend S P R x. 
+    R x (proj1_sigT ? ? (ext2_a S P R x Hx)).
+    intros.
+    elim ext2_a.
+    apply (projT2m (P x) (\lambda Hbeta:P x.R x a)).
+    apply (existT (P x) ).assumption.assumption.
+qed.
+
+(*    
+Lemma ext2 : forall (x : S) (Hx : extend x), R x (ProjT1 (ext2_a x Hx)).
+intros; apply projT2.
 
-clear H1.
-intro H1.
-right.
-exists a.
-exact H1.
 Qed.
 *)
 
-lemma ta_apfun : \forall A, B : CSetoid. tight_apart (CSetoid_fun A B) (eq_fun A B) (ap_fun A B).
-unfold tight_apart.
-intros (A B f g).
-unfold ap_fun.
-unfold eq_fun.
-split
-[ intros. 
-  apply not_ap_imp_eq.unfold.intro.auto.
- |intros. unfold.intro.elim H1.
-  apply (ap_imp_neq B ? ? H2). auto.
-]
+lemma extension_wd :\forall S:CSetoid. \forall P: S \to Prop. 
+  \forall R : (\forall x:S. P x \to Prop).  
+  pred_wd ? P \to
+ (\forall (x,y : S).\forall Hx : (P x). 
+ \forall Hy : (P y). x = y \to R x Hx \to R y Hy) \to 
+  pred_wd ? (extend S P R) .
+intros (S P R H H0).
+unfold.
+intros (x y H1 H2).
+elim H1;split[apply (H x).assumption. exact H2|
+  intro H5.apply (H0 x ? t)[apply H2|apply t1]
+  ]
+qed.
+
+(*End Extension. *)
+
+(*End SubSets_of_G.*)
+
+(* Notation Conj := (conjP _).
+Implicit Arguments disj [S].
+
+Implicit Arguments extend [S].
+Implicit Arguments ext1 [S P R x].
+Implicit Arguments ext2 [S P R x].
+*)
+(**Operations
+
+We are now ready to define the concept of partial function between arbitrary setoids.
+*)
+lemma block : \forall y:nat. \forall x:nat. y = x \to x = y.
+intros.
+symmetry.exact H.
+qed.
+
+record BinPartFunct (S1, S2 : CSetoid) : Type \def 
+  {bpfdom  :  S1 \to Type;
+   bdom_wd :  pred_wd S1 bpfdom;
+   bpfpfun :> \forall x : S1. (bpfdom x) \to S2;
+   bpfstrx :  \forall x,y,Hx,Hy.
+    bpfpfun x Hx ≠ bpfpfun y Hy \to (x \neq y)}.
+
+(* Notation BDom := (bpfdom _ _).
+Implicit Arguments bpfpfun [S1 S2]. *)
+
+(*
+The next lemma states that every partial function is well defined.
+*)
+
+lemma bpfwdef: \forall S1,S2 : CSetoid. \forall F : (BinPartFunct S1 S2). 
+  \forall x,y,Hx,Hy.
+ x = y \to (bpfpfun S1 S2 F x Hx ) = (bpfpfun S1 S2 F y Hy).
+intros.
+apply not_ap_imp_eq;unfold. intro H0.
+generalize in match (bpfstrx ? ? ? ? ? ? ? H0).
+exact (eq_imp_not_ap ? ? ? H).
+qed.
+
+(* Similar for automorphisms. *)
+
+record PartFunct (S : CSetoid) : Type \def 
+  {pfdom  :  S -> Type;
+   dom_wd :  pred_wd S pfdom;
+   pfpfun :> \forall x : S. pfdom x \to S;
+   pfstrx :  \forall x, y, Hx, Hy. pfpfun x Hx \neq pfpfun y Hy \to x \neq y}.
+
+
+(* Notation Dom := (pfdom _).
+Notation Part := (pfpfun _).
+Implicit Arguments pfpfun [S]. *)
+
+(*
+The next lemma states that every partial function is well defined.
+*)
+
+lemma pfwdef : \forall S:CSetoid. \forall F : PartFunct S. \forall x, y, Hx, Hy.
+   x = y \to (pfpfun S F x Hx ) = (pfpfun S F y Hy).
+intros.
+apply not_ap_imp_eq;unfold. intro H0.
+generalize in match (pfstrx ? ? ? ? ? ? H0).
+exact (eq_imp_not_ap ? ? ? H).
+qed. 
+
+(*
+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(&lang;s,H&rang;)#; 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(&lang;s,H&rang;)# 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.
+*)
+
+(* Hint Resolve CI: core. *)
+
+(* Section CSetoid_Ops.*)
+
+(*Variable S : CSetoid.*)
+
+(*
+To begin with, we want to be able to ``see'' each total function as a partial function.
+*)
+
+definition total_eq_part :\forall S:CSetoid. CSetoid_un_op S \to PartFunct S.
+intros (S f).
+apply (mk_PartFunct ? 
+          (\lambda x : S. True) 
+          ?
+              (\lambda (x : S). \lambda (H : True).(csf_fun ? ? f x))).
+unfold. intros;left.
+intros (x y Hx Hy H).
+exact (csf_strext_unfolded ? ? f ? ? H).
 qed.
+(*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}%
+*)
+
+(*Variable c : S.*)
+
+definition Fconst: \forall S:CSetoid. \forall c: S. ? \def
+  \lambda S:CSetoid. \lambda c: S.
+ total_eq_part ? (Const_CSetoid_fun ? ? c).
+
+(* End Part_Function_Const. *)
+
+(* Section Part_Function_Id. *)
+
+definition Fid : \forall S:CSetoid. ? \def 
+  \lambda S:CSetoid.total_eq_part ? (id_un_op S).
+  
+(* 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}%
+*)
+
+(* Section Part_Function_Composition. *)
+
+(* Variables G F : PartFunct S. *)
+
+(* begin hide *)
+
+definition UP : \forall S:CSetoid. \forall F: PartFunct S. ? \def
+   \lambda S:CSetoid. \lambda F: PartFunct S. 
+   pfdom ? F.
+(* Let P := Dom F. *)
+definition UQ : \forall S:CSetoid. \forall G : PartFunct S. ? \def
+   \lambda S:CSetoid. \lambda G: PartFunct S. 
+   pfdom ? G.
+(* Let Q := Dom G. *)
+definition UR : \forall S:CSetoid.  \forall F,G: PartFunct S. \forall x: S. ? \def 
+  \lambda S:CSetoid. \lambda F,G: PartFunct S. \lambda x: S.  
+  (sigT ? (\lambda Hx : UP S F x. UQ S G (pfpfun S F x Hx))).
+(*Let R x := {Hx : P x | Q (F x Hx)}.*)
+
+(* end hide *)
+
+(* TODO ProjT1 *)
+lemma part_function_comp_strext : \forall S:CSetoid.  \forall F,G: PartFunct S. 
+\forall x,y:S. \forall Hx : UR S F G x. \forall Hy : (UR S F G y).
+ (pfpfun ? G (pfpfun ? F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx)) 
+  \neq (pfpfun ? G (pfpfun ? F y (proj1_sigT ? ? Hy)) (proj2_sigTm ? ? Hy)) \to x \neq y.
+intros (S F G x y Hx Hy H).
+exact (pfstrx ? ? ? ? ? ? (pfstrx ? ? ? ? ? ? H)).
+qed.
+(*
+definition TempR : \forall S:CSetoid.  \forall F,G: PartFunct S. \forall x: S. ? \def 
+  \lambda S:CSetoid. \lambda F,G: PartFunct S. \lambda x: S.  
+  (ex  ? (\lambda Hx : UP S F x. UQ S G (pfpfun S F x Hx))). *)
+  
+lemma part_function_comp_dom_wd :\forall S:CSetoid. \forall F,G: PartFunct S. 
+ pred_wd S (UR S F G).
+  intros.unfold.
+  intros (x y H H0).
+  unfold UR.
+  elim H.
+  unfold in a.
+  unfold UP.unfold UQ.
+  apply (existT).
+  apply (dom_wd S F x y a H0).
+apply (dom_wd S G (pfpfun S F x a)).
+assumption.
+apply pfwdef; assumption.
+qed.
+
+definition Fcomp : \forall S:CSetoid. \forall F,G : PartFunct S. ? \def 
+\lambda S:CSetoid. \lambda F,G : PartFunct S. 
+mk_PartFunct ? (UR S F G) (part_function_comp_dom_wd S F G)  
+(\lambda x. \lambda Hx : UR S F G x. (pfpfun S G (pfpfun S F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ?  Hx)))
+(part_function_comp_strext S F G).
+
+(*End Part_Function_Composition.*)
+
+(*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}%
+*)
+
+(* Section BinPart_Function_Composition.*)
+
+(*Variables S1 S2 S3 : CSetoid.
+
+Variable G : BinPartFunct S2 S3.
+Variable F : BinPartFunct S1 S2.
+*)
+(* begin hide *)
+(* Let P := BDom F.
+Let Q := BDom G.*)
+(* end hide *)
+(*Let R x := {Hx : P x | Q (F x Hx)}.*)
+
+definition BP : \forall S1,S2:CSetoid. \forall F: BinPartFunct S1 S2. ? \def
+   \lambda S1,S2:CSetoid. \lambda F: BinPartFunct S1 S2. 
+   bpfdom ? ? F.
+(* Let P := Dom F. *)
+definition BQ : \forall S2,S3:CSetoid. \forall G: BinPartFunct S2 S3. ? \def
+   \lambda S2,S3:CSetoid. \lambda G: BinPartFunct S2 S3. 
+   bpfdom ? ? G.
+(* Let Q := BDom G.*)
+definition BR : \forall S1,S2,S3:CSetoid.  \forall F: BinPartFunct S1 S2.
+\forall G: BinPartFunct S2 S3.
+  \forall x: ?. ? \def 
+  \lambda S1,S2,S3:CSetoid. \lambda F: BinPartFunct S1 S2.  
+  \lambda G: BinPartFunct S2 S3.  \lambda x: ?.  
+  (sigT  ? (\lambda Hx : BP S1 S2 F x. BQ S2 S3  G (bpfpfun S1 S2 F x Hx))).
+(*Let R x := {Hx : P x | Q (F x Hx)}.*)
+
+lemma bin_part_function_comp_strext : \forall S1,S2,S3:CSetoid. \forall F: BinPartFunct S1 S2.
+\forall G: BinPartFunct S2 S3. \forall x,y. \forall Hx : BR S1 S2 S3 F G x. 
+\forall Hy : (BR S1 S2 S3 F G y). 
+(bpfpfun ? ? G (bpfpfun ? ? F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx)) \neq 
+(bpfpfun ? ? G (bpfpfun ? ? F y (proj1_sigT ? ? Hy)) (proj2_sigTm ? ? Hy)) \to x \neq y.
+intros (S1 S2 S3 x y Hx Hy H).
+exact (bpfstrx ? ? ? ? ? ? ? (bpfstrx ? ? ? ? ? ? ? H1)).
+qed.  
+
+lemma bin_part_function_comp_dom_wd : \forall S1,S2,S3:CSetoid. 
+  \forall F: BinPartFunct S1 S2. \forall G: BinPartFunct S2 S3.
+ pred_wd ? (BR S1 S2 S3 F G).
+intros.
+unfold.intros (x y H H0).
+unfold BR; elim H 0.intros (x0).
+apply (existT ? ? (bdom_wd ? ? F x y x0 H0)).
+apply (bdom_wd ? ? G (bpfpfun ? ? F x x0)).
+assumption.
+apply bpfwdef; assumption.
+qed.
+
+definition BinFcomp : \forall S1,S2,S3:CSetoid. \forall F: BinPartFunct S1 S2. 
+  \forall G: BinPartFunct S2 S3. ?
+\def 
+\lambda S1,S2,S3:CSetoid. \lambda F: BinPartFunct S1 S2. \lambda G: BinPartFunct S2 S3.
+mk_BinPartFunct ? ? (BR S1 S2 S3 F G) (bin_part_function_comp_dom_wd S1 S2 S3 F G)
+  (\lambda x. \lambda Hx : BR S1 S2 S3 F G x.(bpfpfun ? ? G (bpfpfun ? ? F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx)))
+  (bin_part_function_comp_strext S1 S2 S3 F G).
+(*End BinPart_Function_Composition.*)
+(* Different tokens for compatibility with coqdoc *)
+
+(*
+Implicit Arguments Fconst [S].
+Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
+
+Notation FId := (Fid _).
+
+Implicit Arguments Fcomp [S].
+Infix "[o]" := Fcomp (at level 65, no associativity).
+
+Hint Resolve pfwdef bpfwdef: algebra.
+*)
+(*Section bijections.*)
+(*Bijections *)
+
+
+definition injective : \forall  A, B :CSetoid. \forall f : CSetoid_fun A B.
+ ? \def 
+  \lambda  A, B :CSetoid. \lambda f : CSetoid_fun A B.
+  (\forall a0: A.\forall a1 : A. a0 \neq a1 \to 
+                    (csf_fun A B f a0) \neq (csf_fun A B f a1)).
+  
+definition injective_weak: \forall  A, B :CSetoid. \forall f : CSetoid_fun A B.
+ ? \def 
+ \lambda  A, B :CSetoid. \lambda f : CSetoid_fun A B.
+ (\forall a0, a1 : A.
+ (csf_fun ? ? f a0) = (csf_fun ? ? f a1) -> a0 = a1).
+
+definition surjective : \forall  A, B :CSetoid. \forall f : CSetoid_fun A B.
+  ? \def 
+  \lambda  A, B :CSetoid. \lambda f : CSetoid_fun A B.
+  (\forall b : B. (\exists a : A. (csf_fun ? ? f a) = b)).
+
+(* Implicit Arguments injective [A B].
+   Implicit Arguments injective_weak [A B].
+   Implicit Arguments surjective [A B]. *)
+
+lemma injective_imp_injective_weak: \forall A, B :CSetoid. \forall f : CSetoid_fun A B.
+ injective A B f \to injective_weak A B f.
+intros 3 (A B f).
+unfold injective.
+intro H.
+unfold injective_weak.
+intros 3 (a0 a1 H0).
+apply not_ap_imp_eq.
+unfold.
+intro H1.
+letin H2 \def (H a0 a1 H1).
+letin H3 \def (ap_imp_neq B (csf_fun ? ? f a0) (csf_fun ? ? f a1) H2).
+letin H4 \def (eq_imp_not_neq B (csf_fun ? ? f a0) (csf_fun ? ? f a1) H0).
+apply H4.
+exact H3.
+qed.
+
+definition bijective : \forall A, B :CSetoid. \forall f : CSetoid_fun A B. 
+? \def \lambda A, B :CSetoid. \lambda f : CSetoid_fun A B.
+injective A B f \and surjective A B f.
+
+
+(* Implicit Arguments bijective [A B]. *)
+
+lemma id_is_bij : \forall A:CSetoid. bijective ? ? (id_un_op A).
+intro A.
+split [unfold. simplify; intros. exact H|
+unfold.intro. apply (ex_intro  ).exact b. apply eq_reflexive]
+qed.
+
+lemma comp_resp_bij :\forall A,B,C,f,g.
+ bijective ? ? f \to bijective ? ? g \to bijective ? ? (compose_CSetoid_fun A B C f g).
+intros 5 (A B C f g).
+intros 2 (H0 H1).
+elim H0 0; clear H0;intros 2 (H00 H01).
+elim H1 0; clear H1; intros 2 (H10 H11).
+split[unfold. intros 2 (a0 a1); simplify; intro.
+unfold compose_CSetoid_fun.simplify.
+ apply H10; apply H00;exact H|unfold.
+ intro c; unfold compose_CSetoid_fun.simplify.
+elim (H11 c) 0;intros (b H20).
+elim (H01 b) 0.intros (a H30).
+apply ex_intro.apply a.
+apply (eq_transitive_unfolded ? ? (csf_fun B C g b)).
+apply csf_wd_unfolded.assumption.assumption]
+qed.
+
+(* Implicit Arguments invfun [A B]. *)
+
+record CSetoid_bijective_fun (A,B:CSetoid): Type \def
+{ direct :2> CSetoid_fun A B;
+  inverse: CSetoid_fun B A;
+  inv1: \forall x:A.(csf_fun ? ? inverse (csf_fun ? ? direct x)) = x;
+  inv2: \forall x:B.(csf_fun ? ? direct (csf_fun ? ? inverse x)) = x
+  }. 
+   
+lemma invfun : \forall A,B:CSetoid. \forall f:CSetoid_bijective_fun A B. 
+  B \to A.
+ intros (A B f ).
+ elim (inverse A B f).apply f1.apply c.
+qed.
+
+lemma inv_strext : \forall A,B. \forall f : CSetoid_bijective_fun A B.
+ fun_strext B A (invfun A B f).
+intros.unfold invfun.
+elim (inverse A B f).simplify.intros.
+unfold in H.apply H.assumption.
+qed.
+
+
+
+definition Inv: \forall  A, B:CSetoid. 
+\forall f:CSetoid_bijective_fun A B. \forall H : (bijective ? ? (direct ? ? f)). ? \def 
+\lambda  A, B:CSetoid. \lambda f:CSetoid_bijective_fun A B. \lambda H : (bijective ? ? (direct ? ? f)).
+  mk_CSetoid_fun B A (invfun ? ? f) (inv_strext ? ?  f).
+
+lemma eq_to_ap_to_ap: \forall A:CSetoid.\forall a,b,c:A.
+a = b \to b \neq c \to a \neq c.
+intros.
+generalize in match (ap_cotransitive_unfolded ? ? ? H1 a).
+intro.elim H2.apply False_ind.apply (eq_imp_not_ap ? ? ? H).
+auto.assumption.
+qed.
+
+lemma Dir_bij : \forall A, B:CSetoid. 
+ \forall f : CSetoid_bijective_fun A B.
+  bijective ? ? (direct ? ? f).
+  intros.unfold bijective.split
+  [unfold injective.intros.
+  apply (csf_strext_unfolded ? ? (inverse ? ? f)).
+  elim f.
+  apply (eq_to_ap_to_ap ? ? ? ? (H1 ?)).
+  apply ap_symmetric_unfolded.
+  apply (eq_to_ap_to_ap ? ? ? ? (H1 ?)).
+  apply ap_symmetric_unfolded.assumption
+  |unfold surjective.intros.
+   elim f.auto.
+  ]
+qed.
+   
+lemma Inv_bij : \forall A, B:CSetoid. 
+ \forall f : CSetoid_bijective_fun A B.
+  bijective ? ?  (inverse A B f).
+ intros;
+ elim f 2;
+ elim c2 0;
+ elim c3 0;
+ simplify;
+ intros;
+ split;
+  [ intros;
+    apply H1;
+    apply (eq_to_ap_to_ap ? ? ? ? (H3 ?)).
+  apply ap_symmetric_unfolded.
+  apply (eq_to_ap_to_ap ? ? ? ? (H3 ?)).
+  apply ap_symmetric_unfolded.assumption|
+  intros.auto]
+qed.
+
+(* End bijections.*)
+
+(* Implicit Arguments bijective [A B].
+Implicit Arguments injective [A B].
+Implicit Arguments injective_weak [A B].
+Implicit Arguments surjective [A B].
+Implicit Arguments inv [A B].
+Implicit Arguments invfun [A B].
+Implicit Arguments Inv [A B].
+
+Implicit Arguments conj_wd [S P Q].
+*)
 
+(* Notation Prj1 := (prj1 _ _ _ _).
+   Notation Prj2 := (prj2 _ _ _ _). *)
index a06c43ab8b367d1af3de6169c8478f4c9332d7f6..cfc6f524e63b48492c88c0ec3330b56f46d3cd4c 100644 (file)
@@ -92,6 +92,8 @@ generalize in match (ap_irreflexive S x);
 elim H. apply H1. assumption.
 qed.
 
+axiom eq_symmetric : \forall S : CSetoid. symmetric S (cs_eq S).
+(*
 lemma eq_symmetric : \forall S : CSetoid. symmetric S (cs_eq S).
 intro. unfold. intros.
 generalize in match (ap_tight S x y). intro.
@@ -101,7 +103,7 @@ elim H1. clear H1.
 elim H2. clear H2.
 apply H1. unfold. intro. auto.
 qed.
-
+*)
 lemma eq_transitive : \forall S : CSetoid. transitive S (cs_eq S).
 intro. unfold. intros (x y z H H0).
 generalize in match (ap_tight S x y). intro.
@@ -130,13 +132,17 @@ lemma eq_transitive_unfolded : \forall S:CSetoid. \forall x,y,z:S. x = y \to y =
 apply eq_transitive.
 qed.
 
+
 lemma eq_wdl : \forall S:CSetoid. \forall x,y,z:S. x = y \to x = z \to z = y.
 intros.
 (* perche' auto non arriva in fondo ??? *)
-apply (eq_transitive_unfolded ? ? x). auto.
-assumption.
+apply (eq_transitive_unfolded ? ? x).
+apply eq_symmetric_unfolded.
+exact H1.
+exact H.
 qed.
 
+
 lemma ap_irreflexive_unfolded : \forall S:CSetoid. \forall x:S. \not (x \neq x).
 apply ap_irreflexive.
 qed.
@@ -318,8 +324,8 @@ definition pred_strong_ext : \forall S: CSetoid. (S \to Prop) \to Prop \def
   P x \to (P y \or (x \neq y)).
 
 (* Definition pred_wd : CProp := forall x y : S, P x -> x [=] y -> P y. *)
-definition pred_wd : \forall S: CSetoid. (S \to Prop) \to Prop \def 
- \lambda S: CSetoid. \lambda P: S \to Prop. \forall x,y : S. 
+definition pred_wd : \forall S: CSetoid. \forall P :S \to Type. Type \def
+ \lambda S: CSetoid. \lambda P: S \to Type. \forall x,y : S. 
   P x \to x = y \to P y.
 
 record wd_pred (S: CSetoid) : Type \def
@@ -720,7 +726,7 @@ qed.
 
 
 record CSetoid_bin_fun (S1,S2,S3: CSetoid) : Type \def 
- {csbf_fun    : S1 \to S2 \to S3;
+ {csbf_fun    :2> S1 \to S2 \to S3;
   csbf_strext :  (bin_fun_strext S1 S2 S3 csbf_fun)}.
 
 lemma csbf_wd : \forall S1,S2,S3: CSetoid. \forall f : CSetoid_bin_fun S1 S2 S3. 
@@ -761,7 +767,7 @@ definition commutes : \forall S: CSetoid. (S \to S \to S)  \to Prop \def
  \lambda S: CSetoid. \lambda f : S \to S \to S. 
  \forall x,y : S. f x y = f y x.
  
-definition associative : \forall S: CSetoid. (S \to S \to S) \to Prop \def 
+definition CSassociative : \forall S: CSetoid. \forall f: S \to S \to S.  Prop \def 
 \lambda S: CSetoid. \lambda f : S \to S \to S. 
 \forall x,y,z : S.
  f x (f y z) = f (f x y) z.
@@ -783,15 +789,18 @@ definition mk_CSetoid_un_op : \forall S:CSetoid. \forall f: S \to S. fun_strext
 
 lemma id_strext : \forall S:CSetoid. un_op_strext S (\lambda x:S. x).
 unfold un_op_strext.
-unfold fun_strext.intros.
-simplify.assumption.
+unfold fun_strext.
+intros.
+simplify in H.
+exact H.
 qed.
 
 lemma id_pres_eq : \forall S:CSetoid. un_op_wd S (\lambda x : S.x).
 unfold un_op_wd.
 unfold fun_wd.
 intros.
-simplify.assumption.
+simplify.
+exact H.
 qed.
 
 definition id_un_op : \forall S:CSetoid. CSetoid_un_op S 
@@ -1047,12 +1056,17 @@ intros. unfold equiv. split
 ]
 qed.
 
+(*
+axiom subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop. 
+is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
+*)
+
 lemma subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop. 
 is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
 intros.
 apply (mk_is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P))
 [ unfold. intros.unfold. elim x. exact (ap_irreflexive_unfolded S ? ?) 
- [ assumption | apply H1.]
+ [ assumption | simplify in H1. exact H1 ]
  (* irreflexive *)
 |unfold. intros 2. elim x. generalize in match H1. elim y.simplify in H3. simplify.
 exact (ap_symmetric ? ? ? H3)
@@ -1064,6 +1078,7 @@ apply (ap_cotransitive ? ? ? H3)
 apply (ap_tight S ? ?)]
 qed.
 
+
 definition mk_SubCSetoid : \forall S:CSetoid. \forall P: S \to Prop. CSetoid \def 
 \lambda S:CSetoid. \lambda P:S \to Prop.
 mk_CSetoid (subcsetoid_crr S P) (subcsetoid_eq S P) (subcsetoid_ap S P) (subcsetoid_is_CSetoid S P).
@@ -1113,12 +1128,18 @@ apply (cs_un_op_strext ? f ? ? H2).
 qed.
 
 definition mk_SubCSetoid_un_op : \forall S:CSetoid. \forall P: S \to Prop. \forall f: CSetoid_un_op S.
- \forall pr:un_op_pres_pred S P f.
- CSetoid_un_op (mk_SubCSetoid S P) \def
+ \forall pr:un_op_pres_pred S P f. CSetoid_un_op (mk_SubCSetoid S P).
+ intros (S P f pr).
+ apply (mk_CSetoid_un_op (mk_SubCSetoid S P) (restr_un_op S P f pr) (restr_un_op_strext S P f pr)).
+ qed.
+
+(* BUG Universe Inconsistency detected 
+ definition mk_SubCSetoid_un_op : \forall S:CSetoid. \forall P: S \to Prop. \forall f: CSetoid_un_op S.
+ \forall pr:un_op_pres_pred S P f. CSetoid_un_op (mk_SubCSetoid S P) \def
  \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
   \lambda pr:un_op_pres_pred S P f.
   mk_CSetoid_un_op (mk_SubCSetoid S P) (restr_un_op S P f pr) (restr_un_op_strext S P f pr).
-
+*)
 
 (* Subsetoid binary operations
 Let [f] be a binary setoid operation on [S].
@@ -1175,17 +1196,26 @@ reduce in H4.
 apply (cs_bin_op_strext ? f ? ? ? ? H4).
 qed.
 
+definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop. 
+  \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f. 
+  CSetoid_bin_op (mk_SubCSetoid S P).
+  intros (S P f pr).
+  apply (mk_CSetoid_bin_op (mk_SubCSetoid S P) (restr_bin_op S P f pr)(restr_bin_op_strext S P f pr)).
+  qed.
+
+(* BUG Universe Inconsistency detected 
 definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop. 
   \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f. 
   CSetoid_bin_op (mk_SubCSetoid S P) \def
   \lambda S:CSetoid. \lambda P: S \to Prop. 
   \lambda f: CSetoid_bin_op S. \lambda pr: bin_op_pres_pred S P f.
     mk_CSetoid_bin_op (mk_SubCSetoid S P) (restr_bin_op S P f pr)(restr_bin_op_strext S P f pr).
+*)
 
 lemma restr_f_assoc : \forall S:CSetoid. \forall P: S \to Prop. 
   \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
-    associative S (csbf_fun S S S f) 
-    \to associative (mk_SubCSetoid S P) (csbf_fun (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid_bin_op S P f pr)).
+    CSassociative S (csbf_fun S S S f) 
+    \to CSassociative (mk_SubCSetoid S P) (csbf_fun (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid_bin_op S P f pr)).
 intros 4.
 intro.
 unfold.
@@ -1210,6 +1240,8 @@ elim n.elim m.simplify. reflexivity.reflexivity.
 elim m.simplify.reflexivity.reflexivity.
 qed.
 
+
+
 lemma proper_caseZ_diff_CS : \forall CS : CSetoid. \forall f : nat \to nat \to CS.
  (\forall m,n,p,q : nat. eq nat (plus m q) (plus n p) \to (f m n) = (f p q)) \to
  \forall m,n : nat. caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = (f m n).
@@ -1231,8 +1263,9 @@ apply f. apply n1. apply m1.
 apply eq_symmetric_unfolded.assumption.
 apply eq_symmetric_unfolded.assumption.
 apply H.
-auto.
+auto new.
 qed.
+
 (*
 Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
 *)