From 3ac7c3ebc1d0af57466a577c555fac8994b1d61f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 17 Jan 2007 15:36:48 +0000 Subject: [PATCH] CoRN (new version) has been committed by Andrea in library/algebra/CoRN. --- matita/contribs/CoRN/algebra/SetoidFun.ma | 1173 ------------------- matita/contribs/CoRN/algebra/Setoids.ma | 1267 --------------------- matita/contribs/CoRN/makefile | 37 - 3 files changed, 2477 deletions(-) delete mode 100644 matita/contribs/CoRN/algebra/SetoidFun.ma delete mode 100644 matita/contribs/CoRN/algebra/Setoids.ma delete mode 100644 matita/contribs/CoRN/makefile diff --git a/matita/contribs/CoRN/algebra/SetoidFun.ma b/matita/contribs/CoRN/algebra/SetoidFun.ma deleted file mode 100644 index 96a583cfa..000000000 --- a/matita/contribs/CoRN/algebra/SetoidFun.ma +++ /dev/null @@ -1,1173 +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/Setoids.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 irrefl_apfun : forall A B : CSetoid, irreflexive (ap_fun A B). -intros A B. -unfold irreflexive in |- *. -intros f. -unfold ap_fun in |- *. -red in |- *. -intro H. -elim H. -intros a H0. -set (H1 := ap_irreflexive_unfolded B (f a)) in *. -intuition. -Qed. -*) - - -lemma cotrans_apfun : \forall A,B : CSetoid. cotransitive (CSetoid_fun A B) (ap_fun A B). -intros (A B). -unfold. -unfold ap_fun. -intros (f g H h). -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). -intros.unfold. -intros. -unfold .unfold. -elim H. -apply (ex_intro ? ? a). -apply ap_symmetric_unfolded. -assumption. -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. - -(* -Definition is_nullary_operation (S:CSetoid) (s:S):Prop := 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))). -(* str_ext *) -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 automaticamente *) -lemma mycor: ∀S. CSetoid_bin_op S → (S → S → S). - intros; - unfold in c; - apply (c c1 c2). -qed. -coercion cic:/matita/algebra/CoRN/SetoidFun/mycor.con 2. - -(* Mettendola a mano con una beta-espansione funzionerebbe *) -(*lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (\lambda e.mycor ? (comp_as_bin_op A) e)).*) -(* Questo sarebbe anche meglio: senza beta-espansione *) -(*lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (mycor ? (comp_as_bin_op A))).*) -(* QUESTO E' QUELLO ORIGINALE MA NON FUNZIONANTE *) -(* lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (comp_as_bin_op A)). *) -lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (comp_as_bin_op A)). -unfold associative in |- *. -unfold comp_as_bin_op in |- *. -intros A f g h. -simpl in |- *. -unfold eq_fun in |- *. -simpl in |- *. -intuition. -Qed. - -Lemma assoc_comp : forall A : CSetoid, associative (comp_as_bin_op A). -unfold associative in |- *. -unfold comp_as_bin_op in |- *. -intros A f g h. -simpl in |- *. -unfold eq_fun in |- *. -simpl in |- *. -intuition. -Qed. - -Section unary_and_binary_function_composition. - -Definition compose_CSetoid_bin_un_fun (A B C : CSetoid) - (f : CSetoid_bin_fun B B C) (g : CSetoid_fun A B) : CSetoid_bin_fun A A C. -intros A B C f g. -apply (Build_CSetoid_bin_fun A A C (fun a0 a1 : A => f (g a0) (g a1))). -intros x1 x2 y1 y2 H0. -assert (H10:= csbf_strext B B C f). -red in H10. -assert (H40 := csf_strext A B g). -red in H40. -elim (H10 (g x1) (g x2) (g y1) (g y2) H0); [left | right]; auto. -Defined. - -Definition compose_CSetoid_bin_fun A B C (f g : CSetoid_fun A B) - (h : CSetoid_bin_fun B B C) : CSetoid_fun A C. -intros A B C f g h. -apply (Build_CSetoid_fun A C (fun a : A => h (f a) (g a))). -intros x y H. -elim (csbf_strext _ _ _ _ _ _ _ _ H); apply csf_strext. -Defined. - -Definition compose_CSetoid_un_bin_fun A B C (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 Build_CSetoid_bin_fun with (fun x y : B0 => g (f x y)). -intros x1 x2 y1 y2. -case f. -simpl in |- *. -unfold bin_fun_strext in |- *. -case g. -simpl in |- *. -unfold fun_strext in |- *. -intros gu gstrext fu fstrext H. -apply fstrext. -apply gstrext. -exact H. -Defined. - -End unary_and_binary_function_composition. - -(** ***Projections -*) - -Section function_projection. - -Lemma proj_bin_fun : forall A B C (f : CSetoid_bin_fun A B C) a, fun_strext (f a). -intros A B C f a. -red in |- *. -elim f. -intro fo. -simpl. -intros csbf_strext0 x y H. -elim (csbf_strext0 _ _ _ _ H); intro H0. - elim (ap_irreflexive_unfolded _ _ H0). -exact H0. -Qed. - -Definition projected_bin_fun A B C (f : CSetoid_bin_fun A B C) (a : A) := - Build_CSetoid_fun B C (f a) (proj_bin_fun A B C f a). - -End function_projection. - -Section BinProj. - -Variable S : CSetoid. - -Definition binproj1 (x y:S) := x. - -Lemma binproj1_strext : bin_fun_strext _ _ _ binproj1. -red in |- *; auto. -Qed. - -Definition cs_binproj1 : CSetoid_bin_op S. -red in |- *; apply Build_CSetoid_bin_op with binproj1. -apply binproj1_strext. -Defined. - -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 : CSetoid_fun S1 S2. -apply (Build_CSetoid_fun S1 S2 (fun x : S1 => op (f x))). -(* str_ext *) -unfold fun_strext in |- *; intros x y H. -apply (csf_strext _ _ f x y). -apply (csf_strext _ _ op _ _ H). -Defined. - -End CombiningUnaryOperations. - -End CombiningOperations. - -Section p66E2b4. - -(** **The Free Setoid -%\begin{convention}% Let [A:CSetoid]. -%\end{convention}% -*) -Variable A:CSetoid. - -Definition Astar := (list A). - -Definition empty_word := (nil A). - -Definition appA:= (app A). - -Fixpoint eq_fm (m:Astar)(k:Astar){struct m}:Prop:= -match m with -|nil => match k with - |nil => True - |cons a l => False - end -|cons b n => match k with - |nil => False - |cons a l => b[=]a /\ (eq_fm n l) - end -end. - -Fixpoint ap_fm (m:Astar)(k:Astar){struct m}: CProp := -match m with -|nil => match k with - |nil => CFalse - |cons a l => CTrue - end -|cons b n => match k with - |nil => CTrue - |cons a l => b[#]a or (ap_fm n l) - end -end. - -Lemma ap_fm_irreflexive: (irreflexive ap_fm). -unfold irreflexive. -intro x. -induction x. -simpl. -red. -intuition. - -simpl. -red. -intro H. -apply IHx. -elim H. -clear H. -generalize (ap_irreflexive A a). -unfold Not. -intuition. - -intuition. -Qed. - - -Lemma ap_fm_symmetric: Csymmetric ap_fm. -unfold Csymmetric. -intros x. -induction x. -intro y. -case y. -simpl. -intuition. - -simpl. -intuition. -simpl. -intro y. -case y. -simpl. -intuition. - -simpl. -intros c l H0. -elim H0. -generalize (ap_symmetric A a c). -intuition. -clear H0. -intro H0. -right. -apply IHx. -exact H0. -Qed. - -Lemma ap_fm_cotransitive : (cotransitive ap_fm). -unfold cotransitive. -intro x. -induction x. -simpl. -intro y. -case y. -intuition. - -intros c l H z. -case z. -simpl. -intuition. - -intuition. - -simpl. -intro y. -case y. -intros H z. -case z. -intuition. - -simpl. -intuition. - -intros c l H z. -case z. -intuition. - -simpl. -intros c0 l0. -elim H. -clear H. -intro H. -generalize (ap_cotransitive A a c H c0). -intuition. - -clear H. -intro H. -generalize (IHx l H l0). -intuition. -Qed. - -Lemma ap_fm_tight : (tight_apart eq_fm ap_fm). -unfold tight_apart. -intros x. -induction x. -simpl. -intro y. -case y. -red. -unfold Not. -intuition. - -intuition. - -intro y. -simpl. -case y. -intuition. - -intros c l. -generalize (IHx l). -red. -intro H0. -elim H0. -intros H1 H2. -split. -intro H3. -split. -red in H3. -generalize (ap_tight A a c). -intuition. - -apply H1. -intro H4. -apply H3. -right. -exact H4. - -intro H3. -elim H3. -clear H3. -intros H3 H4. -intro H5. -elim H5. -generalize (ap_tight A a c). -intuition. - -apply H2. -exact H4. -Qed. - -Definition free_csetoid_is_CSetoid:(is_CSetoid Astar eq_fm ap_fm):= - (Build_is_CSetoid Astar eq_fm ap_fm ap_fm_irreflexive ap_fm_symmetric - ap_fm_cotransitive ap_fm_tight). - -Definition free_csetoid_as_csetoid:CSetoid:= -(Build_CSetoid Astar eq_fm ap_fm free_csetoid_is_CSetoid). - -Lemma app_strext: - (bin_fun_strext free_csetoid_as_csetoid free_csetoid_as_csetoid - free_csetoid_as_csetoid appA). -unfold bin_fun_strext. -intros x1. -induction x1. -simpl. -intro x2. -case x2. -simpl. -intuition. - -intuition. - -intros x2 y1 y2. -simpl. -case x2. -case y2. -simpl. -intuition. - -simpl. -intuition. - -case y2. -simpl. -simpl in IHx1. -intros c l H. -elim H. -intuition. - -clear H. -generalize (IHx1 l y1 (nil A)). -intuition. - -simpl. -intros c l c0 l0. -intro H. -elim H. -intuition. - -generalize (IHx1 l0 y1 (cons c l)). -intuition. -Qed. - -Definition app_as_csb_fun: -(CSetoid_bin_fun free_csetoid_as_csetoid free_csetoid_as_csetoid - free_csetoid_as_csetoid):= - (Build_CSetoid_bin_fun free_csetoid_as_csetoid free_csetoid_as_csetoid - free_csetoid_as_csetoid appA app_strext). - -Lemma eq_fm_reflexive: forall (x:Astar), (eq_fm x x). -intro x. -induction x. -simpl. -intuition. - -simpl. -intuition. -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. - -Definition conjP (x : S) : CProp := P x and Q x. - -Lemma prj1 : forall x : S, conjP x -> P x. -intros x H; inversion_clear H; assumption. -Qed. - -Lemma prj2 : forall x : S, conjP x -> Q x. -intros x H; inversion_clear H; assumption. -Qed. - -Lemma conj_wd : pred_wd _ P -> pred_wd _ Q -> pred_wd _ conjP. -intros H H0. -red in |- *; intros x y H1 H2. -inversion_clear H1; split. - -apply H with x; assumption. - -apply H0 with x; 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 (x : S) : CProp := P x or Q x. - -Lemma inj1 : forall x : S, P x -> disj x. -intros; left; assumption. -Qed. - -Lemma inj2 : forall x : S, Q x -> disj x. -intros; right; assumption. -Qed. - -Lemma disj_wd : pred_wd _ P -> pred_wd _ Q -> pred_wd _ disj. -intros H H0. -red in |- *; intros x y H1 H2. -inversion_clear H1. - -left; apply H with x; assumption. - -right; apply H0 with x; assumption. -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 (x : S) : CProp := P x and (forall H : P x, R x H). - -Lemma ext1 : forall x : S, extend x -> P x. -intros x H; inversion_clear H; assumption. -Qed. - -Lemma ext2_a : forall x : S, extend x -> {H : P x | R x H}. -intros x H; inversion_clear H. -exists X; auto. -Qed. - -Lemma ext2 : forall (x : S) (Hx : extend x), R x (ProjT1 (ext2_a x Hx)). -intros; apply projT2. -Qed. - -Lemma extension_wd : pred_wd _ P -> - (forall (x y : S) Hx Hy, x [=] y -> R x Hx -> R y Hy) -> pred_wd _ extend. -intros H H0. -red in |- *; intros x y H1 H2. -elim H1; intros H3 H4; split. - -apply H with x; assumption. - -intro H5; apply H0 with x H3; [ apply H2 | apply H4 ]. -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. -*) - -Record BinPartFunct (S1 S2 : CSetoid) : Type := - {bpfdom : S1 -> CProp; - bdom_wd : pred_wd S1 bpfdom; - bpfpfun :> forall x : S1, bpfdom x -> S2; - bpfstrx : forall x y Hx Hy, bpfpfun x Hx [#] bpfpfun y Hy -> x [#] 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 (F : BinPartFunct S1 S2) x y Hx Hy, - x [=] y -> F x Hx [=] F y Hy. -intros. -apply not_ap_imp_eq; intro H0. -generalize (bpfstrx _ _ _ _ _ _ _ H0). -exact (eq_imp_not_ap _ _ _ H). -Qed. - -(** Similar for automorphisms. *) - -Record PartFunct (S : CSetoid) : Type := - {pfdom : S -> CProp; - dom_wd : pred_wd S pfdom; - pfpfun :> forall x : S, pfdom x -> S; - pfstrx : forall x y Hx Hy, pfpfun x Hx [#] pfpfun y Hy -> x [#] 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 (F : PartFunct S) x y Hx Hy, x [=] y -> F x Hx [=] F y Hy. -intros. -apply not_ap_imp_eq; intro H0. -generalize (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 : CSetoid_un_op S -> PartFunct S. -intros f. -apply - Build_PartFunct with (fun x : S => CTrue) (fun (x : S) (H : CTrue) => f x). -red in |- *; intros; auto. -intros x y Hx Hy H. -exact (csf_strext_unfolded _ _ f _ _ H). -Defined. - -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 := total_eq_part (Const_CSetoid_fun _ _ c). - -End Part_Function_Const. - -Section Part_Function_Id. - -Definition Fid := 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 *) -Let P := Dom F. -Let Q := Dom G. -(* end hide *) -Let R x := {Hx : P x | Q (F x Hx)}. - -Lemma part_function_comp_strext : forall x y (Hx : R x) (Hy : R y), - G (F x (ProjT1 Hx)) (ProjT2 Hx) [#] G (F y (ProjT1 Hy)) (ProjT2 Hy) -> x [#] y. -intros x y Hx Hy H. -exact (pfstrx _ _ _ _ _ _ (pfstrx _ _ _ _ _ _ H)). -Qed. - -Lemma part_function_comp_dom_wd : pred_wd S R. -red in |- *; intros x y H H0. -unfold R in |- *; inversion_clear H. -exists (dom_wd _ F x y x0 H0). -apply (dom_wd _ G) with (F x x0). -assumption. -apply pfwdef; assumption. -Qed. - -Definition Fcomp := Build_PartFunct _ R part_function_comp_dom_wd - (fun x (Hx : R x) => G (F x (ProjT1 Hx)) (ProjT2 Hx)) - part_function_comp_strext. - -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)}. - -Lemma bin_part_function_comp_strext : forall x y (Hx : R x) (Hy : R y), - G (F x (ProjT1 Hx)) (ProjT2 Hx) [#] G (F y (ProjT1 Hy)) (ProjT2 Hy) -> x [#] y. -intros x y Hx Hy H. -exact (bpfstrx _ _ _ _ _ _ _ (bpfstrx _ _ _ _ _ _ _ H)). -Qed. - -Lemma bin_part_function_comp_dom_wd : pred_wd S1 R. -red in |- *; intros x y H H0. -unfold R in |- *; inversion_clear H. -exists (bdom_wd _ _ F x y x0 H0). -apply (bdom_wd _ _ G) with (F x x0). -assumption. -apply bpfwdef; assumption. -Qed. - -Definition BinFcomp := Build_BinPartFunct _ _ R bin_part_function_comp_dom_wd - (fun x (Hx : R x) => G (F x (ProjT1 Hx)) (ProjT2 Hx)) - bin_part_function_comp_strext. - -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 A B (f : CSetoid_fun A B) := (forall a0 a1 : A, - a0 [#] a1 -> f a0 [#] f a1):CProp. - -Definition injective_weak A B (f : CSetoid_fun A B) := forall a0 a1 : A, - f a0 [=] f a1 -> a0 [=] a1. - -Definition surjective A B (f : CSetoid_fun A B) := (forall b : B, {a : A | f a [=] b}):CProp. - -Implicit Arguments injective [A B]. -Implicit Arguments injective_weak [A B]. -Implicit Arguments surjective [A B]. - -Lemma injective_imp_injective_weak : forall A B (f : CSetoid_fun A B), - injective f -> injective_weak f. -intros A B f. -unfold injective in |- *. -intro H. -unfold injective_weak in |- *. -intros a0 a1 H0. -apply not_ap_imp_eq. -red in |- *. -intro H1. -set (H2 := H a0 a1 H1) in *. -set (H3 := ap_imp_neq B (f a0) (f a1) H2) in *. -set (H4 := eq_imp_not_neq B (f a0) (f a1) H0) in *. -apply H4. -exact H3. -Qed. - -Definition bijective A B (f:CSetoid_fun A B) := injective f and surjective f. - -Implicit Arguments bijective [A B]. - -Lemma id_is_bij : forall A, bijective (id_un_op A). -intro A. -split. - red; simpl; auto. -intro b; exists b; apply eq_reflexive. -Qed. - -Lemma comp_resp_bij : forall A B C f g, bijective f -> bijective g -> - bijective (compose_CSetoid_fun A B C f g). -intros A B C f g. -intros H0 H1. -elim H0; clear H0; intros H00 H01. -elim H1; clear H1; intros H10 H11. -split. - intros a0 a1; simpl; intro. - apply H10; apply H00; auto. -intro c; simpl. -elim (H11 c); intros b H20. -elim (H01 b); intros a H30. -exists a. -Step_final (g b). -Qed. - -Lemma inv : forall A B (f:CSetoid_fun A B), - bijective f -> forall b : B, {a : A | f a [=] b}. -unfold bijective in |- *. -unfold surjective in |- *. -intuition. -Qed. - -Implicit Arguments inv [A B]. - -Definition invfun A B (f : CSetoid_fun A B) (H : bijective f) : B -> A. -intros A B f H H0. -elim (inv f H H0); intros a H2. -apply a. -Defined. - -Implicit Arguments invfun [A B]. - -Lemma inv1 : forall A B (f : CSetoid_fun A B) (H : bijective f) (b : B), - f (invfun f H b) [=] b. -intros A B f H b. -unfold invfun in |- *; case inv. -simpl; auto. -Qed. - -Lemma inv2 : forall A B (f : CSetoid_fun A B) (H : bijective f) (a : A), - invfun f H (f a) [=] a. -intros. -unfold invfun in |- *; case inv; simpl. -elim H; clear H; intros H0 H1. -intro x. -apply injective_imp_injective_weak. -auto. -Qed. - -Lemma inv_strext : forall A B (f : CSetoid_fun A B) (H : bijective f), - fun_strext (invfun f H). -intros A B f H x y. -intro H1. -elim H; intros H00 H01. -elim (H01 x); intros a0 H2. -elim (H01 y); intros a1 H3. -astepl (f a0). -astepr (f a1). -apply H00. -astepl (invfun f H x). -astepr (invfun f H y). -exact H1. -astepl (invfun f H (f a1)). -apply inv2. -apply injective_imp_injective_weak with (f := f); auto. -astepl (f a1). -astepl y. -apply eq_symmetric. -apply inv1. -apply eq_symmetric. -apply inv1. -astepl (invfun f H (f a0)). -apply inv2. - -apply injective_imp_injective_weak with (f := f); auto. -astepl (f a0). -astepl x. -apply eq_symmetric; apply inv1. -apply eq_symmetric; apply inv1. -Qed. - -Definition Inv A B f (H : bijective f) := - Build_CSetoid_fun B A (invfun f H) (inv_strext A B f H). - -Implicit Arguments Inv [A B]. - -Definition Inv_bij : forall A B (f : CSetoid_fun A B) (H : bijective f), - bijective (Inv f H). -intros A B f H. -unfold bijective in |- *. -split. -unfold injective in |- *. -unfold bijective in H. -unfold surjective in H. -elim H. -intros H0 H1. -intros b0 b1 H2. -elim (H1 b0). -intros a0 H3. -elim (H1 b1). -intros a1 H4. -astepl (Inv f (CAnd_intro _ _ H0 H1) (f a0)). -astepr (Inv f (CAnd_intro _ _ H0 H1) (f a1)). -cut (fun_strext f). -unfold fun_strext in |- *. -intros H5. -apply H5. -astepl (f a0). -astepr (f a1). -astepl b0. -astepr b1. -exact H2. -apply eq_symmetric. -unfold Inv in |- *. -simpl in |- *. -apply inv1. -apply eq_symmetric. -unfold Inv in |- *. -simpl in |- *. -apply inv1. -elim f. -intuition. - -unfold surjective in |- *. -intro a. -exists (f a). -unfold Inv in |- *. -simpl in |- *. -apply inv2. -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/matita/contribs/CoRN/algebra/Setoids.ma b/matita/contribs/CoRN/algebra/Setoids.ma deleted file mode 100644 index 5fc3725cc..000000000 --- a/matita/contribs/CoRN/algebra/Setoids.ma +++ /dev/null @@ -1,1267 +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/Setoid/cs_eq.con _ x y). - -interpretation "setoid apart" - 'neq x y = (cic:/matita/algebra/CoRN/Setoid/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. auto. -qed. -*) -lemma eq_transitive : \forall S : CSetoid. transitive S (cs_eq S). -intro. unfold. intros (x y z H H0). -generalize in match (ap_tight S x y). intro. -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' auto 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: ProdT A B. Prop \def -\lambda A,B : CSetoid.\lambda c,d: ProdT A B. - ((cs_ap A (fstT A B c) (fstT A B d)) \or - (cs_ap B (sndT A B c) (sndT A B d))). - -definition prod_eq: \forall A,B : CSetoid.\forall c,d: ProdT A B. Prop \def -\lambda A,B : CSetoid.\lambda c,d: ProdT A B. - ((cs_eq A (fstT A B c) (fstT A B d)) \and - (cs_eq B (sndT A B c) (sndT A B d))). - - -lemma prodcsetoid_is_CSetoid: \forall A,B: CSetoid. - is_CSetoid (ProdT 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 t H1) - |apply (ap_irreflexive B t1 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 ((t \neq t4) \or (t4 \neq t2)) - [elim Hcut - [left. left. assumption - |right. left. assumption - ] - |apply (ap_cotransitive A). assumption - ] - |cut ((t1 \neq t5) \or (t5 \neq t3)) - [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 t t2 H2). assumption - |apply (eq_imp_not_ap B t1 t3 H3). assumption - ] - ] -] -qed. - - -definition ProdCSetoid : \forall A,B: CSetoid. CSetoid \def - \lambda A,B: CSetoid. - mk_CSetoid (ProdT 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. (S \to Prop) \to Prop \def - \lambda S: CSetoid. \lambda P: S \to Prop. \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). - -auto. - -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). - -auto. - -intro H3. -elim H3; intro H4. - -auto. -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. - -auto. - -elim H2; intro H3. - -elim (ap_irreflexive _ _ H3). - -auto. -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); auto. -intro H2. -elim (H0 x1 x2 y2 H2); auto. -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). - -auto. - -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). - -auto. - -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. - -auto. - -case (ap_cotransitive_unfolded _ _ _ H0 y2); intro H1. - -auto. - -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/Setoid/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/Setoid/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/Setoid/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. -reduce 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.reduce 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) \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. -reduce in H4. -reduce 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. -reduce in H4. -apply (cs_bin_op_strext ? f ? ? ? ? H4). -qed. - -definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop. - \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f. - CSetoid_bin_op (mk_SubCSetoid S P) \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. -auto new timeout=100. -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/matita/contribs/CoRN/makefile b/matita/contribs/CoRN/makefile deleted file mode 100644 index 1fda4fb90..000000000 --- a/matita/contribs/CoRN/makefile +++ /dev/null @@ -1,37 +0,0 @@ -H=@ - -RT_BASEDIR=../../ -OPTIONS=-bench -MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) -CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) -MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS) -CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) - -devel:=$(shell basename `pwd`) - -ifneq "$(SRC)" "" - XXX="SRC=$(SRC)" -endif - -all: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) -clean: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) -cleanall: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all - -all.opt opt: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) -clean.opt: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) -cleanall.opt: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all - -%.mo: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ -%.mo.opt: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@ - -preall: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) - -- 2.39.2