From: Enrico Tassi Date: Tue, 27 May 2008 08:51:59 +0000 (+0000) Subject: CoRN moved in contribs X-Git-Tag: make_still_working~5121 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=cb3513ef18e52e6e054f8bc99abb833afbb2aee5;p=helm.git CoRN moved in contribs --- diff --git a/helm/software/matita/contribs/CoRN/Makefile b/helm/software/matita/contribs/CoRN/Makefile new file mode 100644 index 000000000..a3e891435 --- /dev/null +++ b/helm/software/matita/contribs/CoRN/Makefile @@ -0,0 +1,16 @@ +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 diff --git a/helm/software/matita/contribs/CoRN/algebra/CoRN/SemiGroups.ma b/helm/software/matita/contribs/CoRN/algebra/CoRN/SemiGroups.ma new file mode 100644 index 000000000..1ce9f1f9b --- /dev/null +++ b/helm/software/matita/contribs/CoRN/algebra/CoRN/SemiGroups.ma @@ -0,0 +1,400 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +(* $Id: CSemiGroups.v,v 1.10 2004/09/24 15:30:34 loeb Exp $ *) +(* printing [+] %\ensuremath+% #+# *) +(* printing {+} %\ensuremath+% #+# *) + +(* Require Export CSetoidInc. *) + +(* Begin_SpecReals *) + +set "baseuri" "cic:/matita/algebra/CoRN/CSemiGroups". +include "algebra/CoRN/SetoidInc.ma". + +(*------------------------------------------------------------------*) +(* Semigroups - Definition of the notion of Constructive Semigroup *) +(*------------------------------------------------------------------*) + +definition is_CSemiGroup : \forall A : CSetoid. \forall op: CSetoid_bin_op A. Prop \def +\lambda A : CSetoid. \lambda op: CSetoid_bin_op A. CSassociative A (csbf_fun A A A op). + +record CSemiGroup : Type \def + {csg_crr :> CSetoid; + csg_op : CSetoid_bin_op csg_crr; + csg_proof : is_CSemiGroup csg_crr csg_op}. + +(* +Implicit Arguments csg_op [c]. +Infix "[+]" := csg_op (at level 50, left associativity). +End_SpecReals *) + + + +(*--------------------------------------------------------------*) +(* Semigroup axioms - The axiomatic properties of a semi group *) +(*--------------------------------------------------------------*) +(* Variable G : CSemiGroup. *) + +lemma CSemiGroup_is_CSemiGroup : \forall G : CSemiGroup. is_CSemiGroup (csg_crr G) (csg_op G). +intro. +elim G. simplify. exact H. +qed. +(* CoRN +Lemma CSemiGroup_is_CSemiGroup : is_CSemiGroup G csg_op.*) + +lemma plus_assoc : \forall G : CSemiGroup. +CSassociative G (csbf_fun G G G (csg_op G)). +exact CSemiGroup_is_CSemiGroup. +qed. + +(*--------------------------------------------------------------*) +(* Semigroup basics *) +(*--------------------------------------------------------------*) + +lemma plus_assoc_unfolded : \forall G : CSemiGroup. \forall x,y,z : ?. + (csbf_fun G G G (csg_op G) x (csbf_fun G G G (csg_op G) y z)) = + (csbf_fun G G G (csg_op G) (csbf_fun G G G (csg_op G) x y) z). + intros. + apply plus_assoc. +qed. + +(* Section p71R1. *) + +(* Morphism +%\begin{convention}% +Let [S1 S2:CSemiGroup]. +%\end{convention}% +*) + +(* Variable S1:CSemiGroup. +Variable S2:CSemiGroup. *) + +definition morphism_of_CSemiGroups: \forall S1,S2: CSemiGroup. \forall f: CSetoid_fun S1 S2. + Prop \def + \lambda S1,S2: CSemiGroup. \lambda f: CSetoid_fun S1 S2. + (\forall a,b:S1. (csf_fun S1 S2 f (csbf_fun ? ? ? (csg_op ?) a b)) = + (csbf_fun ? ? ? (csg_op ?) (csf_fun S1 S2 f a) (csf_fun S1 S2 f b))). + +(* End p71R1. *) + +(* About the unit *) + +(* Zero ????? *) + +definition is_rht_unit: \forall S: CSemiGroup. \forall op : CSetoid_bin_op S. \forall Zero: ?. Prop + \def + \lambda S: CSemiGroup. \lambda op : CSetoid_bin_op S. \lambda Zero: ?. + \forall x:?. (csbf_fun ? ? ? op x Zero) = x. + +(* Definition is_rht_unit S (op : CSetoid_bin_op S) Zero : Prop := forall x, op x Zero [=] x. *) + +(* End_SpecReals *) + +definition is_lft_unit: \forall S: CSemiGroup. \forall op : CSetoid_bin_op S. \forall Zero: ?. Prop + \def + \lambda S: CSemiGroup. \lambda op : CSetoid_bin_op S. \lambda Zero: ?. + \forall x:?. (csbf_fun ? ? ? op Zero x) = x. + + +(* Implicit Arguments is_lft_unit [S]. *) + +(* Begin_SpecReals *) + +(* Implicit Arguments is_rht_unit [S]. *) + +(* An alternative definition: +*) + +definition is_unit: \forall S:CSemiGroup. S \to Prop \def +\lambda S:CSemiGroup. +\lambda e. (\forall (a:S). (csbf_fun ? ? ? (csg_op ?) e a) = a \and (csbf_fun ? ? ? (csg_op ?) a e) + = a). + +lemma cs_unique_unit : \forall S:CSemiGroup. \forall e,f:S. +(is_unit S e) \and (is_unit S f) \to e = f. +intros 3 (S e f). +unfold is_unit. +intro H. +elim H 0. +clear H. +intros (H0 H1). +elim (H0 f) 0. +clear H0. +intros (H2 H3). +elim (H1 e) 0. +clear H1. +intros (H4 H5). +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. *) diff --git a/helm/software/matita/contribs/CoRN/algebra/CoRN/SetoidFun.ma b/helm/software/matita/contribs/CoRN/algebra/CoRN/SetoidFun.ma new file mode 100644 index 000000000..ad16edf7b --- /dev/null +++ b/helm/software/matita/contribs/CoRN/algebra/CoRN/SetoidFun.ma @@ -0,0 +1,1303 @@ +(**************************************************************************) +(* ___ *) +(* ||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{%##a +priori##%}% 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 _ _ _ _). *) diff --git a/helm/software/matita/contribs/CoRN/algebra/CoRN/SetoidInc.ma b/helm/software/matita/contribs/CoRN/algebra/CoRN/SetoidInc.ma new file mode 100644 index 000000000..5bf067087 --- /dev/null +++ b/helm/software/matita/contribs/CoRN/algebra/CoRN/SetoidInc.ma @@ -0,0 +1,150 @@ +(**************************************************************************) +(* ___ *) +(* ||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. *) diff --git a/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma b/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma new file mode 100644 index 000000000..ee5f99610 --- /dev/null +++ b/helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.ma @@ -0,0 +1,1282 @@ +(**************************************************************************) +(* ___ *) +(* ||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'. diff --git a/helm/software/matita/contribs/CoRN/depends b/helm/software/matita/contribs/CoRN/depends new file mode 100644 index 000000000..ab5d4708f --- /dev/null +++ b/helm/software/matita/contribs/CoRN/depends @@ -0,0 +1,9 @@ +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 diff --git a/helm/software/matita/contribs/CoRN/root b/helm/software/matita/contribs/CoRN/root new file mode 100644 index 000000000..e6f78ade0 --- /dev/null +++ b/helm/software/matita/contribs/CoRN/root @@ -0,0 +1 @@ +baseuri=cic:/matita diff --git a/helm/software/matita/contribs/Makefile b/helm/software/matita/contribs/Makefile index e9ba4d1be..8c2e0647a 100644 --- a/helm/software/matita/contribs/Makefile +++ b/helm/software/matita/contribs/Makefile @@ -1,6 +1,6 @@ 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) $@;) diff --git a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma b/helm/software/matita/library/algebra/CoRN/SemiGroups.ma deleted file mode 100644 index 1ce9f1f9b..000000000 --- a/helm/software/matita/library/algebra/CoRN/SemiGroups.ma +++ /dev/null @@ -1,400 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. *) diff --git a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma deleted file mode 100644 index ad16edf7b..000000000 --- a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma +++ /dev/null @@ -1,1303 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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{%##a -priori##%}% 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 _ _ _ _). *) diff --git a/helm/software/matita/library/algebra/CoRN/SetoidInc.ma b/helm/software/matita/library/algebra/CoRN/SetoidInc.ma deleted file mode 100644 index 5bf067087..000000000 --- a/helm/software/matita/library/algebra/CoRN/SetoidInc.ma +++ /dev/null @@ -1,150 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. *) diff --git a/helm/software/matita/library/algebra/CoRN/Setoids.ma b/helm/software/matita/library/algebra/CoRN/Setoids.ma deleted file mode 100644 index ee5f99610..000000000 --- a/helm/software/matita/library/algebra/CoRN/Setoids.ma +++ /dev/null @@ -1,1282 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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'. diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index 8457f7ea2..76ed2b134 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,85 +1,81 @@ -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