From: Andrea Asperti Date: Thu, 23 Nov 2006 09:33:24 +0000 (+0000) Subject: Adding CoRN. X-Git-Tag: 0.4.95@7852~797 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4416c87ef01ef870067dce5a77e9471e01c3f51f;p=helm.git Adding CoRN. --- diff --git a/matita/library/algebra/CoRN/SetoidFun.ma b/matita/library/algebra/CoRN/SetoidFun.ma new file mode 100644 index 000000000..cfc2492eb --- /dev/null +++ b/matita/library/algebra/CoRN/SetoidFun.ma @@ -0,0 +1,1224 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + + +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. + apply A. + assumption. + assumption. + auto. + auto +| + apply eq_reflexive_unfolded +] +qed. + +(* +Lemma irrefl_apfun : forall A B : CSetoid, irreflexive (ap_fun A B). +intros A B. +unfold irreflexive in |- *. +intros f. +unfold ap_fun in |- *. +red in |- *. +intro H. +elim H. +intros a H0. +set (H1 := ap_irreflexive_unfolded B (f a)) in *. +intuition. +Qed. +*) + + +(* +lemma cotrans_apfun : \forall A,B : CSetoid. cotransitive (CSetoid_fun A B) (ap_fun A B). +intros (A B). +unfold. +unfold ap_fun. +intros (f g H h). +decompose. +apply ap_cotransitive. +apply (ap_imp_neq B (csf_fun A B x a) (csf_fun A B y a) H1). +(* letin foo \def (\exist a:A.csf_fun A B x a\neq csf_fun A B z a). *) + + +apply (ap_cotransitive B ? ? H1 ?). + +split. +left. +elim H. +clear H. +intros a H. +set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *. +elim H1. +clear H1. +intros H1. +left. +exists a. +exact H1. + +clear H1. +intro H1. +right. +exists a. +exact H1. +Qed. +*) + +(* +Lemma cotrans_apfun : forall A B : CSetoid, cotransitive (ap_fun A B). +intros A B. +unfold cotransitive in |- *. +unfold ap_fun in |- *. +intros f g H h. +elim H. +clear H. +intros a H. +set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *. +elim H1. +clear H1. +intros H1. +left. +exists a. +exact H1. + +clear H1. +intro H1. +right. +exists a. +exact H1. +Qed. +*) + +lemma ta_apfun : \forall A, B : CSetoid. tight_apart (CSetoid_fun A B) (eq_fun A B) (ap_fun A B). +unfold tight_apart. +intros (A B f g). +unfold ap_fun. +unfold eq_fun. +split +[ intros. elim H. unfold in H. +generalize in match H. reduce. simplify .unfold. + + | +] +intros. +red in H. +apply not_ap_imp_eq. +red in |- *. +intros H0. +apply H. +exists a. +exact H0. +intros H. +red in |- *. + +intro H1. +elim H1. +intros a X. +set (H2 := eq_imp_not_ap B (f a) (g a) (H a) X) in *. +exact H2. +Qed. + +(* +Lemma ta_apfun : forall A B : CSetoid, tight_apart (eq_fun A B) (ap_fun A B). +unfold tight_apart in |- *. +unfold ap_fun in |- *. +unfold eq_fun in |- *. +intros A B f g. +split. +intros H a. +red in H. +apply not_ap_imp_eq. +red in |- *. +intros H0. +apply H. +exists a. +exact H0. +intros H. +red in |- *. + +intro H1. +elim H1. +intros a X. +set (H2 := eq_imp_not_ap B (f a) (g a) (H a) X) in *. +exact H2. +Qed. +*) + +Lemma sym_apfun : forall A B : CSetoid, Csymmetric (ap_fun A B). +unfold Csymmetric in |- *. +unfold ap_fun in |- *. +intros A B f g H. +elim H. +clear H. +intros a H. +exists a. +apply ap_symmetric_unfolded. +exact H. +Qed. + +Definition FS_is_CSetoid (A B : CSetoid) := + Build_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 (A B : CSetoid) := + Build_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 (S:CSetoid) (s:S):Prop := True. + +Fixpoint n_ary_operation (n:nat)(V:CSetoid){struct n}:CSetoid:= +match n with +|0 => V +|(S m)=> (FS_as_CSetoid V (n_ary_operation m V)) +end. + +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 : CSetoid_fun S1 S3. +apply (Build_CSetoid_fun _ _ (fun x : S1 => g (f x))). +(* str_ext *) +unfold fun_strext in |- *; intros x y H. +apply (csf_strext _ _ f). apply (csf_strext _ _ g). assumption. +Defined. + +End unary_function_composition. + +(** ***Composition as operation +*) +Definition comp (A B C : CSetoid) : + FS_as_CSetoid A B -> FS_as_CSetoid B C -> FS_as_CSetoid A C. +intros A B C f g. +set (H := compose_CSetoid_fun A B C f g) in *. +exact H. +Defined. + +Definition comp_as_bin_op (A:CSetoid) : CSetoid_bin_op (FS_as_CSetoid A A). +intro A. +unfold CSetoid_bin_op in |- *. +eapply Build_CSetoid_bin_fun with (comp A A A). +unfold bin_fun_strext in |- *. +unfold comp in |- *. +intros f1 f2 g1 g2. +simpl in |- *. +unfold ap_fun in |- *. +unfold compose_CSetoid_fun in |- *. +simpl in |- *. +elim f1. +unfold fun_strext in |- *. +clear f1. +intros f1 Hf1. +elim f2. +unfold fun_strext in |- *. +clear f2. +intros f2 Hf2. +elim g1. +unfold fun_strext in |- *. +clear g1. +intros g1 Hg1. +elim g2. +unfold fun_strext in |- *. +clear g2. +intros g2 Hg2. +simpl in |- *. +intro H. +elim H. +clear H. +intros a H. +set (H0 := ap_cotransitive A (g1 (f1 a)) (g2 (f2 a)) H (g2 (f1 a))) in *. +elim H0. +clear H0. +intro H0. +right. +exists (f1 a). +exact H0. + +clear H0. +intro H0. +left. +exists a. +apply Hg2. +exact H0. +Defined. + +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/library/algebra/CoRN/Setoids.ma b/matita/library/algebra/CoRN/Setoids.ma new file mode 100644 index 000000000..a06c43ab8 --- /dev/null +++ b/matita/library/algebra/CoRN/Setoids.ma @@ -0,0 +1,1249 @@ +(**************************************************************************) +(* ___ *) +(* ||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. + +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). auto. +assumption. +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 : 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 associative : \forall S: CSetoid. (S \to S \to S) \to 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.assumption. +qed. + +lemma id_pres_eq : \forall S:CSetoid. un_op_wd S (\lambda x : S.x). +unfold un_op_wd. +unfold fun_wd. +intros. +simplify.assumption. +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. + +lemma subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop. +is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P). +intros. +apply (mk_is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P)) +[ unfold. intros.unfold. elim x. exact (ap_irreflexive_unfolded S ? ?) + [ assumption | apply H1.] + (* 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. + associative S (csbf_fun S S S f) + \to associative (mk_SubCSetoid S P) (csbf_fun (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid_bin_op S P f pr)). +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. +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'.