cs_proof : is_CSetoid cs_crr cs_eq cs_ap}.
interpretation "setoid equality"
- 'eq x y = (cic:/matita/algebra/CoRN/Setoid/cs_eq.con _ x y).
+ 'eq x y = (cic:/matita/algebra/CoRN/Setoids/cs_eq.con _ x y).
interpretation "setoid apart"
- 'neq x y = (cic:/matita/algebra/CoRN/Setoid/cs_ap.con _ x y).
+ 'neq x y = (cic:/matita/algebra/CoRN/Setoids/cs_ap.con _ x y).
(* visto che sia "ap" che "eq" vanno in Prop e data la "tight-apartness",
"cs_neq" e "ap" non sono la stessa cosa? *)
(* -----------------The product of setoids----------------------- *)
-definition prod_ap: \forall A,B : CSetoid.\forall c,d: ProdT A B. Prop \def
-\lambda A,B : CSetoid.\lambda c,d: ProdT A B.
- ((cs_ap A (fstT A B c) (fstT A B d)) \or
- (cs_ap B (sndT A B c) (sndT A B d))).
+definition prod_ap: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def
+\lambda A,B : CSetoid.\lambda c,d: Prod A B.
+ ((cs_ap A (fst A B c) (fst A B d)) \or
+ (cs_ap B (snd A B c) (snd A B d))).
-definition prod_eq: \forall A,B : CSetoid.\forall c,d: ProdT A B. Prop \def
-\lambda A,B : CSetoid.\lambda c,d: ProdT A B.
- ((cs_eq A (fstT A B c) (fstT A B d)) \and
- (cs_eq B (sndT A B c) (sndT A B d))).
+definition prod_eq: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def
+\lambda A,B : CSetoid.\lambda c,d: Prod A B.
+ ((cs_eq A (fst A B c) (fst A B d)) \and
+ (cs_eq B (snd A B c) (snd A B d))).
lemma prodcsetoid_is_CSetoid: \forall A,B: CSetoid.
- is_CSetoid (ProdT A B) (prod_eq A B) (prod_ap A B).
+ is_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B).
intros.
apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
[unfold.
definition ProdCSetoid : \forall A,B: CSetoid. CSetoid \def
\lambda A,B: CSetoid.
- mk_CSetoid (ProdT A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).
+ mk_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).
definition un_op_fun: \forall S:CSetoid. CSetoid_un_op S \to CSetoid_fun S S
\def \lambda S.\lambda f.f.
-coercion cic:/matita/algebra/CoRN/Setoid/un_op_fun.con.
+coercion cic:/matita/algebra/CoRN/Setoids/un_op_fun.con.
definition cs_un_op_strext : \forall S:CSetoid. \forall f: CSetoid_fun S S. fun_strext S S (csf_fun S S f) \def
\lambda S:CSetoid. \lambda f : CSetoid_fun S S. csf_strext S S f.
definition bin_op_bin_fun: \forall S:CSetoid. CSetoid_bin_op S \to CSetoid_bin_fun S S S
\def \lambda S.\lambda f.f.
-coercion cic:/matita/algebra/CoRN/Setoid/bin_op_bin_fun.con.
+coercion cic:/matita/algebra/CoRN/Setoids/bin_op_bin_fun.con.
CSetoid_outer_op S S \to CSetoid_bin_fun S S S
\def \lambda S.\lambda f.f.
-coercion cic:/matita/algebra/CoRN/Setoid/outer_op_bin_fun.con.
+coercion cic:/matita/algebra/CoRN/Setoids/outer_op_bin_fun.con.
(* begin hide
Identity Coercion outer_op_bin_fun : CSetoid_outer_op >-> CSetoid_bin_fun.
end hide *)
unfold.unfold.intros 2.elim x 2.elim y 2.
simplify.
intro.
-reduce in H2.
+normalize in H2.
apply (un_op_wd_unfolded ? f ? ? H2).
qed.
\forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
un_op_strext (mk_SubCSetoid S P) (restr_un_op S P f pr).
intros.unfold.unfold. intros 2.elim y 2. elim x 2.
-intros.reduce in H2.
+intros.normalize in H2.
apply (cs_un_op_strext ? f ? ? H2).
qed.
unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
simplify.
intros.
-reduce in H4.
-reduce in H5.
+normalize in H4.
+normalize in H5.
apply (cs_bin_op_wd ? f ? ? ? ? H4 H5).
qed.
bin_op_strext (mk_SubCSetoid S P) (restr_bin_op S P f pr).
intros.unfold.unfold. intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
simplify.intros.
-reduce in H4.
+normalize in H4.
apply (cs_bin_op_strext ? f ? ? ? ? H4).
qed.