frst step to move away the CoRN stuff

[helm.git] / helm / software / matita / library / algebra / CoRN / Setoids.ma

diff --git a/helm/software/matita/library/algebra/CoRN/Setoids.ma b/helm/software/matita/library/algebra/CoRN/Setoids.ma
index a48d1a522b2c01f14d03dca94cb26b3fe0c4ecb0..ee5f99610ed7be4c91f32c4835c4ed61ef3e3cbd 100644 (file)
--- 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"
    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"
 
 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? *)
 
 (* 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----------------------- *)
 
 
 (* -----------------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.
       
 
 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.
 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
    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.
   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
   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
    ]
    [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
    [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
  |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.
 
 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.
 
 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 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.
 
 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.
 
 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 *)
 (* 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.
 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.
 
 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.
 \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.
 
 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.
 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.
 
 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.
 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.
 
 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.
 apply eq_symmetric_unfolded.assumption.
 apply eq_symmetric_unfolded.assumption.
 apply H.

-autobatch new.
+autobatch.

 qed.
 
 (*
 qed.
 
 (*