X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2FCoRN%2FSetoidFun.ma;h=67f8ac1d6a5763dfab65e15b17128ed1d3f66b85;hb=b348a1a39e17b541fca17d2218a3b91bd7f1fece;hp=cfc2492eba56389541888d2c413bf553ed1a8e51;hpb=109e6f703657938fc534211e394763997b258061;p=helm.git diff --git a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma index cfc2492eb..67f8ac1d6 100644 --- a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma +++ b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/algebra/CoRN/SetoidFun". include "algebra/CoRN/Setoids.ma". - +include "higher_order_defs/relations.ma". definition ap_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def \lambda A,B : CSetoid. \lambda f,g : CSetoid_fun A B. @@ -39,93 +39,29 @@ 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 +[ apply (eq_imp_not_ap A) + [ + assumption|assumption|apply eq_reflexive_unfolded| + apply (csf_strext_unfolded A B f). + exact H1 + ] +|apply eq_reflexive_unfolded ] qed. -(* -Lemma irrefl_apfun : forall A B : CSetoid, irreflexive (ap_fun A B). -intros A B. -unfold irreflexive in |- *. -intros f. -unfold ap_fun in |- *. -red in |- *. -intro H. -elim H. -intros a H0. -set (H1 := ap_irreflexive_unfolded B (f a)) in *. -intuition. -Qed. -*) - - -(* lemma cotrans_apfun : \forall A,B : CSetoid. cotransitive (CSetoid_fun A B) (ap_fun A B). intros (A B). unfold. unfold ap_fun. intros (f g H h). -decompose. -apply ap_cotransitive. -apply (ap_imp_neq B (csf_fun A B x a) (csf_fun A B y a) H1). -(* letin foo \def (\exist a:A.csf_fun A B x a\neq csf_fun A B z a). *) - - -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. +lapply (ap_cotransitive ? ? ? H1 (csf_fun A B h a)). +elim Hletin. left. -exists a. -exact H1. - -clear H1. -intro H1. +apply (ex_intro ? ? a H2). 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. -*) +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. @@ -133,537 +69,544 @@ 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. 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. ] -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. -*) +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. +lemma sym_apfun : \forall A, B : CSetoid. symmetric ? (ap_fun A B). +unfold symmetric. +unfold ap_fun. +intros 5 (A B f g H). +elim H 0. clear H. -intros a H. -exists a. +intros 2 (a H). +apply (ex_intro ? ? a). apply ap_symmetric_unfolded. exact H. -Qed. +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_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 (A B : CSetoid) := - Build_CSetoid (CSetoid_fun A B) (eq_fun A B) (ap_fun 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 -*) +(* Nullary and n-ary operations *) -Definition is_nullary_operation (S:CSetoid) (s:S):Prop := True. +definition is_nullary_operation : \forall S:CSetoid. \forall s:S. Prop \def +\lambda S:CSetoid. \lambda s:S. True. -Fixpoint n_ary_operation (n:nat)(V:CSetoid){struct n}:CSetoid:= +let rec n_ary_operation (n:nat) (V:CSetoid) on n : CSetoid \def match n with -|0 => V -|(S m)=> (FS_as_CSetoid V (n_ary_operation m V)) -end. +[ O \Rightarrow V +|(S m) \Rightarrow (FS_as_CSetoid V (n_ary_operation m V))]. + -Section unary_function_composition. +(* Section unary_function_composition. *) -(** ** Composition of Setoid functions +(* 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. +(* Variables S1 S2 S3 : CSetoid. Variable f : CSetoid_fun S1 S2. -Variable g : CSetoid_fun S2 S3. +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. +definition compose_CSetoid_fun : \forall S1,S2,S3 :CSetoid. \forall f: (CSetoid_fun S1 S2). \forall g: (CSetoid_fun S2 S3). +CSetoid_fun S1 S3. +intros (S1 S2 S3 f g). +apply (mk_CSetoid_fun ? ? (\lambda x :cs_crr S1. csf_fun S2 S3 g (csf_fun S1 S2 f x))). +unfold fun_strext. +intros (x y H). +apply (csf_strext ? ? f). +apply (csf_strext ? ? g). +assumption. +qed. -(** ***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 *. +(* 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. -Defined. +qed. -Definition comp_as_bin_op (A:CSetoid) : CSetoid_bin_op (FS_as_CSetoid A A). +definition comp_as_bin_op : \forall 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 |- *. +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 f1 Hf1. -elim f2. -unfold fun_strext in |- *. +intros 2 (f1 Hf1). +elim f2 0. +unfold fun_strext. clear f2. -intros f2 Hf2. -elim g1. -unfold fun_strext in |- *. +intros 2 (f2 Hf2). +elim g1 0. +unfold fun_strext. clear g1. -intros g1 Hg1. -elim g2. -unfold fun_strext in |- *. +intros 2 (g1 Hg1). +elim g2 0. +unfold fun_strext. clear g2. -intros g2 Hg2. -simpl in |- *. +intros 2 (g2 Hg2). +simplify. intro H. -elim H. +elim H 0. clear H. -intros a H. -set (H0 := ap_cotransitive A (g1 (f1 a)) (g2 (f2 a)) H (g2 (f1 a))) in *. -elim H0. +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 (f1 a). +exists. +apply (f1 a). exact H0. clear H0. intro H0. left. -exists a. +exists. +apply 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. +qed. + + +(* Questa coercion composta non e' stata generata autobatchmaticamente *) +lemma mycor: ∀S. CSetoid_bin_op S → (S → S → S). + intros; + unfold in c; + apply (c c1 c2). +qed. +coercion cic:/matita/algebra/CoRN/SetoidFun/mycor.con 2. + +(* Mettendola a mano con una beta-espansione funzionerebbe *) +(*lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (\lambda e.mycor ? (comp_as_bin_op A) e)).*) +(* Questo sarebbe anche meglio: senza beta-espansione *) +(*lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (mycor ? (comp_as_bin_op A))).*) +(* QUESTO E' QUELLO ORIGINALE MA NON FUNZIONANTE *) +(* lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (comp_as_bin_op A)). *) +lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (mycor ? (comp_as_bin_op A))). +unfold CSassociative. +unfold comp_as_bin_op. +intros 4 (A f g h). +simplify. +elim f. +elim g. +elim h. +whd.intros. +simplify. +apply eq_reflexive_unfolded. +qed. + +definition compose_CSetoid_bin_un_fun: \forall A,B,C : CSetoid. +\forall f : CSetoid_bin_fun B B C. \forall g : CSetoid_fun A B. +CSetoid_bin_fun A A C. +intros 5 (A B C f g). +apply (mk_CSetoid_bin_fun A A C (\lambda a0,a1 : cs_crr A. f (csf_fun ? ? g a0) (csf_fun ? ? g a1))). +unfold. +intros 5 (x1 x2 y1 y2 H0). +letin H10 \def (csbf_strext B B C f). +unfold in H10. +letin H40 \def (csf_strext A B g). +unfold in H40. +elim (H10 (csf_fun ? ? g x1) (csf_fun ? ? g x2) (csf_fun ? ? g y1) (csf_fun ? ? g y2) H0); +[left | right]; autobatch. +qed. -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. +definition compose_CSetoid_bin_fun: \forall A, B, C : CSetoid. +\forall f,g : CSetoid_fun A B.\forall h : CSetoid_bin_fun B B C. +CSetoid_fun A C. +intros (A B C f g h). +apply (mk_CSetoid_fun A C (λa : cs_crr A. csbf_fun ? ? ? h (csf_fun ? ? f a) (csf_fun ? ? g a))). +unfold. +intros (x y H). +elim (csbf_strext ? ? ? ? ? ? ? ? H)[ + apply (csf_strext A B f).exact H1 + |apply (csf_strext A B g).exact H1] +qed. + +definition compose_CSetoid_un_bin_fun: \forall A,B,C :CSetoid. \forall f : CSetoid_bin_fun B B C. + ∀ g : CSetoid_fun C A. CSetoid_bin_fun B B A. +intros (A0 B0 C f g). +apply (mk_CSetoid_bin_fun ? ? ? (\lambda x,y : B0. csf_fun ? ? g (f x y))). +unfold. +intros 4 (x1 x2 y1 y2). +elim f 0. +unfold bin_fun_strext. +elim g 0. +unfold fun_strext. +intros 5 (gu gstrext fu fstrext H). apply fstrext. apply gstrext. exact H. -Defined. +qed. -End unary_and_binary_function_composition. +(* End unary_and_binary_function_composition.*) -(** ***Projections -*) +(*Projections*) -Section function_projection. +(*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. +lemma proj_bin_fun : \forall A, B, C: CSetoid. +\forall f : CSetoid_bin_fun A B C. \forall a: ?. +fun_strext ? ? (f a). +intros (A B C f a). +unfold. +elim f 0. intro fo. -simpl. -intros csbf_strext0 x y H. -elim (csbf_strext0 _ _ _ _ H); intro H0. - elim (ap_irreflexive_unfolded _ _ H0). +simplify. +intros 4 (csbf_strext0 x y H). +elim (csbf_strext0 ? ? ? ? H) 0; intro H0. + elim (ap_irreflexive_unfolded ? ? H0). exact H0. -Qed. +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. +definition projected_bin_fun: \forall A,B,C : CSetoid. \forall f : CSetoid_bin_fun A B C. +\forall a : A. ? \def +\lambda A,B,C : CSetoid. \lambda f : CSetoid_bin_fun A B C. +\lambda a : A. + mk_CSetoid_fun B C (f a) (proj_bin_fun A B C f a). -Section BinProj. +(* End function_projection. *) -Variable S : CSetoid. +(* Section BinProj. *) -Definition binproj1 (x y:S) := x. +(* Variable S : CSetoid. *) -Lemma binproj1_strext : bin_fun_strext _ _ _ binproj1. -red in |- *; auto. -Qed. +definition binproj1 : \forall S: CSetoid. \forall x,y:S. ? \def +\lambda S:CSetoid. \lambda x,y:S. + x. + +lemma binproj1_strext :\forall S:CSetoid. bin_fun_strext ? ? ? (binproj1 S). +intro.unfold; +intros 4.unfold binproj1.intros.left.exact H. +qed. -Definition cs_binproj1 : CSetoid_bin_op S. -red in |- *; apply Build_CSetoid_bin_op with binproj1. +definition cs_binproj1 :\forall S:CSetoid. CSetoid_bin_op S. +intro. +unfold. +apply (mk_CSetoid_bin_op ? (binproj1 S)). apply binproj1_strext. -Defined. +qed. -End BinProj. +(* End BinProj. *) -(** **Combining operations +(*Combining operations %\begin{convention}% Let [S1], [S2] and [S3] be setoids. %\end{convention}% *) -Section CombiningOperations. -Variables S1 S2 S3 : CSetoid. +(* 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. +(* Section CombiningUnaryOperations. +Variable f : CSetoid_fun S1 S2. +Variable op : CSetoid_un_op S2. *) + +definition opOnFun : \forall S1,S2,S3 :CSetoid. \forall f : CSetoid_fun S1 S2. + \forall op : CSetoid_un_op S2. + CSetoid_fun S1 S2. +intros (S1 S2 S3 f op). +apply (mk_CSetoid_fun S1 S2 (\lambda x : cs_crr S1. csf_fun ? ? op (csf_fun ? ? f x))). +unfold fun_strext; intros (x y H). +apply (csf_strext ? ? f x y). +apply (csf_strext ? ? op ? ? H). +qed. +(* End CombiningUnaryOperations. End CombiningOperations. Section p66E2b4. - -(** **The Free Setoid +*) +(* The Free Setoid %\begin{convention}% Let [A:CSetoid]. %\end{convention}% *) -Variable A:CSetoid. -Definition Astar := (list A). +(* Variable A:CSetoid. *) -Definition empty_word := (nil A). +(* TODO from listtype.ma!!!!!!!! *) +inductive Tlist (A : Type) : Type \def + Tnil : Tlist A + | Tcons : A \to Tlist A \to Tlist A. -Definition appA:= (app A). +definition Astar: \forall A: CSetoid. ? \def +\lambda A:CSetoid. + Tlist 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. +definition empty_word : \forall A: Type. ? \def +\lambda A:Type. (Tnil A). -intuition. -Qed. +(* from listtype.ma!!!!!!!! *) +let rec Tapp (A:Type) (l,m: Tlist A) on l \def + match l with + [ Tnil \Rightarrow m + | (Tcons a l1) \Rightarrow (Tcons A a (Tapp A l1 m))]. +definition appA : \forall A: CSetoid. ? \def +\lambda A:CSetoid. + (Tapp A). -Lemma ap_fm_symmetric: Csymmetric ap_fm. -unfold Csymmetric. -intros x. -induction x. -intro y. -case y. -simpl. -intuition. +let rec eq_fm (A:CSetoid) (m:Astar A) (k:Astar A) on m : Prop \def +match m with +[ Tnil ⇒ match k with + [ Tnil ⇒ True + | (Tcons a l) ⇒ False] +| (Tcons b n) ⇒ match k with + [Tnil ⇒ False + |(Tcons a l) ⇒ b=a ∧ (eq_fm A n l)] +]. + +let rec CSap_fm (A:CSetoid)(m:Astar A)(k:Astar A) on m: Prop \def +match m with +[Tnil ⇒ match k with + [Tnil ⇒ False + |(Tcons a l) ⇒ True] +|(Tcons b n) ⇒ match k with + [Tnil ⇒ True + |(Tcons a l) ⇒ b ≠ a ∨ (CSap_fm A n l)] +]. + +lemma ap_fm_irreflexive: \forall A:CSetoid. (irreflexive (Astar A) (CSap_fm A) ). +unfold irreflexive. +intros 2 (A x). +elim x[ +simplify. +unfold. +intro Hy. +exact Hy| +simplify. +unfold. +intro H1. +apply H. +elim H1[ +clear H1. +generalize in match (ap_irreflexive A). +unfold irreflexive. +unfold Not. +intro. +unfold in H. +apply False_ind. +apply H1.apply t. +exact H2|exact H2] +] +qed. -simpl. -intuition. -simpl. +lemma ap_fm_symmetric: \forall A:CSetoid. (symmetric (Astar A) (CSap_fm A)). +intro A. +unfold symmetric. +intro x. +elim x 0 [ 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. + elim y 0[ + simplify. + intro. + exact H| + simplify. + intros. + exact H1]| + intros 4 (t t1 H y). + elim y 0[ + simplify. + intro. + exact H1| + simplify. + intros. + elim H2 0 [ + generalize in match (ap_symmetric A). + unfold symmetric. + intros. + left. + apply ap_symmetric.exact H4| + intro. + right. + apply H. + exact H3] + ] + ] +qed. -Lemma ap_fm_cotransitive : (cotransitive ap_fm). +lemma ap_fm_cotransitive : \forall A:CSetoid. (cotransitive (Astar A) (CSap_fm A)). +intro A. unfold cotransitive. intro x. -induction x. -simpl. -intro y. -case y. -intuition. - -intros c l H z. -case z. -simpl. -intuition. - -intuition. - -simpl. +elim x 0 [ 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. - +elim y 0 [ +intro.simplify in H.intro.elim z.simplify.left. exact H|intros (c l H1 H z). +elim z 0[ +simplify. +right. apply I|intros (a at).simplify. left. apply I]] +simplify. +left. +autobatch new|intros 2 (c l). +intros 2 (Hy). +elim y 0[ +intros 2 (H z). +elim z 0 [simplify. left.apply I| +intros 2 ( a at). +intro H1. +simplify. +right. apply I]| +intros (a at bo H z). +elim z 0[ +simplify.left. +apply I| +intros 2 (c0 l0). +elim H 0 [ clear H. -intro H. -generalize (IHx l H l0). -intuition. -Qed. +intro.intro Hn.simplify. +generalize in match (ap_cotransitive A c a H c0). +intros.elim H1 0[intros.left. left.exact H2| +intro.right.left.exact H2]|intros. +simplify. +generalize in match (Hy at H1 l0). +intros. +elim H3[ +left.right.exact H4| +right.right.exact H4]]]]] +qed. -Lemma ap_fm_tight : (tight_apart eq_fm ap_fm). +lemma ap_fm_tight : \forall A:CSetoid. (tight_apart (Astar A) (eq_fm A) (CSap_fm A)). +intro A. unfold tight_apart. -intros x. -induction x. -simpl. -intro y. -case y. -red. +intro x. unfold Not. -intuition. - -intuition. - -intro y. -simpl. -case y. -intuition. - -intros c l. -generalize (IHx l). -red. +elim x 0[ + intro y. + elim y 0[ + split[simplify.intro.autobatch new|simplify.intros.exact H1]| +intros (a at). +simplify. +split[intro.autobatch new|intros. exact H1] +] +| +intros (a at IHx). +elim y 0[simplify. + split[intro.autobatch new|intros.exact H] + | +intros 2 (c l). +generalize in match (IHx l). intro H0. -elim H0. -intros H1 H2. +elim H0. split. intro H3. split. -red in H3. -generalize (ap_tight A a c). -intuition. - -apply H1. -intro H4. -apply H3. -right. -exact H4. - +generalize in match (ap_tight A a c). +intros. +elim H4. +clear H4.apply H5. +unfold.intro.simplify in H3. +apply H3.left.exact H4. +intros.elim H2. +apply H.intro.apply H3.simplify. right. exact H6. intro H3. -elim H3. +elim H3 0. clear H3. -intros H3 H4. -intro H5. +intros. elim H5. -generalize (ap_tight A a c). -intuition. - -apply H2. -exact H4. -Qed. +generalize in match (ap_tight A a c). +intro. +elim H7.clear H7. +unfold Not in H9.simplify in H5. +apply H9. +exact H3.exact H6. +apply H1. +exact H4.exact H6.]] +qed. -Definition free_csetoid_is_CSetoid:(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_is_CSetoid: \forall A:CSetoid. + (is_CSetoid (Astar A) (eq_fm A) (CSap_fm A)) \def + \lambda A:CSetoid. + (mk_is_CSetoid (Astar A) (eq_fm A) (CSap_fm A) (ap_fm_irreflexive A) (ap_fm_symmetric A) + (ap_fm_cotransitive A) (ap_fm_tight A )). -Definition free_csetoid_as_csetoid:CSetoid:= -(Build_CSetoid Astar eq_fm ap_fm free_csetoid_is_CSetoid). +definition free_csetoid_as_csetoid: \forall A:CSetoid. CSetoid \def +\lambda A:CSetoid. +(mk_CSetoid (Astar A) (eq_fm A) (CSap_fm A) (free_csetoid_is_CSetoid A)). -Lemma app_strext: - (bin_fun_strext free_csetoid_as_csetoid free_csetoid_as_csetoid - free_csetoid_as_csetoid appA). +lemma app_strext: \forall A:CSetoid. + (bin_fun_strext (free_csetoid_as_csetoid A) (free_csetoid_as_csetoid A) + (free_csetoid_as_csetoid A) (appA A)). +intro A. unfold bin_fun_strext. -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. +intro x1. +elim x1 0[simplify.intro x2. + elim x2 0[simplify.intros.right.exact H|simplify.intros.left.left] + |intros 6 (a at IHx1 x2 y1 y2). + simplify. + elim x2 0 [ + elim y2 0 [simplify.intros.left.exact H|intros.left.left] + |elim y2 0[simplify.simplify in IHx1. + intros (c l H). + elim H1 0 [intros.left.left.exact H2| clear H1. + generalize in match (IHx1 l y1 (Tnil A)). + simplify.intros.elim H1 0 [intros.left.right.exact H3| + intros.right.exact H3|exact H2] + ] + |simplify. + intros (c l H c0 l0). + elim H2 0 [intros.left.left.exact H3| + generalize in match (IHx1 l0 y1 (Tcons A c l)).intros. + elim H3 0 [intros.left.right.exact H5|intros.right.exact H5|exact H4] + ] + ] + ] +] +qed. -End p66E2b4. +definition app_as_csb_fun: \forall A:CSetoid. +(CSetoid_bin_fun (free_csetoid_as_csetoid A) (free_csetoid_as_csetoid A) + (free_csetoid_as_csetoid A)) \def + \lambda A:CSetoid. + (mk_CSetoid_bin_fun (free_csetoid_as_csetoid A) (free_csetoid_as_csetoid A) + (free_csetoid_as_csetoid A) (appA A) (app_strext A)). + +(* TODO : Can't qed +lemma eq_fm_reflexive: \forall A:CSetoid. \forall (x:Astar A). (eq_fm A x x). +intros (A x). +elim x. +simplify.left. +simplify. left. apply eq_reflexive_unfolded.assumption. +qed. +*) +(* End p66E2b4. *) -(** **Partial Functions +(* Partial Functions In this section we define a concept of partial function for an arbitrary setoid. Essentially, a partial function is what would be @@ -685,9 +628,9 @@ 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. +(* Section SubSets_of_G. *) -(** ***Subsets of Setoids +(* 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 @@ -702,161 +645,261 @@ welldefinedness. %\end{convention}% *) -Variable S : CSetoid. +(* 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. +(* From CLogic.v *) +inductive CAnd (A,B : Type): Type \def +|CAnd_intro : A \to B \to CAnd A B. -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. +definition conjP : \forall S:CSetoid. \forall P,Q: S \to Type. \forall x : S. Type +\def +\lambda S:CSetoid. \lambda P,Q: S \to Type. \lambda x : S. + CAnd (P x) (Q x). -apply H with x; assumption. +lemma prj1 : \forall S:CSetoid. \forall P,Q : S \to Type. \forall x : S. + (conjP S P Q x) \to (P x). +intros;elim c.assumption. +qed. -apply H0 with x; assumption. -Qed. +lemma prj2 : \forall S:CSetoid. \forall P,Q : S \to Type. \forall x : S. + conjP S P Q x \to Q x. +intros. elim c. assumption. +qed. -End Conjunction. +lemma conj_wd : \forall S:CSetoid. \forall P,Q : S \to Type. + pred_wd ? P \to pred_wd ? Q \to pred_wd ? (conjP S P Q). + intros 3. + unfold pred_wd. + unfold conjP. + intros.elim c. + split [ apply (f x ? t).assumption|apply (f1 x ? t1). assumption] +qed. -Section Disjunction. +(* End Conjunction. *) -Variables P Q : S -> CProp. +(* 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. +definition disj : \forall S:CSetoid. \forall P,Q : S \to Prop. \forall x : S. + Prop \def + \lambda S:CSetoid. \lambda P,Q : S \to Prop. \lambda x : S. + P x \lor Q x. + +lemma inj1 : \forall S:CSetoid. \forall P,Q : S \to Prop. \forall x : S. + P x \to (disj S P Q x). +intros. +left. +assumption. +qed. -right; apply H0 with x; assumption. -Qed. +lemma inj2 : \forall S:CSetoid. \forall P,Q : S \to Prop. \forall x : S. + Q x \to disj S P Q x. +intros. +right. +assumption. +qed. -End Disjunction. +lemma disj_wd : \forall S:CSetoid. \forall P,Q : S \to Prop. + pred_wd ? P \to pred_wd ? Q \to pred_wd ? (disj S P Q). +intros 3. +unfold pred_wd. +unfold disj. +intros. +elim H2 [left; apply (H x ); assumption| + right; apply (H1 x). assumption. exact H3] +qed. +(* End Disjunction. *) -Section Extension. +(* 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). +definition extend : \forall S:CSetoid. \forall P: S \to Type. + \forall R : (\forall x:S. P x \to Type). \forall x : S. ? + \def + \lambda S:CSetoid. \lambda P: S \to Type. + \lambda R : (\forall x:S. P x \to Type). \lambda x : S. + CAnd (P x) (\forall H : P x. (R x H) ). + +lemma ext1 : \forall S:CSetoid. \forall P: S \to Prop. + \forall R : (\forall x:S. P x \to Prop). \forall x : S. + extend S P R x \to P x. +intros. +elim e. +assumption. +qed. -Lemma ext1 : forall x : S, extend x -> P x. -intros x H; inversion_clear H; assumption. -Qed. +inductive sigT (A:Type) (P:A -> Type) : Type \def + |existT : \forall x:A. P x \to sigT A P. -Lemma ext2_a : forall x : S, extend x -> {H : P x | R x H}. -intros x H; inversion_clear H. -exists X; auto. -Qed. +lemma ext2_a : \forall S:CSetoid. \forall P: S \to Prop. + \forall R : (\forall x:S. P x \to Prop). \forall x : S. + extend S P R x \to (sigT ? (λH : P x. R x H)). +intros. +elim e. +apply (existT).assumption. +apply (t1 t). +qed. + +(* +lemma ext2_a : \forall S:CSetoid. \forall P: S \to Prop. + \forall R : (\forall x:S. P x \to Prop). \forall x : S. + extend S P R x \to (ex ? (λH : P x. R x H)). +intros. +elim H. +apply (ex_intro). +exact H1.apply H2. +qed. +*) +definition proj1_sigT: \forall A : Type. \forall P : A \to Type. + \forall e : sigT A P. ? \def + \lambda A : Type. \lambda P : A \to Type. + \lambda e : sigT A P. + match e with + [existT a b \Rightarrow a]. + +(* original def in CLogic.v +Definition proj1_sigT (A : Type) (P : A -> CProp) (e : sigT P) := + match e with + | existT a b => a + end. +*) +(* _ *) +definition proj2_sigTm : \forall A : Type. \forall P : A \to Type. + \forall e : sigT A P. ? \def + \lambda A : Type. \lambda P : A \to Type. + \lambda e : sigT A P. + match e return \lambda s:sigT A P. P (proj1_sigT A P s) with + [ existT a b \Rightarrow b]. + +definition projT1: \forall A: Type. \forall P: A \to Type.\forall H: sigT A P. A \def + \lambda A: Type. \lambda P: A \to Type.\lambda H: sigT A P. + match H with + [existT x b \Rightarrow x]. + +definition projT2m : \forall A: Type. \forall P: A \to Type. \forall x:sigT A P. + P (projT1 A P x) \def + \lambda A: Type. \lambda P: A \to Type. + (\lambda H:sigT A P.match H return \lambda s:sigT A P. P (projT1 A P s) with + [existT (x:A) (h:(P x))\Rightarrow h]). + +lemma ext2 : \forall S:CSetoid. \forall P: S \to Prop. +\forall R : (\forall x:S. P x \to Prop). +\forall x: S. + \forall Hx:extend S P R x. + R x (proj1_sigT ? ? (ext2_a S P R x Hx)). + intros. + elim ext2_a. + apply (projT2m (P x) (\lambda Hbeta:P x.R x a)). + apply (existT (P x) ).assumption.assumption. +qed. +(* Lemma ext2 : forall (x : S) (Hx : extend x), R x (ProjT1 (ext2_a x Hx)). intros; apply projT2. -Qed. - -Lemma extension_wd : 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. +lemma extension_wd :\forall S:CSetoid. \forall P: S \to Prop. + \forall R : (\forall x:S. P x \to Prop). + pred_wd ? P \to + (\forall (x,y : S).\forall Hx : (P x). + \forall Hy : (P y). x = y \to R x Hx \to R y Hy) \to + pred_wd ? (extend S P R) . +intros (S P R H H0). +unfold. +intros (x y H1 H2). +elim H1;split[apply (H x).assumption. exact H2| + intro H5.apply (H0 x ? t)[apply H2|apply t1] + ] +qed. -End SubSets_of_G. +(*End Extension. *) -Notation Conj := (conjP _). +(*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 +*) +(**Operations We are now ready to define the concept of partial function between arbitrary setoids. *) +lemma block : \forall y:nat. \forall x:nat. y = x \to x = y. +intros. +symmetry.exact H. +qed. -Record BinPartFunct (S1 S2 : CSetoid) : Type := - {bpfdom : S1 -> CProp; +record BinPartFunct (S1, S2 : CSetoid) : Type \def + {bpfdom : S1 \to Type; 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}. + bpfpfun :> \forall x : S1. (bpfdom x) \to S2; + bpfstrx : \forall x,y,Hx,Hy. + bpfpfun x Hx ≠ bpfpfun y Hy \to (x \neq y)}. +(* Notation BDom := (bpfdom _ _). +Implicit Arguments bpfpfun [S1 S2]. *) -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. +lemma bpfwdef: \forall S1,S2 : CSetoid. \forall F : (BinPartFunct S1 S2). + \forall x,y,Hx,Hy. + x = y \to (bpfpfun S1 S2 F x Hx ) = (bpfpfun S1 S2 F y Hy). intros. -apply not_ap_imp_eq; intro H0. -generalize (bpfstrx _ _ _ _ _ _ _ H0). -exact (eq_imp_not_ap _ _ _ H). -Qed. +apply not_ap_imp_eq;unfold. intro H0. +generalize in match (bpfstrx ? ? ? ? ? ? ? H0). +exact (eq_imp_not_ap ? ? ? H). +qed. -(** Similar for automorphisms. *) +(* Similar for autobatchmorphisms. *) -Record PartFunct (S : CSetoid) : Type := - {pfdom : S -> CProp; +record PartFunct (S : CSetoid) : Type \def + {pfdom : S -> Type; 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}. + pfpfun :> \forall x : S. pfdom x \to S; + pfstrx : \forall x, y, Hx, Hy. pfpfun x Hx \neq pfpfun y Hy \to x \neq y}. + -Notation Dom := (pfdom _). +(* Notation Dom := (pfdom _). Notation Part := (pfpfun _). -Implicit Arguments pfpfun [S]. +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. +lemma pfwdef : \forall S:CSetoid. \forall F : PartFunct S. \forall x, y, Hx, Hy. + x = y \to (pfpfun S F x Hx ) = (pfpfun S F y Hy). intros. -apply not_ap_imp_eq; intro H0. -generalize (pfstrx _ _ _ _ _ _ H0). -exact (eq_imp_not_ap _ _ _ H). -Qed. +apply not_ap_imp_eq;unfold. intro H0. +generalize in match (pfstrx ? ? ? ? ? ? H0). +exact (eq_imp_not_ap ? ? ? H). +qed. -(** +(* A few characteristics of this definition should be explained: - The domain of the partial function is characterized by a predicate that is required to be well defined but not strongly extensional. The @@ -900,129 +943,194 @@ why we chose to altogether do away with this approach. We now present some methods for defining partial functions. *) -Hint Resolve CI: core. +(* Hint Resolve CI: core. *) -Section CSetoid_Ops. +(* Section CSetoid_Ops.*) -Variable S : CSetoid. +(*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. +definition total_eq_part :\forall S:CSetoid. CSetoid_un_op S \to PartFunct S. +intros (S f). +apply (mk_PartFunct ? + (\lambda x : S. True) + ? + (\lambda (x : S). \lambda (H : True).(csf_fun ? ? f x))). +unfold. intros;left. +intros (x y Hx Hy H). +exact (csf_strext_unfolded ? ? f ? ? H). +qed. +(*Section Part_Function_Const.*) -(** +(* In any setoid we can also define constant functions (one for each element of the setoid) and an identity function: %\begin{convention}% Let [c:S]. %\end{convention}% *) -Variable c : S. +(*Variable c : S.*) -Definition Fconst := total_eq_part (Const_CSetoid_fun _ _ c). +definition Fconst: \forall S:CSetoid. \forall c: S. ? \def + \lambda S:CSetoid. \lambda c: S. + total_eq_part ? (Const_CSetoid_fun ? ? c). -End Part_Function_Const. +(* End Part_Function_Const. *) -Section Part_Function_Id. +(* Section Part_Function_Id. *) -Definition Fid := total_eq_part (id_un_op S). +definition Fid : \forall S:CSetoid. ? \def + \lambda S:CSetoid.total_eq_part ? (id_un_op S). + +(* End Part_Function_Id. *) -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.) -(** -(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]#. -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. +#%\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. +%\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. +(* Section Part_Function_Composition. *) -Variables G F : PartFunct S. +(* 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. +definition UP : \forall S:CSetoid. \forall F: PartFunct S. ? \def + \lambda S:CSetoid. \lambda F: PartFunct S. + pfdom ? F. +(* Let P := Dom F. *) +definition UQ : \forall S:CSetoid. \forall G : PartFunct S. ? \def + \lambda S:CSetoid. \lambda G: PartFunct S. + pfdom ? G. +(* Let Q := Dom G. *) +definition UR : \forall S:CSetoid. \forall F,G: PartFunct S. \forall x: S. ? \def + \lambda S:CSetoid. \lambda F,G: PartFunct S. \lambda x: S. + (sigT ? (\lambda Hx : UP S F x. UQ S G (pfpfun S F x Hx))). +(*Let R x := {Hx : P x | Q (F x Hx)}.*) + +(* end hide *) -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). +(* TODO ProjT1 *) +lemma part_function_comp_strext : \forall S:CSetoid. \forall F,G: PartFunct S. +\forall x,y:S. \forall Hx : UR S F G x. \forall Hy : (UR S F G y). + (pfpfun ? G (pfpfun ? F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx)) + \neq (pfpfun ? G (pfpfun ? F y (proj1_sigT ? ? Hy)) (proj2_sigTm ? ? Hy)) \to x \neq y. +intros (S F G x y Hx Hy H). +exact (pfstrx ? ? ? ? ? ? (pfstrx ? ? ? ? ? ? H)). +qed. +(* +definition TempR : \forall S:CSetoid. \forall F,G: PartFunct S. \forall x: S. ? \def + \lambda S:CSetoid. \lambda F,G: PartFunct S. \lambda x: S. + (ex ? (\lambda Hx : UP S F x. UQ S G (pfpfun S F x Hx))). *) + +lemma part_function_comp_dom_wd :\forall S:CSetoid. \forall F,G: PartFunct S. + pred_wd S (UR S F G). + intros.unfold. + intros (x y H H0). + unfold UR. + elim H. + unfold in a. + unfold UP.unfold UQ. + apply (existT). + apply (dom_wd S F x y a H0). +apply (dom_wd S G (pfpfun S F x a)). assumption. apply pfwdef; assumption. -Qed. +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. +definition Fcomp : \forall S:CSetoid. \forall F,G : PartFunct S. ? \def +\lambda S:CSetoid. \lambda F,G : PartFunct S. +mk_PartFunct ? (UR S F G) (part_function_comp_dom_wd S F G) +(\lambda x. \lambda Hx : UR S F G x. (pfpfun S G (pfpfun S F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx))) +(part_function_comp_strext S F G). -End Part_Function_Composition. +(*End Part_Function_Composition.*) -End CSetoid_Ops. +(*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. +(* Section BinPart_Function_Composition.*) -Variables S1 S2 S3 : CSetoid. +(*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. +(* 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). +(*Let R x := {Hx : P x | Q (F x Hx)}.*) + +definition BP : \forall S1,S2:CSetoid. \forall F: BinPartFunct S1 S2. ? \def + \lambda S1,S2:CSetoid. \lambda F: BinPartFunct S1 S2. + bpfdom ? ? F. +(* Let P := Dom F. *) +definition BQ : \forall S2,S3:CSetoid. \forall G: BinPartFunct S2 S3. ? \def + \lambda S2,S3:CSetoid. \lambda G: BinPartFunct S2 S3. + bpfdom ? ? G. +(* Let Q := BDom G.*) +definition BR : \forall S1,S2,S3:CSetoid. \forall F: BinPartFunct S1 S2. +\forall G: BinPartFunct S2 S3. + \forall x: ?. ? \def + \lambda S1,S2,S3:CSetoid. \lambda F: BinPartFunct S1 S2. + \lambda G: BinPartFunct S2 S3. \lambda x: ?. + (sigT ? (\lambda Hx : BP S1 S2 F x. BQ S2 S3 G (bpfpfun S1 S2 F x Hx))). +(*Let R x := {Hx : P x | Q (F x Hx)}.*) + +lemma bin_part_function_comp_strext : \forall S1,S2,S3:CSetoid. \forall F: BinPartFunct S1 S2. +\forall G: BinPartFunct S2 S3. \forall x,y. \forall Hx : BR S1 S2 S3 F G x. +\forall Hy : (BR S1 S2 S3 F G y). +(bpfpfun ? ? G (bpfpfun ? ? F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx)) \neq +(bpfpfun ? ? G (bpfpfun ? ? F y (proj1_sigT ? ? Hy)) (proj2_sigTm ? ? Hy)) \to x \neq y. +intros (S1 S2 S3 x y Hx Hy H). +exact (bpfstrx ? ? ? ? ? ? ? (bpfstrx ? ? ? ? ? ? ? H1)). +qed. + +lemma bin_part_function_comp_dom_wd : \forall S1,S2,S3:CSetoid. + \forall F: BinPartFunct S1 S2. \forall G: BinPartFunct S2 S3. + pred_wd ? (BR S1 S2 S3 F G). +intros. +unfold.intros (x y H H0). +unfold BR; elim H 0.intros (x0). +apply (existT ? ? (bdom_wd ? ? F x y x0 H0)). +apply (bdom_wd ? ? G (bpfpfun ? ? F x x0)). assumption. apply bpfwdef; assumption. -Qed. - -Definition BinFcomp := 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. +qed. +definition BinFcomp : \forall S1,S2,S3:CSetoid. \forall F: BinPartFunct S1 S2. + \forall G: BinPartFunct S2 S3. ? +\def +\lambda S1,S2,S3:CSetoid. \lambda F: BinPartFunct S1 S2. \lambda G: BinPartFunct S2 S3. +mk_BinPartFunct ? ? (BR S1 S2 S3 F G) (bin_part_function_comp_dom_wd S1 S2 S3 F G) + (\lambda x. \lambda Hx : BR S1 S2 S3 F G x.(bpfpfun ? ? G (bpfpfun ? ? F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx))) + (bin_part_function_comp_strext S1 S2 S3 F G). +(*End BinPart_Function_Composition.*) (* Different tokens for compatibility with coqdoc *) +(* Implicit Arguments Fconst [S]. Notation "[-C-] x" := (Fconst x) (at level 2, right associativity). @@ -1032,185 +1140,155 @@ Implicit Arguments Fcomp [S]. Infix "[o]" := Fcomp (at level 65, no associativity). Hint Resolve pfwdef bpfwdef: algebra. +*) +(*Section bijections.*) +(*Bijections *) -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 |- *. +definition injective : \forall A, B :CSetoid. \forall f : CSetoid_fun A B. + ? \def + \lambda A, B :CSetoid. \lambda f : CSetoid_fun A B. + (\forall a0: A.\forall a1 : A. a0 \neq a1 \to + (csf_fun A B f a0) \neq (csf_fun A B f a1)). + +definition injective_weak: \forall A, B :CSetoid. \forall f : CSetoid_fun A B. + ? \def + \lambda A, B :CSetoid. \lambda f : CSetoid_fun A B. + (\forall a0, a1 : A. + (csf_fun ? ? f a0) = (csf_fun ? ? f a1) -> a0 = a1). + +definition surjective : \forall A, B :CSetoid. \forall f : CSetoid_fun A B. + ? \def + \lambda A, B :CSetoid. \lambda f : CSetoid_fun A B. + (\forall b : B. (\exists a : A. (csf_fun ? ? f a) = b)). + +(* Implicit Arguments injective [A B]. + Implicit Arguments injective_weak [A B]. + Implicit Arguments surjective [A B]. *) + +lemma injective_imp_injective_weak: \forall A, B :CSetoid. \forall f : CSetoid_fun A B. + injective A B f \to injective_weak A B f. +intros 3 (A B f). +unfold injective. intro H. -unfold injective_weak in |- *. -intros a0 a1 H0. +unfold injective_weak. +intros 3 (a0 a1 H0). apply not_ap_imp_eq. -red in |- *. +unfold. 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 *. +letin H2 \def (H a0 a1 H1). +letin H3 \def (ap_imp_neq B (csf_fun ? ? f a0) (csf_fun ? ? f a1) H2). +letin H4 \def (eq_imp_not_neq B (csf_fun ? ? f a0) (csf_fun ? ? f a1) H0). apply H4. exact H3. -Qed. +qed. + +definition bijective : \forall A, B :CSetoid. \forall f : CSetoid_fun A B. +? \def \lambda A, B :CSetoid. \lambda f : CSetoid_fun A B. +injective A B f \and surjective A B f. -Definition bijective A B (f:CSetoid_fun A B) := injective f and surjective f. -Implicit Arguments bijective [A B]. +(* Implicit Arguments bijective [A B]. *) -Lemma id_is_bij : forall A, bijective (id_un_op A). +lemma id_is_bij : \forall A:CSetoid. bijective ? ? (id_un_op A). intro A. -split. - red; simpl; auto. -intro b; exists b; apply eq_reflexive. -Qed. +split [unfold. simplify; intros. exact H| +unfold.intro. apply (ex_intro ).exact b. apply eq_reflexive] +qed. -Lemma comp_resp_bij : forall A B C f g, bijective f -> 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 comp_resp_bij :\forall A,B,C,f,g. + bijective ? ? f \to bijective ? ? g \to bijective ? ? (compose_CSetoid_fun A B C f g). +intros 5 (A B C f g). +intros 2 (H0 H1). +elim H0 0; clear H0;intros 2 (H00 H01). +elim H1 0; clear H1; intros 2 (H10 H11). +split[unfold. intros 2 (a0 a1); simplify; intro. +unfold compose_CSetoid_fun.simplify. + apply H10; apply H00;exact H|unfold. + intro c; unfold compose_CSetoid_fun.simplify. +elim (H11 c) 0;intros (b H20). +elim (H01 b) 0.intros (a H30). +apply ex_intro.apply a. +apply (eq_transitive_unfolded ? ? (csf_fun B C g b)). +apply csf_wd_unfolded.assumption.assumption] +qed. -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 invfun [A B]. *) + +record CSetoid_bijective_fun (A,B:CSetoid): Type \def +{ direct :2> CSetoid_fun A B; + inverse: CSetoid_fun B A; + inv1: \forall x:A.(csf_fun ? ? inverse (csf_fun ? ? direct x)) = x; + inv2: \forall x:B.(csf_fun ? ? direct (csf_fun ? ? inverse x)) = x + }. + +lemma invfun : \forall A,B:CSetoid. \forall f:CSetoid_bijective_fun A B. + B \to A. + intros (A B f ). + elim (inverse A B f).apply f1.apply c. +qed. -Implicit Arguments inv [A B]. +lemma inv_strext : \forall A,B. \forall f : CSetoid_bijective_fun A B. + fun_strext B A (invfun A B f). +intros.unfold invfun. +elim (inverse A B f).simplify.intros. +unfold in H.apply H.assumption. +qed. -Definition 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. +definition Inv: \forall A, B:CSetoid. +\forall f:CSetoid_bijective_fun A B. \forall H : (bijective ? ? (direct ? ? f)). ? \def +\lambda A, B:CSetoid. \lambda f:CSetoid_bijective_fun A B. \lambda H : (bijective ? ? (direct ? ? f)). + mk_CSetoid_fun B A (invfun ? ? f) (inv_strext ? ? f). -Lemma inv2 : forall A B (f : CSetoid_fun A B) (H : bijective f) (a : A), - invfun f H (f a) [=] a. +lemma eq_to_ap_to_ap: \forall A:CSetoid.\forall a,b,c:A. +a = b \to b \neq c \to a \neq c. intros. -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]. +generalize in match (ap_cotransitive_unfolded ? ? ? H1 a). +intro.elim H2.apply False_ind.apply (eq_imp_not_ap ? ? ? H). +apply ap_symmetric_unfolded. assumption. +assumption. +qed. -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. +lemma Dir_bij : \forall A, B:CSetoid. + \forall f : CSetoid_bijective_fun A B. + bijective ? ? (direct ? ? f). + intros.unfold bijective.split + [unfold injective.intros. + apply (csf_strext_unfolded ? ? (inverse ? ? f)). + elim f. + apply (eq_to_ap_to_ap ? ? ? ? (H1 ?)). + apply ap_symmetric_unfolded. + apply (eq_to_ap_to_ap ? ? ? ? (H1 ?)). + apply ap_symmetric_unfolded.assumption + |unfold surjective.intros. + elim f.autobatch. + ] +qed. + +lemma Inv_bij : \forall A, B:CSetoid. + \forall f : CSetoid_bijective_fun A B. + bijective ? ? (inverse A B f). + intros; + elim f 2; + elim c2 0; + elim c3 0; + simplify; + intros; + split; + [ intros; + apply H1; + apply (eq_to_ap_to_ap ? ? ? ? (H3 ?)). + apply ap_symmetric_unfolded. + apply (eq_to_ap_to_ap ? ? ? ? (H3 ?)). + apply ap_symmetric_unfolded.assumption| + intros.autobatch] +qed. +(* End bijections.*) -End bijections. -Implicit Arguments bijective [A B]. +(* Implicit Arguments bijective [A B]. Implicit Arguments injective [A B]. Implicit Arguments injective_weak [A B]. Implicit Arguments surjective [A B]. @@ -1219,6 +1297,7 @@ Implicit Arguments invfun [A B]. Implicit Arguments Inv [A B]. Implicit Arguments conj_wd [S P Q]. +*) -Notation Prj1 := (prj1 _ _ _ _). -Notation Prj2 := (prj2 _ _ _ _). +(* Notation Prj1 := (prj1 _ _ _ _). + Notation Prj2 := (prj2 _ _ _ _). *)