--- /dev/null
+include ../Makefile.defs
+
+DIR=$(shell basename $$PWD)
+
+$(DIR) all:
+ $(BIN)matitac
+$(DIR).opt opt all.opt:
+ $(BIN)matitac.opt
+clean:
+ $(BIN)matitaclean
+clean.opt:
+ $(BIN)matitaclean.opt
+depend:
+ $(BIN)matitadep
+depend.opt:
+ $(BIN)matitadep.opt
--- /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).
+autobatch.
+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 autobatchmorphisms; 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 a|elim Hy.apply a|exact H1]|
+apply pfstrx[apply F'|elim Hx.apply b|elim Hy.apply b|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
+ [pair (x1: (cs_crr (csg_crr M1))) (x2: (cs_crr (csg_crr M2))) \Rightarrow
+ match y with
+ [pair (y1: (cs_crr (csg_crr M1))) (y2: (cs_crr (csg_crr M2))) \Rightarrow
+ pair (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. *)
--- /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: CSetoidFun.v,v 1.12 2004/09/22 11:06:10 loeb Exp $ *)
+
+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.
+ \exists a:A. (csf_fun A B f) a \neq (csf_fun A B g) a.
+(* Definition ap_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
+ {a : A | f a[#]g a}. *)
+
+definition eq_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.
+ \forall a:A. (csf_fun A B f) a = (csf_fun A B g) a.
+(* Definition eq_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
+ forall a : A, f a[=]g a. *)
+
+lemma irrefl_apfun : \forall A,B : CSetoid.
+ irreflexive (CSetoid_fun A B) (ap_fun A B).
+intros.
+unfold irreflexive. intro f.
+unfold ap_fun.
+unfold.
+intro.
+elim H.
+cut (csf_fun A B f a = csf_fun A B f a)
+[ 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 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).
+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.
+
+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).
+
+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 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.
+apply a.
+apply Hg2.
+exact H0.
+qed.
+
+
+(* Questa coercion composta non e' stata generata autobatchmaticamente *)
+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]; autobatch.
+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 a.
+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.
+autobatch |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.autobatch|simplify.intros.exact H1]|
+intros (a at).
+simplify.
+split[intro.autobatch|intros. exact H1]
+]
+|
+intros (a at IHx).
+elim y 0[simplify.
+ split[intro.autobatch|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 ? a).assumption|apply (f1 x ? b). 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.
+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].
+*)
+
+(*
+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 (b a).
+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.
+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.
+
+Qed.
+*)
+
+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 ? a)[apply H2|apply b]
+ ]
+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 autobatchmorphisms. *)
+
+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).
+apply ap_symmetric_unfolded. assumption.
+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.autobatch.
+ ]
+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 c 0;
+ elim c1 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.autobatch]
+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 _ _ _ _). *)
--- /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 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/algebra/CoRN/SetoidInc".
+include "algebra/CoRN/SetoidFun.ma".
+
+(* $Id: CSetoidInc.v,v 1.3 2004/04/22 14:49:43 lcf Exp $ *)
+
+(* printing included %\ensuremath{\subseteq}% #⊆# *)
+
+(* Section inclusion. *)
+
+(* Inclusion
+
+Let [S] be a setoid, and [P], [Q], [R] be predicates on [S]. *)
+
+(* Variable S : CSetoid. *)
+
+definition included : \forall S : CSetoid. \forall P,Q : S \to Type. Type \def
+ \lambda S : CSetoid. \lambda P,Q : S \to Type.
+ \forall x : S. P x \to Q x.
+
+(* Section Basics. *)
+
+(* Variables P Q R : S -> CProp. *)
+lemma included_refl : \forall S : CSetoid. \forall P : S \to Type.
+ included S P P.
+intros.
+unfold.
+intros.
+assumption.
+qed.
+
+lemma included_trans : \forall S : CSetoid. \forall P,Q,R : S \to Type.
+ included S P Q \to included S Q R \to included S P R.
+intros.
+unfold.
+intros.
+apply i1.
+apply i.
+assumption.
+qed.
+
+lemma included_conj : \forall S : CSetoid. \forall P,Q,R : S \to Type.
+ included S P Q \to included S P R \to included S P (conjP S Q R).
+intros 4.
+unfold included.
+intros;
+unfold.
+split [apply f.assumption|apply f1.assumption]
+qed.
+
+lemma included_conj' : \forall S : CSetoid. \forall P,Q,R : S \to Type.
+ included S (conjP S P Q) P.
+ intros.
+exact (prj1 S P Q).
+qed.
+
+lemma included_conj'' : \forall S : CSetoid. \forall P,Q,R : S \to Type.
+ included S (conjP S P Q) Q.
+ intros.
+exact (prj2 S P Q).
+qed.
+
+lemma included_conj_lft : \forall S : CSetoid. \forall P,Q,R : S \to Type.
+ included S R (conjP S P Q) -> included S R P.
+intros 4.
+unfold included.
+unfold conjP.intros (f1 x H2).
+elim (f1 x ); assumption.
+qed.
+
+lemma included_conj_rht : \forall S : CSetoid. \forall P,Q,R : S \to Type.
+ included S R (conjP S P Q) \to included S R Q.
+ intros 4.
+ unfold included.
+ unfold conjP.
+intros (H1 x H2).
+elim (H1 x); assumption.
+qed.
+lemma included_extend : \forall S : CSetoid. \forall P,Q,R : S \to Type.
+ \forall H : \forall x. P x \to Type.
+ included S R (extend S P H) \to included S R P.
+intros 4.
+intros (H0 H1).
+unfold.
+unfold extend in H1.
+intros.
+elim (H1 x);assumption.
+qed.
+
+
+(* End Basics. *)
+
+(*
+%\begin{convention}% Let [I,R:S->CProp] and [F G:(PartFunct S)], and denote
+by [P] and [Q], respectively, the domains of [F] and [G].
+%\end{convention}%
+*)
+
+(* Variables F G : (PartFunct S). *)
+
+(* begin hide *)
+(* Let P := Dom F. *)
+(* Let Q := Dom G. *)
+(* end hide *)
+
+(* Variable R : S -> CProp. *)
+lemma included_FComp : \forall S : CSetoid. \forall F,G: PartFunct S.
+\forall R : S \to Type.
+ included S R (UP ? F) \to (\forall x: S. \forall Hx. (R x) \to UQ ? G (pfpfun ? F x Hx)) \to
+ included S R (pfdom ? (Fcomp ? F G)).
+intros (S F G R HP HQ).
+unfold Fcomp.
+simplify.
+unfold included. intros (x Hx).
+apply (existT ? ? (HP x Hx)).
+apply HQ.
+assumption.
+qed.
+
+lemma included_FComp': \forall S : CSetoid. \forall F,G: PartFunct S.
+\forall R : S \to Type.
+included S R (pfdom ? (Fcomp ? F G)) \to included S R (UP ? F).
+intros (S F G R H).
+unfold Fcomp in H.
+simplify in H.
+unfold. intros (x Hx).
+elim (H x Hx);
+assumption.
+qed.
+
+(* End inclusion. *)
+
+(* Implicit Arguments included [S].
+
+Hint Resolve included_refl included_FComp : included.
+
+Hint Immediate included_trans included_FComp' : included. *)
--- /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 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/algebra/CoRN/Setoid".
+
+
+include "higher_order_defs/relations.ma".
+include "Z/plus.ma".
+
+include "datatypes/constructors.ma".
+include "nat/nat.ma".
+include "logic/equality.ma".
+(*include "Z/Zminus.ma".*)
+
+(* Setoids
+Definition of a constructive setoid with apartness,
+i.e. a set with an equivalence relation and an apartness relation compatible with it.
+*)
+
+(* Definition of Setoid
+Apartness, being the main relation, needs to be [CProp]-valued. Equality,
+as it is characterized by a negative statement, lives in [Prop].
+
+N.B. for the moment we use Prop for both (Matita group)
+*)
+
+record is_CSetoid (A : Type) (eq : relation A) (ap : relation A) : Prop \def
+ {ax_ap_irreflexive : irreflexive A ap;
+ ax_ap_symmetric : symmetric A ap;
+ ax_ap_cotransitive : cotransitive A ap;
+ ax_ap_tight : tight_apart A eq ap}.
+
+record CSetoid : Type \def
+ {cs_crr :> Type;
+ cs_eq : relation cs_crr;
+ cs_ap : relation cs_crr;
+ cs_proof : is_CSetoid cs_crr cs_eq cs_ap}.
+
+interpretation "setoid equality"
+ 'eq x y = (cic:/matita/algebra/CoRN/Setoids/cs_eq.con _ x y).
+
+interpretation "setoid apart"
+ 'neq x y = (cic:/matita/algebra/CoRN/Setoids/cs_ap.con _ x y).
+
+(* visto che sia "ap" che "eq" vanno in Prop e data la "tight-apartness",
+"cs_neq" e "ap" non sono la stessa cosa? *)
+definition cs_neq : \forall S : CSetoid. relation S \def
+ \lambda S : CSetoid. \lambda x,y : S. \not x = y.
+
+lemma CSetoid_is_CSetoid :
+ \forall S : CSetoid. is_CSetoid S (cs_eq S) (cs_ap S).
+intro. apply (cs_proof S).
+qed.
+
+lemma ap_irreflexive: \forall S : CSetoid. irreflexive S (cs_ap S).
+intro. elim (CSetoid_is_CSetoid S). assumption.
+qed.
+
+lemma ap_symmetric : \forall S : CSetoid. symmetric S(cs_ap S).
+intro. elim (CSetoid_is_CSetoid S). assumption.
+qed.
+
+lemma ap_cotransitive : \forall S : CSetoid. cotransitive S (cs_ap S).
+intro. elim (CSetoid_is_CSetoid S). assumption.
+qed.
+
+lemma ap_tight : \forall S : CSetoid. tight_apart S (cs_eq S) (cs_ap S).
+intro. elim (CSetoid_is_CSetoid S). assumption.
+qed.
+
+definition ex_unq : \forall S : CSetoid. (S \to Prop) \to Prop \def
+ \lambda S : CSetoid. \lambda P : S \to Prop.
+ ex2 S (\lambda x. \forall y : S. P y \to x = y) P.
+
+
+lemma eq_reflexive : \forall S : CSetoid. reflexive S (cs_eq S).
+intro. unfold. intro.
+generalize in match (ap_tight S x x).
+intro.
+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.
+generalize in match (ap_tight S y x). intro.
+generalize in match (ap_symmetric S y x). intro.
+elim H1. clear H1.
+elim H2. clear H2.
+apply H1. unfold. intro. autobatch.
+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.
+generalize in match (ap_tight S y z). intro.
+generalize in match (ap_tight S x z). intro.
+elim H3.
+apply H4. unfold. intro.
+generalize in match (ap_cotransitive ? ? ? H6 y). intro H7.
+elim H1 (H1' H1''). clear H1.
+elim H2 (H2' H2''). clear H2.
+elim H3 (H3' H3''). clear H3.
+elim H7 (H1). clear H7.
+generalize in match H1. apply H1''. assumption. (*non ho capito il secondo passo*)
+generalize in match H1. apply H2''. assumption.
+qed.
+
+lemma eq_reflexive_unfolded : \forall S:CSetoid. \forall x:S. x = x.
+apply eq_reflexive.
+qed.
+
+lemma eq_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S. x = y \to y = x.
+apply eq_symmetric.
+qed.
+
+lemma eq_transitive_unfolded : \forall S:CSetoid. \forall x,y,z:S. x = y \to y = z \to x = z.
+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' autobatch non arriva in fondo ??? *)
+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.
+
+lemma ap_cotransitive_unfolded : \forall S:CSetoid. \forall a,b:S. a \neq b \to
+ \forall c:S. a \neq c \or c \neq b.
+apply ap_cotransitive.
+qed.
+
+lemma ap_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S.
+ x \neq y \to y \neq x.
+apply ap_symmetric.
+qed.
+
+lemma eq_imp_not_ap : \forall S:CSetoid. \forall x,y:S.
+ x = y \to \not (x \neq y).
+intros.
+elim (ap_tight S x y).
+apply H2. assumption.
+qed.
+
+lemma not_ap_imp_eq : \forall S:CSetoid. \forall x,y:S.
+ \not (x \neq y) \to x = y.
+intros.
+elim (ap_tight S x y).
+apply H1. assumption.
+qed.
+
+lemma neq_imp_notnot_ap : \forall S:CSetoid. \forall x,y:S.
+ (cs_neq S x y) \to \not \not (x \neq y).
+intros. unfold. intro.
+apply H.
+apply not_ap_imp_eq.
+assumption.
+qed.
+
+lemma notnot_ap_imp_neq: \forall S:CSetoid. \forall x,y:S.
+ (\not \not (x \neq y)) \to (cs_neq S x y).
+intros. unfold. unfold. intro.
+apply H.
+apply eq_imp_not_ap.
+assumption.
+qed.
+
+lemma ap_imp_neq : \forall S:CSetoid. \forall x,y:S.
+ x \neq y \to (cs_neq S x y).
+intros. unfold. unfold. intro.
+apply (eq_imp_not_ap S ? ? H1).
+assumption.
+qed.
+
+lemma not_neq_imp_eq : \forall S:CSetoid. \forall x,y:S.
+ \not (cs_neq S x y) \to x = y.
+intros.
+apply not_ap_imp_eq.
+unfold. intro.
+apply H.
+apply ap_imp_neq.
+assumption.
+qed.
+
+lemma eq_imp_not_neq : \forall S:CSetoid. \forall x,y:S.
+ x = y \to \not (cs_neq S x y).
+intros. unfold. intro.
+apply H1.
+assumption.
+qed.
+
+
+
+(* -----------------The product of setoids----------------------- *)
+
+definition prod_ap: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def
+\lambda A,B : CSetoid.\lambda c,d: Prod A B.
+ ((cs_ap A (fst A B c) (fst A B d)) \or
+ (cs_ap B (snd A B c) (snd A B d))).
+
+definition prod_eq: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def
+\lambda A,B : CSetoid.\lambda c,d: Prod A B.
+ ((cs_eq A (fst A B c) (fst A B d)) \and
+ (cs_eq B (snd A B c) (snd A B d))).
+
+
+lemma prodcsetoid_is_CSetoid: \forall A,B: CSetoid.
+ is_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B).
+intros.
+apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
+ [unfold.
+ intros.
+ elim x.
+ unfold.
+ unfold prod_ap. simplify.
+ intros.
+ elim H
+ [apply (ap_irreflexive A a H1)
+ |apply (ap_irreflexive B b H1)
+ ]
+ |unfold.
+ intros 2.
+ elim x 2.
+ elim y 2.
+ unfold prod_ap. simplify.
+ intro.
+ elim H
+ [left. apply ap_symmetric. assumption.
+ |right. apply ap_symmetric. assumption
+ ]
+ |unfold.
+ intros 2.
+ elim x 2.
+ elim y 4.
+ elim z.
+ unfold prod_ap in H. simplify in H.
+ unfold prod_ap. simplify.
+ elim H
+ [cut ((a \neq a2) \or (a2 \neq a1))
+ [elim Hcut
+ [left. left. assumption
+ |right. left. assumption
+ ]
+ |apply (ap_cotransitive A). assumption
+ ]
+ |cut ((b \neq b2) \or (b2 \neq b1))
+ [elim Hcut
+ [left. right. assumption
+ |right. right. assumption
+ ]
+ |apply (ap_cotransitive B). assumption.
+ ]
+ ]
+|unfold.
+ intros 2.
+ elim x 2.
+ elim y 2.
+ unfold prod_ap. simplify.
+ split
+ [intro.
+ left
+ [apply not_ap_imp_eq.
+ unfold. intro. apply H.
+ left. assumption
+ |apply not_ap_imp_eq.
+ unfold. intro. apply H.
+ right. assumption
+ ]
+ |intro. unfold. intro.
+ elim H.
+ elim H1
+ [apply (eq_imp_not_ap A a a1 H2). assumption
+ |apply (eq_imp_not_ap B b b1 H3). assumption
+ ]
+ ]
+]
+qed.
+
+
+definition ProdCSetoid : \forall A,B: CSetoid. CSetoid \def
+ \lambda A,B: CSetoid.
+ mk_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).
+
+
+
+(* Relations and predicates
+Here we define the notions of well-definedness and strong extensionality
+on predicates and relations.
+*)
+
+
+
+(*-----------------------------------------------------------------------*)
+(*-------------------------- Predicates on Setoids ----------------------*)
+(*-----------------------------------------------------------------------*)
+
+(* throughout this section consider (S : CSetoid) and (P : S -> Prop) *)
+
+(* Definition pred_strong_ext : CProp := forall x y : S, P x -> P y or x [#] y. *)
+definition pred_strong_ext : \forall S: CSetoid. (S \to Prop) \to Prop \def
+ \lambda S: CSetoid. \lambda P: S \to Prop. \forall x,y: S.
+ 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. \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
+ {wdp_pred :> S \to Prop;
+ wdp_well_def : pred_wd S wdp_pred}.
+
+record CSetoid_predicate (S: CSetoid) : Type \def
+ {csp_pred :> S \to Prop;
+ csp_strext : pred_strong_ext S csp_pred}.
+
+lemma csp_wd : \forall S: CSetoid. \forall P: CSetoid_predicate S.
+ pred_wd S (csp_pred S P).
+intros.
+elim P.
+simplify.unfold pred_wd.
+intros.
+elim (H x y H1)
+ [assumption|apply False_ind.apply (eq_imp_not_ap S x y H2 H3)]
+qed.
+
+
+(* Same result with CProp instead of Prop: but we just work with Prop (Matita group) *)
+(*
+Definition pred_strong_ext' : CProp := forall x y : S, P x -> P y or x [#] y.
+Definition pred_wd' : Prop := forall x y : S, P x -> x [=] y -> P y.
+
+Record CSetoid_predicate' : Type :=
+ {csp'_pred :> S -> Prop;
+ csp'_strext : pred_strong_ext' csp'_pred}.
+
+Lemma csp'_wd : forall P : CSetoid_predicate', pred_wd' P.
+intro P.
+intro x; intros y H H0.
+elim (csp'_strext P x y H).
+
+autobatch.
+
+intro H1.
+elimtype False.
+generalize H1.
+exact (eq_imp_not_ap _ _ _ H0).
+Qed.
+*)
+
+
+
+(*------------------------------------------------------------------------*)
+(* --------------------------- Relations on Setoids --------------------- *)
+(*------------------------------------------------------------------------*)
+(* throughout this section consider (S : CSetoid) and (R : S -> S -> Prop) *)
+
+
+(* Definition rel_wdr : Prop := forall x y z : S, R x y -> y [=] z -> R x z. *)
+(*
+ primo tentativo ma R non e' ben tipato: si puo' fare il cast giusto (carrier di S)
+ in modo da sfruttare "relation"?
+ e' concettualmente sbagliato lavorare ad un livello piu' alto (Type) ? *)
+(*
+definition rel_wdr : \forall S: CSetoid. \forall x,y,z: S. \lambda R: relation S. Prop \def
+ \lambda S: CSetoid. \lambda x,y,z: S. \lambda R: relation S.
+ R S x y \to y = z \to R S x z.
+
+definition rel_wdr : \forall S: CSetoid. \forall x,y,z: (cs_crr S). \lambda R: relation (cs_crr S). Prop \def
+ \lambda S: CSetoid. \lambda x,y,z: (cs_crr S). \lambda R: relation (cs_crr S).
+ R (cs_crr S) x y \to y = z \to R (cs_crr S) x z.
+*)
+definition rel_wdr : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
+ \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y,z: S.
+ R x y \to y = z \to R x z.
+
+(*Definition rel_wdl : Prop := forall x y z : S, R x y -> x [=] z -> R z y.*)
+definition rel_wdl : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
+ \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y,z: S.
+ R x y \to x = z \to R z y.
+
+(* Definition rel_strext : CProp := forall x1 x2 y1 y2 : S, R x1 y1 -> (x1 [#] x2 or y1 [#] y2) or R x2 y2. *)
+definition rel_strext : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
+ \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x1,x2,y1,y2: S.
+ R x1 y1 \to (x1 \neq x2 \or y1 \neq y2) \or R x2 y2.
+
+
+(* Definition rel_strext_lft : CProp := forall x1 x2 y : S, R x1 y -> x1 [#] x2 or R x2 y. *)
+definition rel_strext_lft : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
+ \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x1,x2,y: S.
+ R x1 y \to (x1 \neq x2 \or R x2 y).
+
+(* Definition rel_strext_rht : CProp := forall x y1 y2 : S, R x y1 -> y1 [#] y2 or R x y2. *)
+definition rel_strext_rht : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
+ \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y1,y2: S.
+ R x y1 \to (y1 \neq y2 \or R x y2).
+
+
+lemma rel_strext_imp_lftarg : \forall S: CSetoid. \forall R: S \to S \to Prop.
+ rel_strext S R \to rel_strext_lft S R.
+unfold rel_strext.
+unfold rel_strext_lft.
+intros.
+elim (H x1 x2 y y H1)
+[elim H2
+ [left. assumption
+ |absurd (y \neq y) [assumption | apply (ap_irreflexive S y)]
+ ]
+|right. assumption
+]
+qed.
+
+
+lemma rel_strext_imp_rhtarg : \forall S: CSetoid. \forall R: S \to S \to Prop.
+ rel_strext S R \to rel_strext_rht S R.
+unfold rel_strext.
+unfold rel_strext_rht.
+intros.
+elim (H x x y1 y2 H1)
+[elim H2
+ [absurd (x \neq x) [assumption | apply (ap_irreflexive S x)]
+ |left. assumption
+ ]
+|right. assumption
+]
+qed.
+
+
+lemma rel_strextarg_imp_strext : \forall S: CSetoid. \forall R: S \to S \to Prop.
+ (rel_strext_rht S R) \to (rel_strext_lft S R) \to (rel_strext S R).
+unfold rel_strext_rht.
+unfold rel_strext_lft.
+unfold rel_strext.
+intros.
+elim ((H x1 y1 y2) H2)
+[left. right. assumption
+|elim ((H1 x1 x2 y1) H2)
+ [left. left. assumption
+ |elim ((H x2 y1 y2) H4)
+ [left. right. assumption
+ |right. assumption.
+ ]
+ ]
+]
+qed.
+
+(* ---------- Definition of a setoid relation ----------------- *)
+(* The type of relations over a setoid. *)
+
+(* TODO
+record CSetoid_relation1 (S: CSetoid) : Type \def
+ {csr_rel : S \to S \to Prop;
+ csr_wdr : rel_wdr S csr_rel;
+ csr_wdl : rel_wdl S csr_rel;
+ csr_strext : rel_strext S csr_rel}.
+*)
+(* CORN
+Record CSetoid_relation : Type :=
+ {csr_rel :> S -> S -> Prop;
+ csr_wdr : rel_wdr csr_rel;
+ csr_wdl : rel_wdl csr_rel;
+ csr_strext : rel_strext csr_rel}.
+*)
+
+
+(* ---------- gli stessi risultati di prima ma in CProp ---------*)
+(*
+Variable R : S -> S -> CProp.
+Definition Crel_wdr : CProp := forall x y z : S, R x y -> y [=] z -> R x z.
+Definition Crel_wdl : CProp := forall x y z : S, R x y -> x [=] z -> R z y.
+Definition Crel_strext : CProp := forall x1 x2 y1 y2 : S,
+ R x1 y1 -> R x2 y2 or x1 [#] x2 or y1 [#] y2.
+
+Definition Crel_strext_lft : CProp := forall x1 x2 y : S, R x1 y -> R x2 y or x1 [#] x2.
+Definition Crel_strext_rht : CProp := forall x y1 y2 : S, R x y1 -> R x y2 or y1 [#] y2.
+
+Lemma Crel_strext_imp_lftarg : Crel_strext -> Crel_strext_lft.
+Proof.
+unfold Crel_strext, Crel_strext_lft in |- *; intros H x1 x2 y H0.
+generalize (H x1 x2 y y).
+intro H1.
+elim (H1 H0).
+
+autobatch.
+
+intro H3.
+elim H3; intro H4.
+
+autobatch.
+elim (ap_irreflexive _ _ H4).
+Qed.
+
+Lemma Crel_strext_imp_rhtarg : Crel_strext -> Crel_strext_rht.
+unfold Crel_strext, Crel_strext_rht in |- *; intros H x y1 y2 H0.
+generalize (H x x y1 y2 H0); intro H1.
+elim H1; intro H2.
+
+autobatch.
+
+elim H2; intro H3.
+
+elim (ap_irreflexive _ _ H3).
+
+autobatch.
+Qed.
+
+Lemma Crel_strextarg_imp_strext :
+ Crel_strext_rht -> Crel_strext_lft -> Crel_strext.
+unfold Crel_strext, Crel_strext_lft, Crel_strext_rht in |- *;
+ intros H H0 x1 x2 y1 y2 H1.
+elim (H x1 y1 y2 H1); autobatch.
+intro H2.
+elim (H0 x1 x2 y2 H2); autobatch.
+Qed.
+*)
+
+
+
+
+(* ---- e questo ??????? -----*)
+
+(*Definition of a [CProp] setoid relation
+The type of relations over a setoid. *)
+(*
+Record CCSetoid_relation : Type :=
+ {Ccsr_rel :> S -> S -> CProp;
+ Ccsr_strext : Crel_strext Ccsr_rel}.
+
+Lemma Ccsr_wdr : forall R : CCSetoid_relation, Crel_wdr R.
+intro R.
+red in |- *; intros x y z H H0.
+elim (Ccsr_strext R x x y z H).
+
+autobatch.
+
+intro H1; elimtype False.
+elim H1; intro H2.
+
+exact (ap_irreflexive_unfolded _ _ H2).
+
+generalize H2.
+exact (eq_imp_not_ap _ _ _ H0).
+Qed.
+
+Lemma Ccsr_wdl : forall R : CCSetoid_relation, Crel_wdl R.
+intro R.
+red in |- *; intros x y z H H0.
+elim (Ccsr_strext R x z y y H).
+
+autobatch.
+
+intro H1; elimtype False.
+elim H1; intro H2.
+
+generalize H2.
+exact (eq_imp_not_ap _ _ _ H0).
+
+exact (ap_irreflexive_unfolded _ _ H2).
+Qed.
+
+Lemma ap_wdr : Crel_wdr (cs_ap (c:=S)).
+red in |- *; intros x y z H H0.
+generalize (eq_imp_not_ap _ _ _ H0); intro H1.
+elim (ap_cotransitive_unfolded _ _ _ H z); intro H2.
+
+assumption.
+
+elim H1.
+apply ap_symmetric_unfolded.
+assumption.
+Qed.
+
+Lemma ap_wdl : Crel_wdl (cs_ap (c:=S)).
+red in |- *; intros x y z H H0.
+generalize (ap_wdr y x z); intro H1.
+apply ap_symmetric_unfolded.
+apply H1.
+
+apply ap_symmetric_unfolded.
+assumption.
+
+assumption.
+Qed.
+
+Lemma ap_wdr_unfolded : forall x y z : S, x [#] y -> y [=] z -> x [#] z.
+Proof ap_wdr.
+
+Lemma ap_wdl_unfolded : forall x y z : S, x [#] y -> x [=] z -> z [#] y.
+Proof ap_wdl.
+
+Lemma ap_strext : Crel_strext (cs_ap (c:=S)).
+red in |- *; intros x1 x2 y1 y2 H.
+case (ap_cotransitive_unfolded _ _ _ H x2); intro H0.
+
+autobatch.
+
+case (ap_cotransitive_unfolded _ _ _ H0 y2); intro H1.
+
+autobatch.
+
+right; right.
+apply ap_symmetric_unfolded.
+assumption.
+Qed.
+
+Definition predS_well_def (P : S -> CProp) : CProp := forall x y : S,
+ P x -> x [=] y -> P y.
+
+End CSetoid_relations_and_predicates.
+
+Declare Left Step ap_wdl_unfolded.
+Declare Right Step ap_wdr_unfolded.
+*)
+
+
+
+
+
+
+
+
+
+(*------------------------------------------------------------------------*)
+(* ------------------------- Functions between setoids ------------------ *)
+(*------------------------------------------------------------------------*)
+
+(* Such functions must preserve the setoid equality
+and be strongly extensional w.r.t. the apartness, i.e.
+if f(x,y) # f(x1,y1), then x # x1 or y # y1.
+For every arity this has to be defined separately. *)
+
+(* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2) *)
+
+(* First we consider unary functions. *)
+
+(*
+In the following two definitions,
+f is a function from (the carrier of) S1 to (the carrier of) S2 *)
+
+(* Nota: senza le parentesi di (S1 \to S2) non funziona, perche'? *)
+definition fun_wd : \forall S1,S2 : CSetoid. (S1 \to S2) \to Prop \def
+ \lambda S1,S2 : CSetoid.\lambda f : S1 \to S2. \forall x,y : S1.
+ x = y \to f x = f y.
+
+definition fun_strext : \forall S1,S2 : CSetoid. (S1 \to S2) \to Prop \def
+ \lambda S1,S2 : CSetoid.\lambda f : S1 \to S2. \forall x,y : S1.
+ (f x \neq f y) \to (x \neq y).
+
+lemma fun_strext_imp_wd : \forall S1,S2 : CSetoid. \forall f : S1 \to S2.
+ fun_strext S1 S2 f \to fun_wd S1 S2 f.
+unfold fun_strext.
+unfold fun_wd.
+intros.
+apply not_ap_imp_eq.
+unfold.intro.
+apply (eq_imp_not_ap ? ? ? H1).
+apply H.assumption.
+qed.
+
+(* funzioni tra setoidi *)
+record CSetoid_fun (S1,S2 : CSetoid) : Type \def
+ {csf_fun : S1 \to S2;
+ csf_strext : (fun_strext S1 S2 csf_fun)}.
+
+lemma csf_wd : \forall S1,S2 : CSetoid. \forall f : CSetoid_fun S1 S2. fun_wd S1 S2 (csf_fun S1 S2 f).
+intros.
+apply fun_strext_imp_wd.
+apply csf_strext.
+qed.
+
+definition Const_CSetoid_fun : \forall S1,S2: CSetoid. S2 \to CSetoid_fun S1 S2.
+intros. apply (mk_CSetoid_fun S1 S2 (\lambda x:S1.c)).
+unfold.intros.
+elim (ap_irreflexive ? ? H).
+qed.
+
+
+(* ---- Binary functions ------*)
+(* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2 \to S3) *)
+
+definition bin_fun_wd : \forall S1,S2,S3 : CSetoid. (S1 \to S2 \to S3) \to Prop \def
+ \lambda S1,S2,S3 : CSetoid. \lambda f : S1 \to S2 \to S3. \forall x1,x2: S1. \forall y1,y2: S2.
+ x1 = x2 \to y1 = y2 \to f x1 y1 = f x2 y2.
+
+(*
+Definition bin_fun_strext : CProp := forall x1 x2 y1 y2,
+ f x1 y1 [#] f x2 y2 -> x1 [#] x2 or y1 [#] y2.
+*)
+
+definition bin_fun_strext: \forall S1,S2,S3 : CSetoid. (S1 \to S2 \to S3) \to Prop \def
+ \lambda S1,S2,S3 : CSetoid. \lambda f : S1 \to S2 \to S3. \forall x1,x2: S1. \forall y1,y2: S2.
+ f x1 y1 \neq f x2 y2 \to x1 \neq x2 \lor y1 \neq y2.
+
+lemma bin_fun_strext_imp_wd : \forall S1,S2,S3: CSetoid.\forall f:S1 \to S2 \to S3.
+bin_fun_strext ? ? ? f \to bin_fun_wd ? ? ? f.
+intros.unfold in H.
+unfold.intros.
+apply not_ap_imp_eq.unfold.intro.
+elim (H x1 x2 y1 y2 H3).
+apply (eq_imp_not_ap ? ? ? H1 H4).
+apply (eq_imp_not_ap ? ? ? H2 H4).
+qed.
+
+
+
+record CSetoid_bin_fun (S1,S2,S3: CSetoid) : Type \def
+ {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.
+ bin_fun_wd S1 S2 S3 (csbf_fun S1 S2 S3 f).
+intros.
+apply bin_fun_strext_imp_wd.
+apply csbf_strext.
+qed.
+
+lemma csf_wd_unfolded : \forall S1,S2: CSetoid. \forall f : CSetoid_fun S1 S2. \forall x,x' : S1.
+ x = x' \to (csf_fun S1 S2 f) x = (csf_fun S1 S2 f) x'.
+intros.
+apply (csf_wd S1 S2 f x x').
+assumption.
+qed.
+
+lemma csf_strext_unfolded : \forall S1,S2: CSetoid. \forall f : CSetoid_fun S1 S2. \forall x,y : S1.
+(csf_fun S1 S2 f) x \neq (csf_fun S1 S2 f) y \to x \neq y.
+intros.
+apply (csf_strext S1 S2 f x y).
+assumption.
+qed.
+
+lemma csbf_wd_unfolded : \forall S1,S2,S3 : CSetoid. \forall f : CSetoid_bin_fun S1 S2 S3. \forall x,x':S1.
+\forall y,y' : S2. x = x' \to y = y' \to (csbf_fun S1 S2 S3 f) x y = (csbf_fun S1 S2 S3 f) x' y'.
+intros.
+apply (csbf_wd S1 S2 S3 f x x' y y'); assumption.
+qed.
+
+(* Hint Resolve csf_wd_unfolded csbf_wd_unfolded: algebra_c.*)
+
+(* The unary and binary (inner) operations on a csetoid
+An operation is a function with domain(s) and co-domain equal. *)
+
+(* Properties of binary operations *)
+
+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 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.
+
+definition un_op_wd : \forall S:CSetoid. (S \to S) \to Prop \def
+\lambda S: CSetoid. \lambda f: (S \to S). fun_wd S S f.
+
+
+definition un_op_strext: \forall S:CSetoid. (S \to S) \to Prop \def
+\lambda S:CSetoid. \lambda f: (S \to S). fun_strext S S f.
+
+
+definition CSetoid_un_op : CSetoid \to Type \def
+\lambda S:CSetoid. CSetoid_fun S S.
+
+definition mk_CSetoid_un_op : \forall S:CSetoid. \forall f: S \to S. fun_strext S S f \to CSetoid_fun S S
+ \def
+\lambda S:CSetoid. \lambda f: S \to S. mk_CSetoid_fun S S f.
+
+lemma id_strext : \forall S:CSetoid. un_op_strext S (\lambda x:S. x).
+unfold un_op_strext.
+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.
+exact H.
+qed.
+
+definition id_un_op : \forall S:CSetoid. CSetoid_un_op S
+ \def \lambda S: CSetoid. mk_CSetoid_un_op S (\lambda x : cs_crr S.x) (id_strext S).
+
+definition un_op_fun: \forall S:CSetoid. CSetoid_un_op S \to CSetoid_fun S S
+\def \lambda S.\lambda f.f.
+
+coercion cic:/matita/algebra/CoRN/Setoids/un_op_fun.con.
+
+definition cs_un_op_strext : \forall S:CSetoid. \forall f: CSetoid_fun S S. fun_strext S S (csf_fun S S f) \def
+\lambda S:CSetoid. \lambda f : CSetoid_fun S S. csf_strext S S f.
+
+lemma un_op_wd_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op S.
+\forall x, y : S.
+x = y \to (csf_fun S S op) x = (csf_fun S S op) y.
+intros.
+apply (csf_wd S S ?).assumption.
+qed.
+
+lemma un_op_strext_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op S.
+\forall x, y : S.
+ (csf_fun S S op) x \neq (csf_fun S S op) y \to x \neq y.
+exact cs_un_op_strext.
+qed.
+
+
+(* Well-defined binary operations on a setoid. *)
+
+definition bin_op_wd : \forall S:CSetoid. (S \to S \to S) \to Prop \def
+\lambda S:CSetoid. bin_fun_wd S S S.
+
+definition bin_op_strext : \forall S:CSetoid. (S \to S \to S) \to Prop \def
+\lambda S:CSetoid. bin_fun_strext S S S.
+
+definition CSetoid_bin_op : CSetoid \to Type \def
+\lambda S:CSetoid. CSetoid_bin_fun S S S.
+
+
+definition mk_CSetoid_bin_op : \forall S:CSetoid. \forall f: S \to S \to S.
+bin_fun_strext S S S f \to CSetoid_bin_fun S S S \def
+ \lambda S:CSetoid. \lambda f: S \to S \to S.
+ mk_CSetoid_bin_fun S S S f.
+
+(* da controllare che sia ben tipata
+definition cs_bin_op_wd : \forall S:CSetoid. ? \def
+\lambda S:CSetoid. csbf_wd S S S.
+*)
+definition cs_bin_op_wd : \forall S:CSetoid. \forall f: CSetoid_bin_fun S S S. bin_fun_wd S S S (csbf_fun S S S f) \def
+\lambda S:CSetoid. csbf_wd S S S.
+
+definition cs_bin_op_strext : \forall S:CSetoid. \forall f: CSetoid_bin_fun S S S. bin_fun_strext S S S (csbf_fun S S S f) \def
+\lambda S:CSetoid. csbf_strext S S S.
+
+
+
+(* Identity Coercion bin_op_bin_fun : CSetoid_bin_op >-> CSetoid_bin_fun. *)
+
+definition bin_op_bin_fun: \forall S:CSetoid. CSetoid_bin_op S \to CSetoid_bin_fun S S S
+\def \lambda S.\lambda f.f.
+
+coercion cic:/matita/algebra/CoRN/Setoids/bin_op_bin_fun.con.
+
+
+
+
+lemma bin_op_wd_unfolded :\forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall x1, x2, y1, y2 : S.
+ x1 = x2 \to y1 = y2 \to (csbf_fun S S S op) x1 y1 = (csbf_fun S S S op) x2 y2.
+exact cs_bin_op_wd.
+qed.
+
+lemma bin_op_strext_unfolded : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall x1, x2, y1, y2 : S.
+ (csbf_fun S S S op) x1 y1 \neq (csbf_fun S S S op) x2 y2 \to x1 \neq x2 \lor y1 \neq y2.
+exact cs_bin_op_strext.
+qed.
+
+lemma bin_op_is_wd_un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
+ un_op_wd S (\lambda x : cs_crr S. ((csbf_fun S S S op) x c)).
+intros. unfold. unfold.
+intros. apply bin_op_wd_unfolded [ assumption | apply eq_reflexive_unfolded ]
+qed.
+
+lemma bin_op_is_wd_un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
+ un_op_wd S (\lambda x : cs_crr S. ((csbf_fun S S S op) c x)).
+intros. unfold. unfold.
+intros. apply bin_op_wd_unfolded [ apply eq_reflexive_unfolded | assumption ]
+qed.
+
+
+lemma bin_op_is_strext_un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
+ un_op_strext S (\lambda x : cs_crr S. ((csbf_fun S S S op) x c)).
+intros. unfold un_op_strext. unfold fun_strext.
+intros.
+cut (x \neq y \lor c \neq c)
+[ elim Hcut
+ [ assumption
+ | generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
+ ]
+| apply (bin_op_strext_unfolded S op x y c c). assumption.
+]
+qed.
+
+lemma bin_op_is_strext_un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
+ un_op_strext S (\lambda x : cs_crr S. ((csbf_fun S S S op) c x)).
+intros. unfold un_op_strext. unfold fun_strext.
+intros.
+cut (c \neq c \lor x \neq y)
+[ elim Hcut
+ [ generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
+ | assumption
+ ]
+| apply (bin_op_strext_unfolded S op c c x y). assumption.
+]
+qed.
+
+definition bin_op2un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S.
+\forall c : cs_crr S. CSetoid_un_op S \def
+ \lambda S:CSetoid. \lambda op: CSetoid_bin_op S. \lambda c : cs_crr S.
+ mk_CSetoid_un_op S (\lambda x:cs_crr S. ((csbf_fun S S S op) c x))
+ (bin_op_is_strext_un_op_rht S op c).
+
+definition bin_op2un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S.
+\forall c : cs_crr S. CSetoid_un_op S \def
+ \lambda S:CSetoid. \lambda op: CSetoid_bin_op S. \lambda c : cs_crr S.
+ mk_CSetoid_un_op S (\lambda x:cs_crr S. ((csbf_fun S S S op) x c))
+ (bin_op_is_strext_un_op_lft S op c).
+
+(*
+Definition bin_op2un_op_rht (op : CSetoid_bin_op) (c : S) : CSetoid_un_op :=
+ Build_CSetoid_un_op (fun x : S => op c x) (bin_op_is_strext_un_op_rht op c).
+
+
+Definition bin_op2un_op_lft (op : CSetoid_bin_op) (c : S) : CSetoid_un_op :=
+ Build_CSetoid_un_op (fun x : S => op x c) (bin_op_is_strext_un_op_lft op c).
+*)
+
+
+(*
+Implicit Arguments commutes [S].
+Implicit Arguments associative [S].
+Hint Resolve bin_op_wd_unfolded un_op_wd_unfolded: algebra_c.
+*)
+
+(*The binary outer operations on a csetoid*)
+
+
+(*
+Well-defined outer operations on a setoid.
+*)
+definition outer_op_well_def : \forall S1,S2:CSetoid. (S1 \to S2 \to S2) \to Prop \def
+\lambda S1,S2:CSetoid. bin_fun_wd S1 S2 S2.
+
+definition outer_op_strext : \forall S1,S2:CSetoid. (S1 \to S2 \to S2) \to Prop \def
+\lambda S1,S2:CSetoid. bin_fun_strext S1 S2 S2.
+
+definition CSetoid_outer_op : \forall S1,S2:CSetoid.Type \def
+\lambda S1,S2:CSetoid.
+ CSetoid_bin_fun S1 S2 S2.
+
+definition mk_CSetoid_outer_op : \forall S1,S2:CSetoid.
+\forall f : S1 \to S2 \to S2.
+bin_fun_strext S1 S2 S2 f \to CSetoid_bin_fun S1 S2 S2 \def
+\lambda S1,S2:CSetoid.
+mk_CSetoid_bin_fun S1 S2 S2.
+
+definition csoo_wd : \forall S1,S2:CSetoid. \forall f : CSetoid_bin_fun S1 S2 S2.
+bin_fun_wd S1 S2 S2 (csbf_fun S1 S2 S2 f) \def
+\lambda S1,S2:CSetoid.
+csbf_wd S1 S2 S2.
+
+definition csoo_strext : \forall S1,S2:CSetoid.
+\forall f : CSetoid_bin_fun S1 S2 S2.
+bin_fun_strext S1 S2 S2 (csbf_fun S1 S2 S2 f) \def
+\lambda S1,S2:CSetoid.
+csbf_strext S1 S2 S2.
+
+
+definition outer_op_bin_fun: \forall S:CSetoid.
+CSetoid_outer_op S S \to CSetoid_bin_fun S S S
+\def \lambda S.\lambda f.f.
+
+coercion cic:/matita/algebra/CoRN/Setoids/outer_op_bin_fun.con.
+(* begin hide
+Identity Coercion outer_op_bin_fun : CSetoid_outer_op >-> CSetoid_bin_fun.
+end hide *)
+
+lemma csoo_wd_unfolded :\forall S:CSetoid. \forall op : CSetoid_outer_op S S.
+\forall x1, x2, y1, y2 : S.
+ x1 = x2 -> y1 = y2 -> (csbf_fun S S S op) x1 y1 = (csbf_fun S S S op) x2 y2.
+intros.
+apply csoo_wd[assumption|assumption]
+qed.
+
+(*
+Hint Resolve csoo_wd_unfolded: algebra_c.
+*)
+
+
+
+(*---------------------------------------------------------------*)
+(*--------------------------- Subsetoids ------------------------*)
+(*---------------------------------------------------------------*)
+
+(* Let S be a setoid, and P a predicate on the carrier of S *)
+(* Variable P : S -> CProp *)
+
+record subcsetoid_crr (S: CSetoid) (P: S \to Prop) : Type \def
+ {scs_elem :> S;
+ scs_prf : P scs_elem}.
+
+definition restrict_relation : \forall S:CSetoid. \forall R : S \to S \to Prop.
+ \forall P: S \to Prop. relation (subcsetoid_crr S P) \def
+ \lambda S:CSetoid. \lambda R : S \to S \to Prop.
+ \lambda P: S \to Prop. \lambda a,b: subcsetoid_crr S P.
+ match a with
+ [ (mk_subcsetoid_crr x H) \Rightarrow
+ match b with
+ [ (mk_subcsetoid_crr y H) \Rightarrow R x y ]
+ ].
+(* CPROP
+definition Crestrict_relation (R : Crelation S) : Crelation subcsetoid_crr :=
+ fun a b : subcsetoid_crr =>
+ match a, b with
+ | Build_subcsetoid_crr x _, Build_subcsetoid_crr y _ => R x y
+ end.
+*)
+
+definition subcsetoid_eq : \forall S:CSetoid. \forall P: S \to Prop.
+ relation (subcsetoid_crr S P)\def
+ \lambda S:CSetoid.
+ restrict_relation S (cs_eq S).
+
+definition subcsetoid_ap : \forall S:CSetoid. \forall P: S \to Prop.
+ relation (subcsetoid_crr S P)\def
+ \lambda S:CSetoid.
+ restrict_relation S (cs_ap S).
+
+(* N.B. da spostare in relations.ma... *)
+definition equiv : \forall A: Type. \forall R: relation A. Prop \def
+ \lambda A: Type. \lambda R: relation A.
+ (reflexive A R) \land (transitive A R) \land (symmetric A R).
+
+remark subcsetoid_equiv : \forall S:CSetoid. \forall P: S \to Prop.
+equiv ? (subcsetoid_eq S P).
+intros. unfold equiv. split
+[split
+ [unfold. intro. elim x. simplify. apply (eq_reflexive S)
+ |unfold. intros 3. elim y 2.
+ elim x 2. elim z 2. simplify.
+ exact (eq_transitive ? c1 c c2)
+ ]
+| unfold. intros 2. elim x 2. elim y 2. simplify. exact (eq_symmetric ? c c1).
+]
+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 | 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)
+(* cotransitive *)
+|unfold.intros 2. elim x.generalize in match H1. elim y. elim z.simplify. simplify in H3.
+apply (ap_cotransitive ? ? ? H3)
+(* tight *)
+|unfold.intros.elim x. elim y.simplify.
+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).
+
+(* Subsetoid unary operations
+%\begin{convention}%
+Let [f] be a unary setoid operation on [S].
+%\end{convention}%
+*)
+
+(* Section SubCSetoid_unary_operations.
+Variable f : CSetoid_un_op S.
+*)
+
+definition un_op_pres_pred : \forall S:CSetoid. \forall P: S \to Prop.
+ CSetoid_un_op S \to Prop \def
+ \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
+ \forall x : cs_crr S. P x \to P ((csf_fun S S f) x).
+
+definition restr_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.
+ subcsetoid_crr S P \to subcsetoid_crr 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.\lambda a: subcsetoid_crr S P.
+ match a with
+ [ (mk_subcsetoid_crr x p) \Rightarrow
+ (mk_subcsetoid_crr ? ? ((csf_fun S S f) x) (pr x p))].
+
+(* TODO *)
+lemma restr_un_op_wd : \forall S:CSetoid. \forall P: S \to Prop.
+\forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
+un_op_wd (mk_SubCSetoid S P) (restr_un_op S P f pr).
+intros.
+unfold.unfold.intros 2.elim x 2.elim y 2.
+simplify.
+intro.
+normalize in H2.
+apply (un_op_wd_unfolded ? f ? ? H2).
+qed.
+
+lemma restr_un_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
+\forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
+un_op_strext (mk_SubCSetoid S P) (restr_un_op S P f pr).
+intros.unfold.unfold. intros 2.elim y 2. elim x 2.
+intros.normalize in H2.
+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).
+ 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].
+*)
+
+(* Section SubCSetoid_binary_operations.
+Variable f : CSetoid_bin_op S.
+*)
+
+definition bin_op_pres_pred : \forall S:CSetoid. \forall P: S \to Prop.
+(CSetoid_bin_op S) \to Prop \def
+ \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_bin_op S.
+ \forall x,y : S. P x \to P y \to P ( (csbf_fun S S S f) x y).
+
+(*
+Assume [bin_op_pres_pred].
+*)
+
+(* Variable pr : bin_op_pres_pred. *)
+
+definition restr_bin_op : \forall S:CSetoid. \forall P:S \to Prop.
+ \forall f: CSetoid_bin_op S.\forall op : (bin_op_pres_pred S P f).
+ \forall a, b : subcsetoid_crr S P. subcsetoid_crr 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).
+ \lambda a, b : subcsetoid_crr S P.
+ match a with
+ [ (mk_subcsetoid_crr x p) \Rightarrow
+ match b with
+ [ (mk_subcsetoid_crr y q) \Rightarrow
+ (mk_subcsetoid_crr ? ? ((csbf_fun S S S f) x y) (pr x y p q))]
+ ].
+
+
+(* TODO *)
+lemma restr_bin_op_well_def : \forall S:CSetoid. \forall P: S \to Prop.
+\forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
+bin_op_wd (mk_SubCSetoid S P) (restr_bin_op S P f pr).
+intros.
+unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
+simplify.
+intros.
+normalize in H4.
+normalize in H5.
+apply (cs_bin_op_wd ? f ? ? ? ? H4 H5).
+qed.
+
+lemma restr_bin_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
+\forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
+bin_op_strext (mk_SubCSetoid S P) (restr_bin_op S P f pr).
+intros.unfold.unfold. intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
+simplify.intros.
+normalize 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.
+ 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.
+intros 3.
+elim z 2.elim y 2. elim x 2.
+whd.
+apply H.
+qed.
+
+definition caseZ_diff: \forall A:Type.Z \to (nat \to nat \to A) \to A \def
+\lambda A:Type.\lambda z:Z.\lambda f:nat \to nat \to A.
+ match z with
+ [OZ \Rightarrow f O O
+ |(pos n) \Rightarrow f (S n) O
+ |(neg n) \Rightarrow f O (S n)].
+
+(* Zminus.ma *)
+theorem Zminus_S_S : \forall n,m:nat.
+Z_of_nat (S n) - S m = Z_of_nat n - m.
+intros.
+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).
+intros.
+(* perche' apply nat_elim2 non funziona?? *)
+apply (nat_elim2 (\lambda m,n.caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = f m n)).
+intro.simplify.
+apply (nat_case n1).simplify.
+apply eq_reflexive.
+intro.simplify.apply eq_reflexive.
+intro.simplify.apply eq_reflexive.
+intros 2.
+rewrite > (Zminus_S_S n1 m1).
+intros.
+cut (f n1 m1 = f (S n1) (S m1)).
+apply eq_symmetric_unfolded.
+apply eq_transitive.
+apply f. apply n1. apply m1.
+apply eq_symmetric_unfolded.assumption.
+apply eq_symmetric_unfolded.assumption.
+apply H.
+autobatch.
+qed.
+
+(*
+Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
+*)
+
+
+definition nat_less_n_fun : \forall S:CSetoid. \forall n:nat. ? \def
+ \lambda S:CSetoid. \lambda n:nat. \lambda f: \forall i:nat. i < n \to S.
+ \forall i,j : nat. eq nat i j \to (\forall H : i < n.
+ \forall H' : j < n . (f i H) = (f j H')).
+
+definition nat_less_n_fun' : \forall S:CSetoid. \forall n:nat. ? \def
+ \lambda S:CSetoid. \lambda n:nat. \lambda f: \forall i: nat. i <= n \to S.
+ \forall i,j : nat. eq nat i j \to \forall H : i <= n.
+ \forall H' : j <= n. f i H = f j H'.
--- /dev/null
+algebra/CoRN/SemiGroups.ma algebra/CoRN/SetoidInc.ma
+algebra/CoRN/SetoidInc.ma algebra/CoRN/SetoidFun.ma
+algebra/CoRN/Setoids.ma Z/plus.ma datatypes/constructors.ma higher_order_defs/relations.ma logic/equality.ma nat/nat.ma
+algebra/CoRN/SetoidFun.ma algebra/CoRN/Setoids.ma higher_order_defs/relations.ma
+Z/plus.ma
+datatypes/constructors.ma
+higher_order_defs/relations.ma
+logic/equality.ma
+nat/nat.ma
--- /dev/null
+baseuri=cic:/matita
GOALS = all opt clean clean.opt
-DEVELS = RELATIONAL LOGIC LAMBDA-TYPES assembly dama POPLmark
+DEVELS = RELATIONAL LOGIC LAMBDA-TYPES assembly dama POPLmark CoRN
$(GOALS):
@$(foreach DEVEL, $(DEVELS), $(MAKE) -C $(DEVEL) $@;)
+++ /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).
-autobatch.
-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 autobatchmorphisms; 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 a|elim Hy.apply a|exact H1]|
-apply pfstrx[apply F'|elim Hx.apply b|elim Hy.apply b|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
- [pair (x1: (cs_crr (csg_crr M1))) (x2: (cs_crr (csg_crr M2))) \Rightarrow
- match y with
- [pair (y1: (cs_crr (csg_crr M1))) (y2: (cs_crr (csg_crr M2))) \Rightarrow
- pair (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. *)
+++ /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: CSetoidFun.v,v 1.12 2004/09/22 11:06:10 loeb Exp $ *)
-
-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.
- \exists a:A. (csf_fun A B f) a \neq (csf_fun A B g) a.
-(* Definition ap_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
- {a : A | f a[#]g a}. *)
-
-definition eq_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.
- \forall a:A. (csf_fun A B f) a = (csf_fun A B g) a.
-(* Definition eq_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
- forall a : A, f a[=]g a. *)
-
-lemma irrefl_apfun : \forall A,B : CSetoid.
- irreflexive (CSetoid_fun A B) (ap_fun A B).
-intros.
-unfold irreflexive. intro f.
-unfold ap_fun.
-unfold.
-intro.
-elim H.
-cut (csf_fun A B f a = csf_fun A B f a)
-[ 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 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).
-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.
-
-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).
-
-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 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.
-apply a.
-apply Hg2.
-exact H0.
-qed.
-
-
-(* Questa coercion composta non e' stata generata autobatchmaticamente *)
-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]; autobatch.
-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 a.
-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.
-autobatch |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.autobatch|simplify.intros.exact H1]|
-intros (a at).
-simplify.
-split[intro.autobatch|intros. exact H1]
-]
-|
-intros (a at IHx).
-elim y 0[simplify.
- split[intro.autobatch|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 ? a).assumption|apply (f1 x ? b). 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.
-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].
-*)
-
-(*
-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 (b a).
-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.
-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.
-
-Qed.
-*)
-
-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 ? a)[apply H2|apply b]
- ]
-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 autobatchmorphisms. *)
-
-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).
-apply ap_symmetric_unfolded. assumption.
-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.autobatch.
- ]
-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 c 0;
- elim c1 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.autobatch]
-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 _ _ _ _). *)
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/algebra/CoRN/SetoidInc".
-include "algebra/CoRN/SetoidFun.ma".
-
-(* $Id: CSetoidInc.v,v 1.3 2004/04/22 14:49:43 lcf Exp $ *)
-
-(* printing included %\ensuremath{\subseteq}% #⊆# *)
-
-(* Section inclusion. *)
-
-(* Inclusion
-
-Let [S] be a setoid, and [P], [Q], [R] be predicates on [S]. *)
-
-(* Variable S : CSetoid. *)
-
-definition included : \forall S : CSetoid. \forall P,Q : S \to Type. Type \def
- \lambda S : CSetoid. \lambda P,Q : S \to Type.
- \forall x : S. P x \to Q x.
-
-(* Section Basics. *)
-
-(* Variables P Q R : S -> CProp. *)
-lemma included_refl : \forall S : CSetoid. \forall P : S \to Type.
- included S P P.
-intros.
-unfold.
-intros.
-assumption.
-qed.
-
-lemma included_trans : \forall S : CSetoid. \forall P,Q,R : S \to Type.
- included S P Q \to included S Q R \to included S P R.
-intros.
-unfold.
-intros.
-apply i1.
-apply i.
-assumption.
-qed.
-
-lemma included_conj : \forall S : CSetoid. \forall P,Q,R : S \to Type.
- included S P Q \to included S P R \to included S P (conjP S Q R).
-intros 4.
-unfold included.
-intros;
-unfold.
-split [apply f.assumption|apply f1.assumption]
-qed.
-
-lemma included_conj' : \forall S : CSetoid. \forall P,Q,R : S \to Type.
- included S (conjP S P Q) P.
- intros.
-exact (prj1 S P Q).
-qed.
-
-lemma included_conj'' : \forall S : CSetoid. \forall P,Q,R : S \to Type.
- included S (conjP S P Q) Q.
- intros.
-exact (prj2 S P Q).
-qed.
-
-lemma included_conj_lft : \forall S : CSetoid. \forall P,Q,R : S \to Type.
- included S R (conjP S P Q) -> included S R P.
-intros 4.
-unfold included.
-unfold conjP.intros (f1 x H2).
-elim (f1 x ); assumption.
-qed.
-
-lemma included_conj_rht : \forall S : CSetoid. \forall P,Q,R : S \to Type.
- included S R (conjP S P Q) \to included S R Q.
- intros 4.
- unfold included.
- unfold conjP.
-intros (H1 x H2).
-elim (H1 x); assumption.
-qed.
-lemma included_extend : \forall S : CSetoid. \forall P,Q,R : S \to Type.
- \forall H : \forall x. P x \to Type.
- included S R (extend S P H) \to included S R P.
-intros 4.
-intros (H0 H1).
-unfold.
-unfold extend in H1.
-intros.
-elim (H1 x);assumption.
-qed.
-
-
-(* End Basics. *)
-
-(*
-%\begin{convention}% Let [I,R:S->CProp] and [F G:(PartFunct S)], and denote
-by [P] and [Q], respectively, the domains of [F] and [G].
-%\end{convention}%
-*)
-
-(* Variables F G : (PartFunct S). *)
-
-(* begin hide *)
-(* Let P := Dom F. *)
-(* Let Q := Dom G. *)
-(* end hide *)
-
-(* Variable R : S -> CProp. *)
-lemma included_FComp : \forall S : CSetoid. \forall F,G: PartFunct S.
-\forall R : S \to Type.
- included S R (UP ? F) \to (\forall x: S. \forall Hx. (R x) \to UQ ? G (pfpfun ? F x Hx)) \to
- included S R (pfdom ? (Fcomp ? F G)).
-intros (S F G R HP HQ).
-unfold Fcomp.
-simplify.
-unfold included. intros (x Hx).
-apply (existT ? ? (HP x Hx)).
-apply HQ.
-assumption.
-qed.
-
-lemma included_FComp': \forall S : CSetoid. \forall F,G: PartFunct S.
-\forall R : S \to Type.
-included S R (pfdom ? (Fcomp ? F G)) \to included S R (UP ? F).
-intros (S F G R H).
-unfold Fcomp in H.
-simplify in H.
-unfold. intros (x Hx).
-elim (H x Hx);
-assumption.
-qed.
-
-(* End inclusion. *)
-
-(* Implicit Arguments included [S].
-
-Hint Resolve included_refl included_FComp : included.
-
-Hint Immediate included_trans included_FComp' : included. *)
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/algebra/CoRN/Setoid".
-
-
-include "higher_order_defs/relations.ma".
-include "Z/plus.ma".
-
-include "datatypes/constructors.ma".
-include "nat/nat.ma".
-include "logic/equality.ma".
-(*include "Z/Zminus.ma".*)
-
-(* Setoids
-Definition of a constructive setoid with apartness,
-i.e. a set with an equivalence relation and an apartness relation compatible with it.
-*)
-
-(* Definition of Setoid
-Apartness, being the main relation, needs to be [CProp]-valued. Equality,
-as it is characterized by a negative statement, lives in [Prop].
-
-N.B. for the moment we use Prop for both (Matita group)
-*)
-
-record is_CSetoid (A : Type) (eq : relation A) (ap : relation A) : Prop \def
- {ax_ap_irreflexive : irreflexive A ap;
- ax_ap_symmetric : symmetric A ap;
- ax_ap_cotransitive : cotransitive A ap;
- ax_ap_tight : tight_apart A eq ap}.
-
-record CSetoid : Type \def
- {cs_crr :> Type;
- cs_eq : relation cs_crr;
- cs_ap : relation cs_crr;
- cs_proof : is_CSetoid cs_crr cs_eq cs_ap}.
-
-interpretation "setoid equality"
- 'eq x y = (cic:/matita/algebra/CoRN/Setoids/cs_eq.con _ x y).
-
-interpretation "setoid apart"
- 'neq x y = (cic:/matita/algebra/CoRN/Setoids/cs_ap.con _ x y).
-
-(* visto che sia "ap" che "eq" vanno in Prop e data la "tight-apartness",
-"cs_neq" e "ap" non sono la stessa cosa? *)
-definition cs_neq : \forall S : CSetoid. relation S \def
- \lambda S : CSetoid. \lambda x,y : S. \not x = y.
-
-lemma CSetoid_is_CSetoid :
- \forall S : CSetoid. is_CSetoid S (cs_eq S) (cs_ap S).
-intro. apply (cs_proof S).
-qed.
-
-lemma ap_irreflexive: \forall S : CSetoid. irreflexive S (cs_ap S).
-intro. elim (CSetoid_is_CSetoid S). assumption.
-qed.
-
-lemma ap_symmetric : \forall S : CSetoid. symmetric S(cs_ap S).
-intro. elim (CSetoid_is_CSetoid S). assumption.
-qed.
-
-lemma ap_cotransitive : \forall S : CSetoid. cotransitive S (cs_ap S).
-intro. elim (CSetoid_is_CSetoid S). assumption.
-qed.
-
-lemma ap_tight : \forall S : CSetoid. tight_apart S (cs_eq S) (cs_ap S).
-intro. elim (CSetoid_is_CSetoid S). assumption.
-qed.
-
-definition ex_unq : \forall S : CSetoid. (S \to Prop) \to Prop \def
- \lambda S : CSetoid. \lambda P : S \to Prop.
- ex2 S (\lambda x. \forall y : S. P y \to x = y) P.
-
-
-lemma eq_reflexive : \forall S : CSetoid. reflexive S (cs_eq S).
-intro. unfold. intro.
-generalize in match (ap_tight S x x).
-intro.
-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.
-generalize in match (ap_tight S y x). intro.
-generalize in match (ap_symmetric S y x). intro.
-elim H1. clear H1.
-elim H2. clear H2.
-apply H1. unfold. intro. autobatch.
-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.
-generalize in match (ap_tight S y z). intro.
-generalize in match (ap_tight S x z). intro.
-elim H3.
-apply H4. unfold. intro.
-generalize in match (ap_cotransitive ? ? ? H6 y). intro H7.
-elim H1 (H1' H1''). clear H1.
-elim H2 (H2' H2''). clear H2.
-elim H3 (H3' H3''). clear H3.
-elim H7 (H1). clear H7.
-generalize in match H1. apply H1''. assumption. (*non ho capito il secondo passo*)
-generalize in match H1. apply H2''. assumption.
-qed.
-
-lemma eq_reflexive_unfolded : \forall S:CSetoid. \forall x:S. x = x.
-apply eq_reflexive.
-qed.
-
-lemma eq_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S. x = y \to y = x.
-apply eq_symmetric.
-qed.
-
-lemma eq_transitive_unfolded : \forall S:CSetoid. \forall x,y,z:S. x = y \to y = z \to x = z.
-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' autobatch non arriva in fondo ??? *)
-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.
-
-lemma ap_cotransitive_unfolded : \forall S:CSetoid. \forall a,b:S. a \neq b \to
- \forall c:S. a \neq c \or c \neq b.
-apply ap_cotransitive.
-qed.
-
-lemma ap_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S.
- x \neq y \to y \neq x.
-apply ap_symmetric.
-qed.
-
-lemma eq_imp_not_ap : \forall S:CSetoid. \forall x,y:S.
- x = y \to \not (x \neq y).
-intros.
-elim (ap_tight S x y).
-apply H2. assumption.
-qed.
-
-lemma not_ap_imp_eq : \forall S:CSetoid. \forall x,y:S.
- \not (x \neq y) \to x = y.
-intros.
-elim (ap_tight S x y).
-apply H1. assumption.
-qed.
-
-lemma neq_imp_notnot_ap : \forall S:CSetoid. \forall x,y:S.
- (cs_neq S x y) \to \not \not (x \neq y).
-intros. unfold. intro.
-apply H.
-apply not_ap_imp_eq.
-assumption.
-qed.
-
-lemma notnot_ap_imp_neq: \forall S:CSetoid. \forall x,y:S.
- (\not \not (x \neq y)) \to (cs_neq S x y).
-intros. unfold. unfold. intro.
-apply H.
-apply eq_imp_not_ap.
-assumption.
-qed.
-
-lemma ap_imp_neq : \forall S:CSetoid. \forall x,y:S.
- x \neq y \to (cs_neq S x y).
-intros. unfold. unfold. intro.
-apply (eq_imp_not_ap S ? ? H1).
-assumption.
-qed.
-
-lemma not_neq_imp_eq : \forall S:CSetoid. \forall x,y:S.
- \not (cs_neq S x y) \to x = y.
-intros.
-apply not_ap_imp_eq.
-unfold. intro.
-apply H.
-apply ap_imp_neq.
-assumption.
-qed.
-
-lemma eq_imp_not_neq : \forall S:CSetoid. \forall x,y:S.
- x = y \to \not (cs_neq S x y).
-intros. unfold. intro.
-apply H1.
-assumption.
-qed.
-
-
-
-(* -----------------The product of setoids----------------------- *)
-
-definition prod_ap: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def
-\lambda A,B : CSetoid.\lambda c,d: Prod A B.
- ((cs_ap A (fst A B c) (fst A B d)) \or
- (cs_ap B (snd A B c) (snd A B d))).
-
-definition prod_eq: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def
-\lambda A,B : CSetoid.\lambda c,d: Prod A B.
- ((cs_eq A (fst A B c) (fst A B d)) \and
- (cs_eq B (snd A B c) (snd A B d))).
-
-
-lemma prodcsetoid_is_CSetoid: \forall A,B: CSetoid.
- is_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B).
-intros.
-apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
- [unfold.
- intros.
- elim x.
- unfold.
- unfold prod_ap. simplify.
- intros.
- elim H
- [apply (ap_irreflexive A a H1)
- |apply (ap_irreflexive B b H1)
- ]
- |unfold.
- intros 2.
- elim x 2.
- elim y 2.
- unfold prod_ap. simplify.
- intro.
- elim H
- [left. apply ap_symmetric. assumption.
- |right. apply ap_symmetric. assumption
- ]
- |unfold.
- intros 2.
- elim x 2.
- elim y 4.
- elim z.
- unfold prod_ap in H. simplify in H.
- unfold prod_ap. simplify.
- elim H
- [cut ((a \neq a2) \or (a2 \neq a1))
- [elim Hcut
- [left. left. assumption
- |right. left. assumption
- ]
- |apply (ap_cotransitive A). assumption
- ]
- |cut ((b \neq b2) \or (b2 \neq b1))
- [elim Hcut
- [left. right. assumption
- |right. right. assumption
- ]
- |apply (ap_cotransitive B). assumption.
- ]
- ]
-|unfold.
- intros 2.
- elim x 2.
- elim y 2.
- unfold prod_ap. simplify.
- split
- [intro.
- left
- [apply not_ap_imp_eq.
- unfold. intro. apply H.
- left. assumption
- |apply not_ap_imp_eq.
- unfold. intro. apply H.
- right. assumption
- ]
- |intro. unfold. intro.
- elim H.
- elim H1
- [apply (eq_imp_not_ap A a a1 H2). assumption
- |apply (eq_imp_not_ap B b b1 H3). assumption
- ]
- ]
-]
-qed.
-
-
-definition ProdCSetoid : \forall A,B: CSetoid. CSetoid \def
- \lambda A,B: CSetoid.
- mk_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).
-
-
-
-(* Relations and predicates
-Here we define the notions of well-definedness and strong extensionality
-on predicates and relations.
-*)
-
-
-
-(*-----------------------------------------------------------------------*)
-(*-------------------------- Predicates on Setoids ----------------------*)
-(*-----------------------------------------------------------------------*)
-
-(* throughout this section consider (S : CSetoid) and (P : S -> Prop) *)
-
-(* Definition pred_strong_ext : CProp := forall x y : S, P x -> P y or x [#] y. *)
-definition pred_strong_ext : \forall S: CSetoid. (S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda P: S \to Prop. \forall x,y: S.
- 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. \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
- {wdp_pred :> S \to Prop;
- wdp_well_def : pred_wd S wdp_pred}.
-
-record CSetoid_predicate (S: CSetoid) : Type \def
- {csp_pred :> S \to Prop;
- csp_strext : pred_strong_ext S csp_pred}.
-
-lemma csp_wd : \forall S: CSetoid. \forall P: CSetoid_predicate S.
- pred_wd S (csp_pred S P).
-intros.
-elim P.
-simplify.unfold pred_wd.
-intros.
-elim (H x y H1)
- [assumption|apply False_ind.apply (eq_imp_not_ap S x y H2 H3)]
-qed.
-
-
-(* Same result with CProp instead of Prop: but we just work with Prop (Matita group) *)
-(*
-Definition pred_strong_ext' : CProp := forall x y : S, P x -> P y or x [#] y.
-Definition pred_wd' : Prop := forall x y : S, P x -> x [=] y -> P y.
-
-Record CSetoid_predicate' : Type :=
- {csp'_pred :> S -> Prop;
- csp'_strext : pred_strong_ext' csp'_pred}.
-
-Lemma csp'_wd : forall P : CSetoid_predicate', pred_wd' P.
-intro P.
-intro x; intros y H H0.
-elim (csp'_strext P x y H).
-
-autobatch.
-
-intro H1.
-elimtype False.
-generalize H1.
-exact (eq_imp_not_ap _ _ _ H0).
-Qed.
-*)
-
-
-
-(*------------------------------------------------------------------------*)
-(* --------------------------- Relations on Setoids --------------------- *)
-(*------------------------------------------------------------------------*)
-(* throughout this section consider (S : CSetoid) and (R : S -> S -> Prop) *)
-
-
-(* Definition rel_wdr : Prop := forall x y z : S, R x y -> y [=] z -> R x z. *)
-(*
- primo tentativo ma R non e' ben tipato: si puo' fare il cast giusto (carrier di S)
- in modo da sfruttare "relation"?
- e' concettualmente sbagliato lavorare ad un livello piu' alto (Type) ? *)
-(*
-definition rel_wdr : \forall S: CSetoid. \forall x,y,z: S. \lambda R: relation S. Prop \def
- \lambda S: CSetoid. \lambda x,y,z: S. \lambda R: relation S.
- R S x y \to y = z \to R S x z.
-
-definition rel_wdr : \forall S: CSetoid. \forall x,y,z: (cs_crr S). \lambda R: relation (cs_crr S). Prop \def
- \lambda S: CSetoid. \lambda x,y,z: (cs_crr S). \lambda R: relation (cs_crr S).
- R (cs_crr S) x y \to y = z \to R (cs_crr S) x z.
-*)
-definition rel_wdr : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y,z: S.
- R x y \to y = z \to R x z.
-
-(*Definition rel_wdl : Prop := forall x y z : S, R x y -> x [=] z -> R z y.*)
-definition rel_wdl : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y,z: S.
- R x y \to x = z \to R z y.
-
-(* Definition rel_strext : CProp := forall x1 x2 y1 y2 : S, R x1 y1 -> (x1 [#] x2 or y1 [#] y2) or R x2 y2. *)
-definition rel_strext : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x1,x2,y1,y2: S.
- R x1 y1 \to (x1 \neq x2 \or y1 \neq y2) \or R x2 y2.
-
-
-(* Definition rel_strext_lft : CProp := forall x1 x2 y : S, R x1 y -> x1 [#] x2 or R x2 y. *)
-definition rel_strext_lft : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x1,x2,y: S.
- R x1 y \to (x1 \neq x2 \or R x2 y).
-
-(* Definition rel_strext_rht : CProp := forall x y1 y2 : S, R x y1 -> y1 [#] y2 or R x y2. *)
-definition rel_strext_rht : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y1,y2: S.
- R x y1 \to (y1 \neq y2 \or R x y2).
-
-
-lemma rel_strext_imp_lftarg : \forall S: CSetoid. \forall R: S \to S \to Prop.
- rel_strext S R \to rel_strext_lft S R.
-unfold rel_strext.
-unfold rel_strext_lft.
-intros.
-elim (H x1 x2 y y H1)
-[elim H2
- [left. assumption
- |absurd (y \neq y) [assumption | apply (ap_irreflexive S y)]
- ]
-|right. assumption
-]
-qed.
-
-
-lemma rel_strext_imp_rhtarg : \forall S: CSetoid. \forall R: S \to S \to Prop.
- rel_strext S R \to rel_strext_rht S R.
-unfold rel_strext.
-unfold rel_strext_rht.
-intros.
-elim (H x x y1 y2 H1)
-[elim H2
- [absurd (x \neq x) [assumption | apply (ap_irreflexive S x)]
- |left. assumption
- ]
-|right. assumption
-]
-qed.
-
-
-lemma rel_strextarg_imp_strext : \forall S: CSetoid. \forall R: S \to S \to Prop.
- (rel_strext_rht S R) \to (rel_strext_lft S R) \to (rel_strext S R).
-unfold rel_strext_rht.
-unfold rel_strext_lft.
-unfold rel_strext.
-intros.
-elim ((H x1 y1 y2) H2)
-[left. right. assumption
-|elim ((H1 x1 x2 y1) H2)
- [left. left. assumption
- |elim ((H x2 y1 y2) H4)
- [left. right. assumption
- |right. assumption.
- ]
- ]
-]
-qed.
-
-(* ---------- Definition of a setoid relation ----------------- *)
-(* The type of relations over a setoid. *)
-
-(* TODO
-record CSetoid_relation1 (S: CSetoid) : Type \def
- {csr_rel : S \to S \to Prop;
- csr_wdr : rel_wdr S csr_rel;
- csr_wdl : rel_wdl S csr_rel;
- csr_strext : rel_strext S csr_rel}.
-*)
-(* CORN
-Record CSetoid_relation : Type :=
- {csr_rel :> S -> S -> Prop;
- csr_wdr : rel_wdr csr_rel;
- csr_wdl : rel_wdl csr_rel;
- csr_strext : rel_strext csr_rel}.
-*)
-
-
-(* ---------- gli stessi risultati di prima ma in CProp ---------*)
-(*
-Variable R : S -> S -> CProp.
-Definition Crel_wdr : CProp := forall x y z : S, R x y -> y [=] z -> R x z.
-Definition Crel_wdl : CProp := forall x y z : S, R x y -> x [=] z -> R z y.
-Definition Crel_strext : CProp := forall x1 x2 y1 y2 : S,
- R x1 y1 -> R x2 y2 or x1 [#] x2 or y1 [#] y2.
-
-Definition Crel_strext_lft : CProp := forall x1 x2 y : S, R x1 y -> R x2 y or x1 [#] x2.
-Definition Crel_strext_rht : CProp := forall x y1 y2 : S, R x y1 -> R x y2 or y1 [#] y2.
-
-Lemma Crel_strext_imp_lftarg : Crel_strext -> Crel_strext_lft.
-Proof.
-unfold Crel_strext, Crel_strext_lft in |- *; intros H x1 x2 y H0.
-generalize (H x1 x2 y y).
-intro H1.
-elim (H1 H0).
-
-autobatch.
-
-intro H3.
-elim H3; intro H4.
-
-autobatch.
-elim (ap_irreflexive _ _ H4).
-Qed.
-
-Lemma Crel_strext_imp_rhtarg : Crel_strext -> Crel_strext_rht.
-unfold Crel_strext, Crel_strext_rht in |- *; intros H x y1 y2 H0.
-generalize (H x x y1 y2 H0); intro H1.
-elim H1; intro H2.
-
-autobatch.
-
-elim H2; intro H3.
-
-elim (ap_irreflexive _ _ H3).
-
-autobatch.
-Qed.
-
-Lemma Crel_strextarg_imp_strext :
- Crel_strext_rht -> Crel_strext_lft -> Crel_strext.
-unfold Crel_strext, Crel_strext_lft, Crel_strext_rht in |- *;
- intros H H0 x1 x2 y1 y2 H1.
-elim (H x1 y1 y2 H1); autobatch.
-intro H2.
-elim (H0 x1 x2 y2 H2); autobatch.
-Qed.
-*)
-
-
-
-
-(* ---- e questo ??????? -----*)
-
-(*Definition of a [CProp] setoid relation
-The type of relations over a setoid. *)
-(*
-Record CCSetoid_relation : Type :=
- {Ccsr_rel :> S -> S -> CProp;
- Ccsr_strext : Crel_strext Ccsr_rel}.
-
-Lemma Ccsr_wdr : forall R : CCSetoid_relation, Crel_wdr R.
-intro R.
-red in |- *; intros x y z H H0.
-elim (Ccsr_strext R x x y z H).
-
-autobatch.
-
-intro H1; elimtype False.
-elim H1; intro H2.
-
-exact (ap_irreflexive_unfolded _ _ H2).
-
-generalize H2.
-exact (eq_imp_not_ap _ _ _ H0).
-Qed.
-
-Lemma Ccsr_wdl : forall R : CCSetoid_relation, Crel_wdl R.
-intro R.
-red in |- *; intros x y z H H0.
-elim (Ccsr_strext R x z y y H).
-
-autobatch.
-
-intro H1; elimtype False.
-elim H1; intro H2.
-
-generalize H2.
-exact (eq_imp_not_ap _ _ _ H0).
-
-exact (ap_irreflexive_unfolded _ _ H2).
-Qed.
-
-Lemma ap_wdr : Crel_wdr (cs_ap (c:=S)).
-red in |- *; intros x y z H H0.
-generalize (eq_imp_not_ap _ _ _ H0); intro H1.
-elim (ap_cotransitive_unfolded _ _ _ H z); intro H2.
-
-assumption.
-
-elim H1.
-apply ap_symmetric_unfolded.
-assumption.
-Qed.
-
-Lemma ap_wdl : Crel_wdl (cs_ap (c:=S)).
-red in |- *; intros x y z H H0.
-generalize (ap_wdr y x z); intro H1.
-apply ap_symmetric_unfolded.
-apply H1.
-
-apply ap_symmetric_unfolded.
-assumption.
-
-assumption.
-Qed.
-
-Lemma ap_wdr_unfolded : forall x y z : S, x [#] y -> y [=] z -> x [#] z.
-Proof ap_wdr.
-
-Lemma ap_wdl_unfolded : forall x y z : S, x [#] y -> x [=] z -> z [#] y.
-Proof ap_wdl.
-
-Lemma ap_strext : Crel_strext (cs_ap (c:=S)).
-red in |- *; intros x1 x2 y1 y2 H.
-case (ap_cotransitive_unfolded _ _ _ H x2); intro H0.
-
-autobatch.
-
-case (ap_cotransitive_unfolded _ _ _ H0 y2); intro H1.
-
-autobatch.
-
-right; right.
-apply ap_symmetric_unfolded.
-assumption.
-Qed.
-
-Definition predS_well_def (P : S -> CProp) : CProp := forall x y : S,
- P x -> x [=] y -> P y.
-
-End CSetoid_relations_and_predicates.
-
-Declare Left Step ap_wdl_unfolded.
-Declare Right Step ap_wdr_unfolded.
-*)
-
-
-
-
-
-
-
-
-
-(*------------------------------------------------------------------------*)
-(* ------------------------- Functions between setoids ------------------ *)
-(*------------------------------------------------------------------------*)
-
-(* Such functions must preserve the setoid equality
-and be strongly extensional w.r.t. the apartness, i.e.
-if f(x,y) # f(x1,y1), then x # x1 or y # y1.
-For every arity this has to be defined separately. *)
-
-(* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2) *)
-
-(* First we consider unary functions. *)
-
-(*
-In the following two definitions,
-f is a function from (the carrier of) S1 to (the carrier of) S2 *)
-
-(* Nota: senza le parentesi di (S1 \to S2) non funziona, perche'? *)
-definition fun_wd : \forall S1,S2 : CSetoid. (S1 \to S2) \to Prop \def
- \lambda S1,S2 : CSetoid.\lambda f : S1 \to S2. \forall x,y : S1.
- x = y \to f x = f y.
-
-definition fun_strext : \forall S1,S2 : CSetoid. (S1 \to S2) \to Prop \def
- \lambda S1,S2 : CSetoid.\lambda f : S1 \to S2. \forall x,y : S1.
- (f x \neq f y) \to (x \neq y).
-
-lemma fun_strext_imp_wd : \forall S1,S2 : CSetoid. \forall f : S1 \to S2.
- fun_strext S1 S2 f \to fun_wd S1 S2 f.
-unfold fun_strext.
-unfold fun_wd.
-intros.
-apply not_ap_imp_eq.
-unfold.intro.
-apply (eq_imp_not_ap ? ? ? H1).
-apply H.assumption.
-qed.
-
-(* funzioni tra setoidi *)
-record CSetoid_fun (S1,S2 : CSetoid) : Type \def
- {csf_fun : S1 \to S2;
- csf_strext : (fun_strext S1 S2 csf_fun)}.
-
-lemma csf_wd : \forall S1,S2 : CSetoid. \forall f : CSetoid_fun S1 S2. fun_wd S1 S2 (csf_fun S1 S2 f).
-intros.
-apply fun_strext_imp_wd.
-apply csf_strext.
-qed.
-
-definition Const_CSetoid_fun : \forall S1,S2: CSetoid. S2 \to CSetoid_fun S1 S2.
-intros. apply (mk_CSetoid_fun S1 S2 (\lambda x:S1.c)).
-unfold.intros.
-elim (ap_irreflexive ? ? H).
-qed.
-
-
-(* ---- Binary functions ------*)
-(* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2 \to S3) *)
-
-definition bin_fun_wd : \forall S1,S2,S3 : CSetoid. (S1 \to S2 \to S3) \to Prop \def
- \lambda S1,S2,S3 : CSetoid. \lambda f : S1 \to S2 \to S3. \forall x1,x2: S1. \forall y1,y2: S2.
- x1 = x2 \to y1 = y2 \to f x1 y1 = f x2 y2.
-
-(*
-Definition bin_fun_strext : CProp := forall x1 x2 y1 y2,
- f x1 y1 [#] f x2 y2 -> x1 [#] x2 or y1 [#] y2.
-*)
-
-definition bin_fun_strext: \forall S1,S2,S3 : CSetoid. (S1 \to S2 \to S3) \to Prop \def
- \lambda S1,S2,S3 : CSetoid. \lambda f : S1 \to S2 \to S3. \forall x1,x2: S1. \forall y1,y2: S2.
- f x1 y1 \neq f x2 y2 \to x1 \neq x2 \lor y1 \neq y2.
-
-lemma bin_fun_strext_imp_wd : \forall S1,S2,S3: CSetoid.\forall f:S1 \to S2 \to S3.
-bin_fun_strext ? ? ? f \to bin_fun_wd ? ? ? f.
-intros.unfold in H.
-unfold.intros.
-apply not_ap_imp_eq.unfold.intro.
-elim (H x1 x2 y1 y2 H3).
-apply (eq_imp_not_ap ? ? ? H1 H4).
-apply (eq_imp_not_ap ? ? ? H2 H4).
-qed.
-
-
-
-record CSetoid_bin_fun (S1,S2,S3: CSetoid) : Type \def
- {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.
- bin_fun_wd S1 S2 S3 (csbf_fun S1 S2 S3 f).
-intros.
-apply bin_fun_strext_imp_wd.
-apply csbf_strext.
-qed.
-
-lemma csf_wd_unfolded : \forall S1,S2: CSetoid. \forall f : CSetoid_fun S1 S2. \forall x,x' : S1.
- x = x' \to (csf_fun S1 S2 f) x = (csf_fun S1 S2 f) x'.
-intros.
-apply (csf_wd S1 S2 f x x').
-assumption.
-qed.
-
-lemma csf_strext_unfolded : \forall S1,S2: CSetoid. \forall f : CSetoid_fun S1 S2. \forall x,y : S1.
-(csf_fun S1 S2 f) x \neq (csf_fun S1 S2 f) y \to x \neq y.
-intros.
-apply (csf_strext S1 S2 f x y).
-assumption.
-qed.
-
-lemma csbf_wd_unfolded : \forall S1,S2,S3 : CSetoid. \forall f : CSetoid_bin_fun S1 S2 S3. \forall x,x':S1.
-\forall y,y' : S2. x = x' \to y = y' \to (csbf_fun S1 S2 S3 f) x y = (csbf_fun S1 S2 S3 f) x' y'.
-intros.
-apply (csbf_wd S1 S2 S3 f x x' y y'); assumption.
-qed.
-
-(* Hint Resolve csf_wd_unfolded csbf_wd_unfolded: algebra_c.*)
-
-(* The unary and binary (inner) operations on a csetoid
-An operation is a function with domain(s) and co-domain equal. *)
-
-(* Properties of binary operations *)
-
-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 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.
-
-definition un_op_wd : \forall S:CSetoid. (S \to S) \to Prop \def
-\lambda S: CSetoid. \lambda f: (S \to S). fun_wd S S f.
-
-
-definition un_op_strext: \forall S:CSetoid. (S \to S) \to Prop \def
-\lambda S:CSetoid. \lambda f: (S \to S). fun_strext S S f.
-
-
-definition CSetoid_un_op : CSetoid \to Type \def
-\lambda S:CSetoid. CSetoid_fun S S.
-
-definition mk_CSetoid_un_op : \forall S:CSetoid. \forall f: S \to S. fun_strext S S f \to CSetoid_fun S S
- \def
-\lambda S:CSetoid. \lambda f: S \to S. mk_CSetoid_fun S S f.
-
-lemma id_strext : \forall S:CSetoid. un_op_strext S (\lambda x:S. x).
-unfold un_op_strext.
-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.
-exact H.
-qed.
-
-definition id_un_op : \forall S:CSetoid. CSetoid_un_op S
- \def \lambda S: CSetoid. mk_CSetoid_un_op S (\lambda x : cs_crr S.x) (id_strext S).
-
-definition un_op_fun: \forall S:CSetoid. CSetoid_un_op S \to CSetoid_fun S S
-\def \lambda S.\lambda f.f.
-
-coercion cic:/matita/algebra/CoRN/Setoids/un_op_fun.con.
-
-definition cs_un_op_strext : \forall S:CSetoid. \forall f: CSetoid_fun S S. fun_strext S S (csf_fun S S f) \def
-\lambda S:CSetoid. \lambda f : CSetoid_fun S S. csf_strext S S f.
-
-lemma un_op_wd_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op S.
-\forall x, y : S.
-x = y \to (csf_fun S S op) x = (csf_fun S S op) y.
-intros.
-apply (csf_wd S S ?).assumption.
-qed.
-
-lemma un_op_strext_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op S.
-\forall x, y : S.
- (csf_fun S S op) x \neq (csf_fun S S op) y \to x \neq y.
-exact cs_un_op_strext.
-qed.
-
-
-(* Well-defined binary operations on a setoid. *)
-
-definition bin_op_wd : \forall S:CSetoid. (S \to S \to S) \to Prop \def
-\lambda S:CSetoid. bin_fun_wd S S S.
-
-definition bin_op_strext : \forall S:CSetoid. (S \to S \to S) \to Prop \def
-\lambda S:CSetoid. bin_fun_strext S S S.
-
-definition CSetoid_bin_op : CSetoid \to Type \def
-\lambda S:CSetoid. CSetoid_bin_fun S S S.
-
-
-definition mk_CSetoid_bin_op : \forall S:CSetoid. \forall f: S \to S \to S.
-bin_fun_strext S S S f \to CSetoid_bin_fun S S S \def
- \lambda S:CSetoid. \lambda f: S \to S \to S.
- mk_CSetoid_bin_fun S S S f.
-
-(* da controllare che sia ben tipata
-definition cs_bin_op_wd : \forall S:CSetoid. ? \def
-\lambda S:CSetoid. csbf_wd S S S.
-*)
-definition cs_bin_op_wd : \forall S:CSetoid. \forall f: CSetoid_bin_fun S S S. bin_fun_wd S S S (csbf_fun S S S f) \def
-\lambda S:CSetoid. csbf_wd S S S.
-
-definition cs_bin_op_strext : \forall S:CSetoid. \forall f: CSetoid_bin_fun S S S. bin_fun_strext S S S (csbf_fun S S S f) \def
-\lambda S:CSetoid. csbf_strext S S S.
-
-
-
-(* Identity Coercion bin_op_bin_fun : CSetoid_bin_op >-> CSetoid_bin_fun. *)
-
-definition bin_op_bin_fun: \forall S:CSetoid. CSetoid_bin_op S \to CSetoid_bin_fun S S S
-\def \lambda S.\lambda f.f.
-
-coercion cic:/matita/algebra/CoRN/Setoids/bin_op_bin_fun.con.
-
-
-
-
-lemma bin_op_wd_unfolded :\forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall x1, x2, y1, y2 : S.
- x1 = x2 \to y1 = y2 \to (csbf_fun S S S op) x1 y1 = (csbf_fun S S S op) x2 y2.
-exact cs_bin_op_wd.
-qed.
-
-lemma bin_op_strext_unfolded : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall x1, x2, y1, y2 : S.
- (csbf_fun S S S op) x1 y1 \neq (csbf_fun S S S op) x2 y2 \to x1 \neq x2 \lor y1 \neq y2.
-exact cs_bin_op_strext.
-qed.
-
-lemma bin_op_is_wd_un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
- un_op_wd S (\lambda x : cs_crr S. ((csbf_fun S S S op) x c)).
-intros. unfold. unfold.
-intros. apply bin_op_wd_unfolded [ assumption | apply eq_reflexive_unfolded ]
-qed.
-
-lemma bin_op_is_wd_un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
- un_op_wd S (\lambda x : cs_crr S. ((csbf_fun S S S op) c x)).
-intros. unfold. unfold.
-intros. apply bin_op_wd_unfolded [ apply eq_reflexive_unfolded | assumption ]
-qed.
-
-
-lemma bin_op_is_strext_un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
- un_op_strext S (\lambda x : cs_crr S. ((csbf_fun S S S op) x c)).
-intros. unfold un_op_strext. unfold fun_strext.
-intros.
-cut (x \neq y \lor c \neq c)
-[ elim Hcut
- [ assumption
- | generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
- ]
-| apply (bin_op_strext_unfolded S op x y c c). assumption.
-]
-qed.
-
-lemma bin_op_is_strext_un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
- un_op_strext S (\lambda x : cs_crr S. ((csbf_fun S S S op) c x)).
-intros. unfold un_op_strext. unfold fun_strext.
-intros.
-cut (c \neq c \lor x \neq y)
-[ elim Hcut
- [ generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
- | assumption
- ]
-| apply (bin_op_strext_unfolded S op c c x y). assumption.
-]
-qed.
-
-definition bin_op2un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S.
-\forall c : cs_crr S. CSetoid_un_op S \def
- \lambda S:CSetoid. \lambda op: CSetoid_bin_op S. \lambda c : cs_crr S.
- mk_CSetoid_un_op S (\lambda x:cs_crr S. ((csbf_fun S S S op) c x))
- (bin_op_is_strext_un_op_rht S op c).
-
-definition bin_op2un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S.
-\forall c : cs_crr S. CSetoid_un_op S \def
- \lambda S:CSetoid. \lambda op: CSetoid_bin_op S. \lambda c : cs_crr S.
- mk_CSetoid_un_op S (\lambda x:cs_crr S. ((csbf_fun S S S op) x c))
- (bin_op_is_strext_un_op_lft S op c).
-
-(*
-Definition bin_op2un_op_rht (op : CSetoid_bin_op) (c : S) : CSetoid_un_op :=
- Build_CSetoid_un_op (fun x : S => op c x) (bin_op_is_strext_un_op_rht op c).
-
-
-Definition bin_op2un_op_lft (op : CSetoid_bin_op) (c : S) : CSetoid_un_op :=
- Build_CSetoid_un_op (fun x : S => op x c) (bin_op_is_strext_un_op_lft op c).
-*)
-
-
-(*
-Implicit Arguments commutes [S].
-Implicit Arguments associative [S].
-Hint Resolve bin_op_wd_unfolded un_op_wd_unfolded: algebra_c.
-*)
-
-(*The binary outer operations on a csetoid*)
-
-
-(*
-Well-defined outer operations on a setoid.
-*)
-definition outer_op_well_def : \forall S1,S2:CSetoid. (S1 \to S2 \to S2) \to Prop \def
-\lambda S1,S2:CSetoid. bin_fun_wd S1 S2 S2.
-
-definition outer_op_strext : \forall S1,S2:CSetoid. (S1 \to S2 \to S2) \to Prop \def
-\lambda S1,S2:CSetoid. bin_fun_strext S1 S2 S2.
-
-definition CSetoid_outer_op : \forall S1,S2:CSetoid.Type \def
-\lambda S1,S2:CSetoid.
- CSetoid_bin_fun S1 S2 S2.
-
-definition mk_CSetoid_outer_op : \forall S1,S2:CSetoid.
-\forall f : S1 \to S2 \to S2.
-bin_fun_strext S1 S2 S2 f \to CSetoid_bin_fun S1 S2 S2 \def
-\lambda S1,S2:CSetoid.
-mk_CSetoid_bin_fun S1 S2 S2.
-
-definition csoo_wd : \forall S1,S2:CSetoid. \forall f : CSetoid_bin_fun S1 S2 S2.
-bin_fun_wd S1 S2 S2 (csbf_fun S1 S2 S2 f) \def
-\lambda S1,S2:CSetoid.
-csbf_wd S1 S2 S2.
-
-definition csoo_strext : \forall S1,S2:CSetoid.
-\forall f : CSetoid_bin_fun S1 S2 S2.
-bin_fun_strext S1 S2 S2 (csbf_fun S1 S2 S2 f) \def
-\lambda S1,S2:CSetoid.
-csbf_strext S1 S2 S2.
-
-
-definition outer_op_bin_fun: \forall S:CSetoid.
-CSetoid_outer_op S S \to CSetoid_bin_fun S S S
-\def \lambda S.\lambda f.f.
-
-coercion cic:/matita/algebra/CoRN/Setoids/outer_op_bin_fun.con.
-(* begin hide
-Identity Coercion outer_op_bin_fun : CSetoid_outer_op >-> CSetoid_bin_fun.
-end hide *)
-
-lemma csoo_wd_unfolded :\forall S:CSetoid. \forall op : CSetoid_outer_op S S.
-\forall x1, x2, y1, y2 : S.
- x1 = x2 -> y1 = y2 -> (csbf_fun S S S op) x1 y1 = (csbf_fun S S S op) x2 y2.
-intros.
-apply csoo_wd[assumption|assumption]
-qed.
-
-(*
-Hint Resolve csoo_wd_unfolded: algebra_c.
-*)
-
-
-
-(*---------------------------------------------------------------*)
-(*--------------------------- Subsetoids ------------------------*)
-(*---------------------------------------------------------------*)
-
-(* Let S be a setoid, and P a predicate on the carrier of S *)
-(* Variable P : S -> CProp *)
-
-record subcsetoid_crr (S: CSetoid) (P: S \to Prop) : Type \def
- {scs_elem :> S;
- scs_prf : P scs_elem}.
-
-definition restrict_relation : \forall S:CSetoid. \forall R : S \to S \to Prop.
- \forall P: S \to Prop. relation (subcsetoid_crr S P) \def
- \lambda S:CSetoid. \lambda R : S \to S \to Prop.
- \lambda P: S \to Prop. \lambda a,b: subcsetoid_crr S P.
- match a with
- [ (mk_subcsetoid_crr x H) \Rightarrow
- match b with
- [ (mk_subcsetoid_crr y H) \Rightarrow R x y ]
- ].
-(* CPROP
-definition Crestrict_relation (R : Crelation S) : Crelation subcsetoid_crr :=
- fun a b : subcsetoid_crr =>
- match a, b with
- | Build_subcsetoid_crr x _, Build_subcsetoid_crr y _ => R x y
- end.
-*)
-
-definition subcsetoid_eq : \forall S:CSetoid. \forall P: S \to Prop.
- relation (subcsetoid_crr S P)\def
- \lambda S:CSetoid.
- restrict_relation S (cs_eq S).
-
-definition subcsetoid_ap : \forall S:CSetoid. \forall P: S \to Prop.
- relation (subcsetoid_crr S P)\def
- \lambda S:CSetoid.
- restrict_relation S (cs_ap S).
-
-(* N.B. da spostare in relations.ma... *)
-definition equiv : \forall A: Type. \forall R: relation A. Prop \def
- \lambda A: Type. \lambda R: relation A.
- (reflexive A R) \land (transitive A R) \land (symmetric A R).
-
-remark subcsetoid_equiv : \forall S:CSetoid. \forall P: S \to Prop.
-equiv ? (subcsetoid_eq S P).
-intros. unfold equiv. split
-[split
- [unfold. intro. elim x. simplify. apply (eq_reflexive S)
- |unfold. intros 3. elim y 2.
- elim x 2. elim z 2. simplify.
- exact (eq_transitive ? c1 c c2)
- ]
-| unfold. intros 2. elim x 2. elim y 2. simplify. exact (eq_symmetric ? c c1).
-]
-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 | 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)
-(* cotransitive *)
-|unfold.intros 2. elim x.generalize in match H1. elim y. elim z.simplify. simplify in H3.
-apply (ap_cotransitive ? ? ? H3)
-(* tight *)
-|unfold.intros.elim x. elim y.simplify.
-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).
-
-(* Subsetoid unary operations
-%\begin{convention}%
-Let [f] be a unary setoid operation on [S].
-%\end{convention}%
-*)
-
-(* Section SubCSetoid_unary_operations.
-Variable f : CSetoid_un_op S.
-*)
-
-definition un_op_pres_pred : \forall S:CSetoid. \forall P: S \to Prop.
- CSetoid_un_op S \to Prop \def
- \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
- \forall x : cs_crr S. P x \to P ((csf_fun S S f) x).
-
-definition restr_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.
- subcsetoid_crr S P \to subcsetoid_crr 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.\lambda a: subcsetoid_crr S P.
- match a with
- [ (mk_subcsetoid_crr x p) \Rightarrow
- (mk_subcsetoid_crr ? ? ((csf_fun S S f) x) (pr x p))].
-
-(* TODO *)
-lemma restr_un_op_wd : \forall S:CSetoid. \forall P: S \to Prop.
-\forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
-un_op_wd (mk_SubCSetoid S P) (restr_un_op S P f pr).
-intros.
-unfold.unfold.intros 2.elim x 2.elim y 2.
-simplify.
-intro.
-normalize in H2.
-apply (un_op_wd_unfolded ? f ? ? H2).
-qed.
-
-lemma restr_un_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
-\forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
-un_op_strext (mk_SubCSetoid S P) (restr_un_op S P f pr).
-intros.unfold.unfold. intros 2.elim y 2. elim x 2.
-intros.normalize in H2.
-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).
- 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].
-*)
-
-(* Section SubCSetoid_binary_operations.
-Variable f : CSetoid_bin_op S.
-*)
-
-definition bin_op_pres_pred : \forall S:CSetoid. \forall P: S \to Prop.
-(CSetoid_bin_op S) \to Prop \def
- \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_bin_op S.
- \forall x,y : S. P x \to P y \to P ( (csbf_fun S S S f) x y).
-
-(*
-Assume [bin_op_pres_pred].
-*)
-
-(* Variable pr : bin_op_pres_pred. *)
-
-definition restr_bin_op : \forall S:CSetoid. \forall P:S \to Prop.
- \forall f: CSetoid_bin_op S.\forall op : (bin_op_pres_pred S P f).
- \forall a, b : subcsetoid_crr S P. subcsetoid_crr 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).
- \lambda a, b : subcsetoid_crr S P.
- match a with
- [ (mk_subcsetoid_crr x p) \Rightarrow
- match b with
- [ (mk_subcsetoid_crr y q) \Rightarrow
- (mk_subcsetoid_crr ? ? ((csbf_fun S S S f) x y) (pr x y p q))]
- ].
-
-
-(* TODO *)
-lemma restr_bin_op_well_def : \forall S:CSetoid. \forall P: S \to Prop.
-\forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
-bin_op_wd (mk_SubCSetoid S P) (restr_bin_op S P f pr).
-intros.
-unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
-simplify.
-intros.
-normalize in H4.
-normalize in H5.
-apply (cs_bin_op_wd ? f ? ? ? ? H4 H5).
-qed.
-
-lemma restr_bin_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
-\forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
-bin_op_strext (mk_SubCSetoid S P) (restr_bin_op S P f pr).
-intros.unfold.unfold. intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
-simplify.intros.
-normalize 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.
- 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.
-intros 3.
-elim z 2.elim y 2. elim x 2.
-whd.
-apply H.
-qed.
-
-definition caseZ_diff: \forall A:Type.Z \to (nat \to nat \to A) \to A \def
-\lambda A:Type.\lambda z:Z.\lambda f:nat \to nat \to A.
- match z with
- [OZ \Rightarrow f O O
- |(pos n) \Rightarrow f (S n) O
- |(neg n) \Rightarrow f O (S n)].
-
-(* Zminus.ma *)
-theorem Zminus_S_S : \forall n,m:nat.
-Z_of_nat (S n) - S m = Z_of_nat n - m.
-intros.
-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).
-intros.
-(* perche' apply nat_elim2 non funziona?? *)
-apply (nat_elim2 (\lambda m,n.caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = f m n)).
-intro.simplify.
-apply (nat_case n1).simplify.
-apply eq_reflexive.
-intro.simplify.apply eq_reflexive.
-intro.simplify.apply eq_reflexive.
-intros 2.
-rewrite > (Zminus_S_S n1 m1).
-intros.
-cut (f n1 m1 = f (S n1) (S m1)).
-apply eq_symmetric_unfolded.
-apply eq_transitive.
-apply f. apply n1. apply m1.
-apply eq_symmetric_unfolded.assumption.
-apply eq_symmetric_unfolded.assumption.
-apply H.
-autobatch.
-qed.
-
-(*
-Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
-*)
-
-
-definition nat_less_n_fun : \forall S:CSetoid. \forall n:nat. ? \def
- \lambda S:CSetoid. \lambda n:nat. \lambda f: \forall i:nat. i < n \to S.
- \forall i,j : nat. eq nat i j \to (\forall H : i < n.
- \forall H' : j < n . (f i H) = (f j H')).
-
-definition nat_less_n_fun' : \forall S:CSetoid. \forall n:nat. ? \def
- \lambda S:CSetoid. \lambda n:nat. \lambda f: \forall i: nat. i <= n \to S.
- \forall i,j : nat. eq nat i j \to \forall H : i <= n.
- \forall H' : j <= n. f i H = f j H'.
-logic/connectives.ma
-logic/coimplication.ma logic/connectives.ma
-logic/connectives2.ma higher_order_defs/relations.ma
-logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma
-Z/z.ma datatypes/bool.ma nat/nat.ma
-Z/plus.ma Z/z.ma nat/minus.ma
Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma
+Z/moebius.ma Z/sigma_p.ma nat/factorization.ma
+Z/times.ma Z/plus.ma nat/lt_arith.ma
Z/orders.ma Z/z.ma logic/connectives.ma nat/orders.ma
-Z/compare.ma Z/orders.ma nat/compare.ma
Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma
-Z/times.ma Z/plus.ma nat/lt_arith.ma
+Z/plus.ma Z/z.ma nat/minus.ma
+Z/compare.ma Z/orders.ma nat/compare.ma
Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
-Z/moebius.ma Z/sigma_p.ma nat/factorization.ma
-nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma
-nat/binomial.ma nat/factorial2.ma nat/iteration2.ma
-nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sqrt.ma
-nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma
+Z/z.ma datatypes/bool.ma nat/nat.ma
+datatypes/constructors.ma logic/equality.ma
+datatypes/compare.ma
+datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma
+algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma
+algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma
+algebra/semigroups.ma higher_order_defs/functions.ma
+algebra/monoids.ma algebra/semigroups.ma
+demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma
+demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma
+demo/realisability.ma datatypes/constructors.ma logic/connectives.ma
+list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma
+list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma
+list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
+logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma
+logic/connectives.ma
+logic/coimplication.ma logic/connectives.ma
+logic/connectives2.ma higher_order_defs/relations.ma
+nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma
nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma
+nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma
+nat/congruence.ma nat/primes.ma nat/relevant_equations.ma
+nat/minus.ma nat/compare.ma nat/le_arith.ma
+nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
+nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma
nat/factorial.ma nat/le_arith.ma
-nat/lt_arith.ma nat/div_and_mod.ma
-nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma
-nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma
-nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma
+nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma
+nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
+nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma
+nat/minimization.ma nat/minus.ma
+nat/gcd.ma nat/lt_arith.ma nat/primes.ma
nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma
nat/le_arith.ma nat/orders.ma nat/times.ma
-nat/minimization.ma nat/minus.ma
-nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma
+nat/times.ma nat/plus.ma
+nat/gcd_properties1.ma nat/gcd.ma
nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma
-nat/plus.ma nat/nat.ma
-nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma
-nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma
-nat/div_and_mod_diseq.ma nat/lt_arith.ma
-nat/orders.ma higher_order_defs/ordering.ma logic/connectives.ma nat/nat.ma
-nat/euler_theorem.ma nat/map_iter_p.ma nat/nat.ma nat/totient.ma
-nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma
-nat/chebyshev_thm.ma nat/neper.ma
-nat/congruence.ma nat/primes.ma nat/relevant_equations.ma
-nat/gcd.ma nat/lt_arith.ma nat/primes.ma
+nat/lt_arith.ma nat/div_and_mod.ma
+nat/factorization.ma nat/ord.ma
nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma
-nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma
nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
-nat/map_iter_p.ma nat/count.ma nat/permutation.ma
nat/factorial2.ma nat/exp.ma nat/factorial.ma
-nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
-nat/times.ma nat/plus.ma
-nat/o.ma nat/binomial.ma nat/sqrt.ma
-nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma
-nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma
-nat/gcd_properties1.ma nat/gcd.ma
-nat/factorization.ma nat/ord.ma
-nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma
-nat/minus.ma nat/compare.ma nat/le_arith.ma
+nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma
nat/nat.ma higher_order_defs/functions.ma
+nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma
+nat/map_iter_p.ma nat/count.ma nat/permutation.ma
+nat/orders.ma higher_order_defs/ordering.ma logic/connectives.ma nat/nat.ma
+nat/plus.ma nat/nat.ma
+nat/euler_theorem.ma nat/nat.ma nat/map_iter_p.ma nat/totient.ma
+nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma
+nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma
nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma
-nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma
-nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma
+nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma
+nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma
+nat/chebyshev_thm.ma nat/neper.ma
+nat/div_and_mod_diseq.ma nat/lt_arith.ma
+nat/binomial.ma nat/factorial2.ma nat/iteration2.ma
+nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma
+nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma
+nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma
+nat/o.ma nat/binomial.ma nat/sqrt.ma
+nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sqrt.ma
+Q/q.ma Z/compare.ma Z/plus.ma
+Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma
decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma
+decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma
decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma
decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma
decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma
decidable_kit/fgraph.ma decidable_kit/fintype.ma
-decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma
-datatypes/constructors.ma logic/equality.ma
-datatypes/compare.ma
-datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma
-demo/realisability.ma datatypes/constructors.ma logic/connectives.ma
-demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma
-demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma
-algebra/monoids.ma algebra/semigroups.ma
-algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma
-algebra/semigroups.ma higher_order_defs/functions.ma
-algebra/finite_groups.ma nat/relevant_equations.ma algebra/groups.ma
-algebra/CoRN/SemiGroups.ma algebra/CoRN/SetoidInc.ma
-algebra/CoRN/SetoidFun.ma algebra/CoRN/Setoids.ma higher_order_defs/relations.ma
-algebra/CoRN/Setoids.ma Z/plus.ma datatypes/constructors.ma higher_order_defs/relations.ma logic/equality.ma nat/nat.ma
-algebra/CoRN/SetoidInc.ma algebra/CoRN/SetoidFun.ma
+higher_order_defs/relations.ma logic/connectives.ma
higher_order_defs/functions.ma logic/equality.ma
higher_order_defs/ordering.ma logic/equality.ma
-higher_order_defs/relations.ma logic/connectives.ma
-Q/q.ma Z/compare.ma Z/plus.ma
-Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
-list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma
-list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
-list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/in.ma
projects / helm.git / commitdiff