--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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. *)
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.
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(⟨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.
+*)
+
+(* 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 _ _ _ _). *)
projects / helm.git / commitdiff