X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2FCoRN%2FSetoids.ma;h=ee5f99610ed7be4c91f32c4835c4ed61ef3e3cbd;hb=bfef67a8e21e943fa760512faeddd47b5a236ca5;hp=a48d1a522b2c01f14d03dca94cb26b3fe0c4ecb0;hpb=a180bddcd4a8f35de3d7292162ba05d0077723aa;p=helm.git

diff --git a/helm/software/matita/library/algebra/CoRN/Setoids.ma b/helm/software/matita/library/algebra/CoRN/Setoids.ma
index a48d1a522..ee5f99610 100644
--- a/helm/software/matita/library/algebra/CoRN/Setoids.ma
+++ b/helm/software/matita/library/algebra/CoRN/Setoids.ma
@@ -48,10 +48,10 @@ record CSetoid : Type \def
    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? *)
@@ -215,19 +215,19 @@ 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.
@@ -237,8 +237,8 @@ apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
    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.
@@ -258,14 +258,14 @@ apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
   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
@@ -291,8 +291,8 @@ apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
  |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
   ]
  ]
 ]
@@ -301,7 +301,7 @@ qed.
 
 definition ProdCSetoid : \forall A,B: CSetoid. CSetoid \def
  \lambda A,B: CSetoid.
-  mk_CSetoid (ProdT A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).
+  mk_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).
 
 
 
@@ -809,7 +809,7 @@ 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.
@@ -862,7 +862,7 @@ definition cs_bin_op_strext : \forall S:CSetoid. \forall f: CSetoid_bin_fun S S
 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.
 
 
 
@@ -982,7 +982,7 @@ definition outer_op_bin_fun: \forall S:CSetoid.
 CSetoid_outer_op S S \to CSetoid_bin_fun S S S
 \def \lambda S.\lambda f.f.
 
-coercion cic:/matita/algebra/CoRN/Setoid/outer_op_bin_fun.con.
+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 *)
@@ -1115,7 +1115,7 @@ intros.
 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.
 
@@ -1123,7 +1123,7 @@ lemma restr_un_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
 \forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.  
 un_op_strext (mk_SubCSetoid S P) (restr_un_op S P f pr).
 intros.unfold.unfold. intros 2.elim y 2. elim x 2.
-intros.reduce in H2.
+intros.normalize in H2.
 apply (cs_un_op_strext ? f ? ? H2).
 qed.
 
@@ -1182,8 +1182,8 @@ intros.
 unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
 simplify.
 intros.
-reduce in H4.
-reduce in H5.
+normalize in H4.
+normalize in H5.
 apply (cs_bin_op_wd ? f ? ? ? ? H4 H5).
 qed.
 
@@ -1192,7 +1192,7 @@ lemma restr_bin_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
 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.
 
@@ -1263,7 +1263,7 @@ apply f. apply n1. apply m1.
 apply eq_symmetric_unfolded.assumption.
 apply eq_symmetric_unfolded.assumption.
 apply H.
-autobatch new.
+autobatch.
 qed.
 
 (*