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? *)
elim H. apply H1. assumption.
qed.
+axiom eq_symmetric : \forall S : CSetoid. symmetric S (cs_eq S).
+(*
lemma eq_symmetric : \forall S : CSetoid. symmetric S (cs_eq S).
intro. unfold. intros.
generalize in match (ap_tight S x y). intro.
generalize in match (ap_symmetric S y x). intro.
elim H1. clear H1.
elim H2. clear H2.
-apply H1. unfold. intro. auto.
+apply H1. unfold. intro. autobatch.
qed.
-
+*)
lemma eq_transitive : \forall S : CSetoid. transitive S (cs_eq S).
intro. unfold. intros (x y z H H0).
generalize in match (ap_tight S x y). intro.
apply eq_transitive.
qed.
+
lemma eq_wdl : \forall S:CSetoid. \forall x,y,z:S. x = y \to x = z \to z = y.
intros.
-(* perche' auto non arriva in fondo ??? *)
-apply (eq_transitive_unfolded ? ? x). auto.
-assumption.
+(* perche' autobatch non arriva in fondo ??? *)
+apply (eq_transitive_unfolded ? ? x).
+apply eq_symmetric_unfolded.
+exact H1.
+exact H.
qed.
+
lemma ap_irreflexive_unfolded : \forall S:CSetoid. \forall x:S. \not (x \neq x).
apply ap_irreflexive.
qed.
(* -----------------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.
unfold prod_ap. simplify.
intros.
elim H
- [apply (ap_irreflexive A t H1)
- |apply (ap_irreflexive B t1 H1)
+ [apply (ap_irreflexive A a H1)
+ |apply (ap_irreflexive B b H1)
]
|unfold.
intros 2.
unfold prod_ap in H. simplify in H.
unfold prod_ap. simplify.
elim H
- [cut ((t \neq t4) \or (t4 \neq t2))
+ [cut ((a \neq a2) \or (a2 \neq a1))
[elim Hcut
[left. left. assumption
|right. left. assumption
]
|apply (ap_cotransitive A). assumption
]
- |cut ((t1 \neq t5) \or (t5 \neq t3))
+ |cut ((b \neq b2) \or (b2 \neq b1))
[elim Hcut
[left. right. assumption
|right. right. assumption
|intro. unfold. intro.
elim H.
elim H1
- [apply (eq_imp_not_ap A t t2 H2). assumption
- |apply (eq_imp_not_ap B t1 t3 H3). assumption
+ [apply (eq_imp_not_ap A a a1 H2). assumption
+ |apply (eq_imp_not_ap B b b1 H3). assumption
]
]
]
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).
P x \to (P y \or (x \neq y)).
(* Definition pred_wd : CProp := forall x y : S, P x -> x [=] y -> P y. *)
-definition pred_wd : \forall S: CSetoid. (S \to Prop) \to Prop \def
- \lambda S: CSetoid. \lambda P: S \to Prop. \forall x,y : S.
+definition pred_wd : \forall S: CSetoid. \forall P :S \to Type. Type \def
+ \lambda S: CSetoid. \lambda P: S \to Type. \forall x,y : S.
P x \to x = y \to P y.
record wd_pred (S: CSetoid) : Type \def
intro x; intros y H H0.
elim (csp'_strext P x y H).
-auto.
+autobatch.
intro H1.
elimtype False.
intro H1.
elim (H1 H0).
-auto.
+autobatch.
intro H3.
elim H3; intro H4.
-auto.
+autobatch.
elim (ap_irreflexive _ _ H4).
Qed.
generalize (H x x y1 y2 H0); intro H1.
elim H1; intro H2.
-auto.
+autobatch.
elim H2; intro H3.
elim (ap_irreflexive _ _ H3).
-auto.
+autobatch.
Qed.
Lemma Crel_strextarg_imp_strext :
Crel_strext_rht -> Crel_strext_lft -> Crel_strext.
unfold Crel_strext, Crel_strext_lft, Crel_strext_rht in |- *;
intros H H0 x1 x2 y1 y2 H1.
-elim (H x1 y1 y2 H1); auto.
+elim (H x1 y1 y2 H1); autobatch.
intro H2.
-elim (H0 x1 x2 y2 H2); auto.
+elim (H0 x1 x2 y2 H2); autobatch.
Qed.
*)
red in |- *; intros x y z H H0.
elim (Ccsr_strext R x x y z H).
-auto.
+autobatch.
intro H1; elimtype False.
elim H1; intro H2.
red in |- *; intros x y z H H0.
elim (Ccsr_strext R x z y y H).
-auto.
+autobatch.
intro H1; elimtype False.
elim H1; intro H2.
red in |- *; intros x1 x2 y1 y2 H.
case (ap_cotransitive_unfolded _ _ _ H x2); intro H0.
-auto.
+autobatch.
case (ap_cotransitive_unfolded _ _ _ H0 y2); intro H1.
-auto.
+autobatch.
right; right.
apply ap_symmetric_unfolded.
record CSetoid_bin_fun (S1,S2,S3: CSetoid) : Type \def
- {csbf_fun : S1 \to S2 \to S3;
+ {csbf_fun :2> S1 \to S2 \to S3;
csbf_strext : (bin_fun_strext S1 S2 S3 csbf_fun)}.
lemma csbf_wd : \forall S1,S2,S3: CSetoid. \forall f : CSetoid_bin_fun S1 S2 S3.
\lambda S: CSetoid. \lambda f : S \to S \to S.
\forall x,y : S. f x y = f y x.
-definition associative : \forall S: CSetoid. (S \to S \to S) \to Prop \def
+definition CSassociative : \forall S: CSetoid. \forall f: S \to S \to S. Prop \def
\lambda S: CSetoid. \lambda f : S \to S \to S.
\forall x,y,z : S.
f x (f y z) = f (f x y) z.
lemma id_strext : \forall S:CSetoid. un_op_strext S (\lambda x:S. x).
unfold un_op_strext.
-unfold fun_strext.intros.
-simplify.assumption.
+unfold fun_strext.
+intros.
+simplify in H.
+exact H.
qed.
lemma id_pres_eq : \forall S:CSetoid. un_op_wd S (\lambda x : S.x).
unfold un_op_wd.
unfold fun_wd.
intros.
-simplify.assumption.
+simplify.
+exact H.
qed.
definition id_un_op : \forall S:CSetoid. CSetoid_un_op S
definition un_op_fun: \forall S:CSetoid. CSetoid_un_op S \to CSetoid_fun S S
\def \lambda S.\lambda f.f.
-coercion cic:/matita/algebra/CoRN/Setoid/un_op_fun.con.
+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 *)
]
qed.
+(*
+axiom subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop.
+is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
+*)
+
lemma subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop.
is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
intros.
apply (mk_is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P))
[ unfold. intros.unfold. elim x. exact (ap_irreflexive_unfolded S ? ?)
- [ assumption | apply H1.]
+ [ assumption | simplify in H1. exact H1 ]
(* irreflexive *)
|unfold. intros 2. elim x. generalize in match H1. elim y.simplify in H3. simplify.
exact (ap_symmetric ? ? ? H3)
apply (ap_tight S ? ?)]
qed.
+
definition mk_SubCSetoid : \forall S:CSetoid. \forall P: S \to Prop. CSetoid \def
\lambda S:CSetoid. \lambda P:S \to Prop.
mk_CSetoid (subcsetoid_crr S P) (subcsetoid_eq S P) (subcsetoid_ap S P) (subcsetoid_is_CSetoid S P).
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.
definition mk_SubCSetoid_un_op : \forall S:CSetoid. \forall P: S \to Prop. \forall f: CSetoid_un_op S.
- \forall pr:un_op_pres_pred S P f.
- CSetoid_un_op (mk_SubCSetoid S P) \def
+ \forall pr:un_op_pres_pred S P f. CSetoid_un_op (mk_SubCSetoid S P).
+ intros (S P f pr).
+ apply (mk_CSetoid_un_op (mk_SubCSetoid S P) (restr_un_op S P f pr) (restr_un_op_strext S P f pr)).
+ qed.
+
+(* BUG Universe Inconsistency detected
+ definition mk_SubCSetoid_un_op : \forall S:CSetoid. \forall P: S \to Prop. \forall f: CSetoid_un_op S.
+ \forall pr:un_op_pres_pred S P f. CSetoid_un_op (mk_SubCSetoid S P) \def
\lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
\lambda pr:un_op_pres_pred S P f.
mk_CSetoid_un_op (mk_SubCSetoid S P) (restr_un_op S P f pr) (restr_un_op_strext S P f pr).
-
+*)
(* Subsetoid binary operations
Let [f] be a binary setoid operation on [S].
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.
+definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop.
+ \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
+ CSetoid_bin_op (mk_SubCSetoid S P).
+ intros (S P f pr).
+ apply (mk_CSetoid_bin_op (mk_SubCSetoid S P) (restr_bin_op S P f pr)(restr_bin_op_strext S P f pr)).
+ qed.
+
+(* BUG Universe Inconsistency detected
definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop.
\forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
CSetoid_bin_op (mk_SubCSetoid S P) \def
\lambda S:CSetoid. \lambda P: S \to Prop.
\lambda f: CSetoid_bin_op S. \lambda pr: bin_op_pres_pred S P f.
mk_CSetoid_bin_op (mk_SubCSetoid S P) (restr_bin_op S P f pr)(restr_bin_op_strext S P f pr).
+*)
lemma restr_f_assoc : \forall S:CSetoid. \forall P: S \to Prop.
\forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
- associative S (csbf_fun S S S f)
- \to associative (mk_SubCSetoid S P) (csbf_fun (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid_bin_op S P f pr)).
+ CSassociative S (csbf_fun S S S f)
+ \to CSassociative (mk_SubCSetoid S P) (csbf_fun (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid_bin_op S P f pr)).
intros 4.
intro.
unfold.
elim m.simplify.reflexivity.reflexivity.
qed.
+
+
lemma proper_caseZ_diff_CS : \forall CS : CSetoid. \forall f : nat \to nat \to CS.
(\forall m,n,p,q : nat. eq nat (plus m q) (plus n p) \to (f m n) = (f p q)) \to
\forall m,n : nat. caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = (f m n).
apply eq_symmetric_unfolded.assumption.
apply eq_symmetric_unfolded.assumption.
apply H.
-auto.
+autobatch.
qed.
+
(*
Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
*)
projects / helm.git / blobdiff