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.
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.
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 automaticamente *)
+lemma mycor: ∀S. CSetoid_bin_op S → (S → S → S).
+ intros;
+ unfold in c;
+ apply (c c1 c2).
+qed.
+coercion cic:/matita/algebra/CoRN/SetoidFun/mycor.con 2.
+
+(* Mettendola a mano con una beta-espansione funzionerebbe *)
+(*lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (\lambda e.mycor ? (comp_as_bin_op A) e)).*)
+(* Questo sarebbe anche meglio: senza beta-espansione *)
+(*lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (mycor ? (comp_as_bin_op A))).*)
+(* QUESTO E' QUELLO ORIGINALE MA NON FUNZIONANTE *)
+(* lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (comp_as_bin_op A)). *)
+lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (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]; auto.
+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.
+auto 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.auto new|simplify.intros.exact H1]|
+intros (a at).
+simplify.
+split[intro.auto new|intros. exact H1]
+]
+|
+intros (a at IHx).
+elim y 0[simplify.
+ split[intro.auto 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
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
%\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 : \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.
-Definition extend (x : S) : CProp := P x and (forall H : P x, R x H).
+inductive sigT (A:Type) (P:A -> Type) : Type \def
+ |existT : \forall x:A. P x \to sigT A P.
-Lemma ext1 : forall x : S, extend x -> P x.
-intros x H; inversion_clear H; assumption.
-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 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 (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.
+*)
+
+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 Extension.
+(*End Extension. *)
-End SubSets_of_G.
+(*End SubSets_of_G.*)
-Notation Conj := (conjP _).
+(* 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 automorphisms. *)
-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
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)}.*)
-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).
+(* end hide *)
+
+(* TODO ProjT1 *)
+lemma part_function_comp_strext : \forall S:CSetoid. \forall F,G: PartFunct S.
+\forall x,y:S. \forall Hx : UR S F G x. \forall Hy : (UR S F G y).
+ (pfpfun ? G (pfpfun ? F x (proj1_sigT ? ? Hx)) (proj2_sigTm ? ? Hx))
+ \neq (pfpfun ? G (pfpfun ? F y (proj1_sigT ? ? Hy)) (proj2_sigTm ? ? Hy)) \to x \neq y.
+intros (S F G x y Hx Hy H).
+exact (pfstrx ? ? ? ? ? ? (pfstrx ? ? ? ? ? ? H)).
+qed.
+(*
+definition TempR : \forall S:CSetoid. \forall F,G: PartFunct S. \forall x: S. ? \def
+ \lambda S:CSetoid. \lambda F,G: PartFunct S. \lambda x: S.
+ (ex ? (\lambda Hx : UP S F x. UQ S G (pfpfun S F x Hx))). *)
+
+lemma part_function_comp_dom_wd :\forall S:CSetoid. \forall F,G: PartFunct S.
+ pred_wd S (UR S F G).
+ intros.unfold.
+ intros (x y H H0).
+ unfold UR.
+ elim H.
+ unfold in a.
+ unfold UP.unfold UQ.
+ apply (existT).
+ apply (dom_wd S F x y a H0).
+apply (dom_wd S G (pfpfun S F x a)).
assumption.
apply pfwdef; assumption.
-Qed.
+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).
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 A B (f:CSetoid_fun A B) := injective f and surjective f.
+definition bijective : \forall A, B :CSetoid. \forall f : CSetoid_fun A B.
+? \def \lambda A, B :CSetoid. \lambda f : CSetoid_fun A B.
+injective A B f \and surjective A B f.
-Implicit Arguments bijective [A B].
-Lemma id_is_bij : forall A, bijective (id_un_op A).
+(* Implicit Arguments bijective [A B]. *)
+
+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).
+auto.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.auto.
+ ]
+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.auto]
+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].
Implicit Arguments Inv [A B].
Implicit Arguments conj_wd [S P Q].
+*)
-Notation Prj1 := (prj1 _ _ _ _).
-Notation Prj2 := (prj2 _ _ _ _).
+(* Notation Prj1 := (prj1 _ _ _ _).
+ Notation Prj2 := (prj2 _ _ _ _). *)
projects / helm.git / blobdiff