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 cfc6f524e63b48492c88c0ec3330b56f46d3cd4c..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? *)


@@ -101,7 +101,7 @@ generalize in match (ap_tight S y x). intro.
 generalize in match (ap_symmetric S y x). intro.
 elim H1. clear H1.
 elim H2. clear H2.
 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).
 qed.
 *)
 lemma eq_transitive : \forall S : CSetoid. transitive S (cs_eq S).


@@ -135,7 +135,7 @@ qed.
 
 lemma eq_wdl : \forall S:CSetoid. \forall x,y,z:S. x = y \to x = z \to z = y.
 intros.
 
 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 ??? *)
+(* perche' autobatch non arriva in fondo ??? *)

 apply (eq_transitive_unfolded ? ? x).
 apply eq_symmetric_unfolded.
 exact H1.
 apply (eq_transitive_unfolded ? ? x).
 apply eq_symmetric_unfolded.
 exact H1.


@@ -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).

 
 
 
 
 
 


@@ -361,7 +361,7 @@ intro P.
 intro x; intros y H H0.
 elim (csp'_strext P x y H).
 
 intro x; intros y H H0.
 elim (csp'_strext P x y H).
 

-auto.
+autobatch.

 
 intro H1.
 elimtype False.
 
 intro H1.
 elimtype False.


@@ -503,12 +503,12 @@ generalize (H x1 x2 y y).
 intro H1.
 elim (H1 H0).
 
 intro H1.
 elim (H1 H0).
 

-auto.
+autobatch.

 
 intro H3.
 elim H3; intro H4.
 
 
 intro H3.
 elim H3; intro H4.
 

-auto.
+autobatch.

 elim (ap_irreflexive _ _ H4).
 Qed.
 
 elim (ap_irreflexive _ _ H4).
 Qed.
 


@@ -517,22 +517,22 @@ unfold Crel_strext, Crel_strext_rht in |- *; intros H x y1 y2 H0.
 generalize (H x x y1 y2 H0); intro H1.
 elim H1; intro H2.
 
 generalize (H x x y1 y2 H0); intro H1.
 elim H1; intro H2.
 

-auto.
+autobatch.

 
 elim H2; intro H3.
 
 elim (ap_irreflexive _ _ H3).
 
 
 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.
 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.
 intro H2.

-elim (H0 x1 x2 y2 H2); auto.
+elim (H0 x1 x2 y2 H2); autobatch.

 Qed.
 *)
 
 Qed.
 *)
 


@@ -553,7 +553,7 @@ intro R.
 red in |- *; intros x y z H H0.
 elim (Ccsr_strext R x x y z H).
 
 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.
 
 intro H1; elimtype False.
 elim H1; intro H2.


@@ -569,7 +569,7 @@ intro R.
 red in |- *; intros x y z H H0.
 elim (Ccsr_strext R x z y y H).
 
 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.
 
 intro H1; elimtype False.
 elim H1; intro H2.


@@ -614,11 +614,11 @@ Lemma ap_strext : Crel_strext (cs_ap (c:=S)).
 red in |- *; intros x1 x2 y1 y2 H.
 case (ap_cotransitive_unfolded _ _ _ H x2); intro H0.
 
 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.
 
 
 case (ap_cotransitive_unfolded _ _ _ H0 y2); intro H1.
 

-auto.
+autobatch.

 
 right; right.
 apply ap_symmetric_unfolded.
 
 right; right.
 apply ap_symmetric_unfolded.


@@ -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.

-auto new.
+autobatch.

 qed.
 
 (*
 qed.
 
 (*