update in groud_2 and models

[helm.git] / helm / software / matita / library / technicalities / setoids.ma

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index f9c5e878bf1490346d82810827c2aea0d9470f36..fd1fb0037a1cff7c0525e3f88ed185df9b5eba08 100644 (file)
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -15,8 +15,6 @@
 (* Code ported from the Coq theorem prover by Claudio Sacerdoti Coen *)
 (* Original author: Claudio Sacerdoti Coen. for the Coq system       *)
 
-set "baseuri" "cic:/matita/technicalities/setoids".
-
 include "datatypes/constructors.ma".
 include "logic/coimplication.ma".
 include "logic/connectives2.ma".
@@ -86,8 +84,8 @@ definition Arguments := nelistT Argument_Class.
 definition function_type_of_morphism_signature :
  Arguments → Relation_Class → Type.
   intros (In Out); elim In; 
-  [ exact (carrier_of_relation_class ? t → carrier_of_relation_class ? Out)
-  | exact (carrier_of_relation_class ? t → T)
+  [ exact (carrier_of_relation_class ? a → carrier_of_relation_class ? Out)
+  | exact (carrier_of_relation_class ? a → T)
   ]
 qed. 
 
@@ -99,24 +97,24 @@ definition make_compatibility_goal_aux:
  generalize in match f; clear f;
   [ elim a; simplify in f f1;
      [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
-     | cases t;
+     | cases x;
         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
         ]
      | exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
-     | cases t;
+     | cases x;
         [ exact (∀x1,x2. r x1 x2 → relation_of_relation_class ? Out (f x1) (f1 x2))
         | exact (∀x1,x2. r x2 x1 → relation_of_relation_class ? Out (f x1) (f1 x2))
         ]
      | exact (∀x. relation_of_relation_class ? Out (f x) (f1 x))
      ]
   | change with
-     ((carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
-      (carrier_of_relation_class ? t → function_type_of_morphism_signature n Out) →
+     ((carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) →
+      (carrier_of_relation_class ? a → function_type_of_morphism_signature n Out) →
       Prop).
-    elim t; simplify in f f1;
+    elim a; simplify in f f1;
      [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
-     |2,4: cases t1;
+     |2,4: cases x;
         [1,3: exact (∀x1,x2. r x1 x2 → R (f x1) (f1 x2))
         |2,4: exact (∀x1,x2. r x2 x1 → R (f x1) (f1 x2))
         ]
@@ -136,8 +134,8 @@ record Morphism_Theory (In: Arguments) (Out: Relation_Class) : Type :=
 definition list_of_Leibniz_of_list_of_types: nelistT Type → Arguments.
  intro;
  elim n;
-  [ apply (singl ? (Leibniz ? t))
-  | apply (cons ? (Leibniz ? t) a)
+  [ apply (singl ? (Leibniz ? a))
+  | apply (cons ? (Leibniz ? a) a1)
   ]
 qed.
 
@@ -367,9 +365,9 @@ definition variance_of_argument_class : Argument_Class → option variance.
  intros;
  elim a;
   [ apply None
-  | apply (Some ? t)
+  | apply (Some ? x)
   | apply None
-  | apply (Some ? t)
+  | apply (Some ? x)
   | apply None
   ]
 qed.
@@ -569,8 +567,8 @@ in F0.
 definition product_of_arguments : Arguments → Type.
  intro;
  elim a;
-  [ apply (carrier_of_relation_class ? t)
-  | apply (Prod (carrier_of_relation_class ? t) T)
+  [ apply (carrier_of_relation_class ? a1)
+  | apply (Prod (carrier_of_relation_class ? a1) T)
   ]
 qed.
 
@@ -611,15 +609,15 @@ definition relation_of_product_of_arguments:
  elim In 0;
   [ simplify;
     intro;
-    exact (directed_relation_of_argument_class (get_rewrite_direction r t) t)
+    exact (directed_relation_of_argument_class (get_rewrite_direction r a) a)
   | intros;
-    change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
-    change in p1 with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
+    change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
+    change in p1 with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
     cases p (c p2);
     cases p1 (c1 p3);
    apply And;
     [ exact
-      (directed_relation_of_argument_class (get_rewrite_direction r t) t c c1)
+      (directed_relation_of_argument_class (get_rewrite_direction r a) a c c1)
     | exact (R p2 p3)
     ]
   ]
@@ -631,10 +629,10 @@ definition apply_morphism:
  intro;
  elim In;
   [ exact (f p)
-  | change in p with (Prod (carrier_of_relation_class variance t) (product_of_arguments n));
+  | change in p with (Prod (carrier_of_relation_class variance a) (product_of_arguments n));
    elim p;
-   change in f1 with (carrier_of_relation_class variance t → function_type_of_morphism_signature n Out);
-   exact (f ? (f1 t1) t2)
+   change in f1 with (carrier_of_relation_class variance a → function_type_of_morphism_signature n Out);
+   exact (f ? (f1 a1) b)
   ]
 qed.
 
@@ -651,14 +649,14 @@ theorem apply_morphism_compatibility_Right2Left:
    [ simplify in m1 m2 args1 args2 ⊢ %;
      change in H1 with
       (directed_relation_of_argument_class
-        (get_rewrite_direction Right2Left t) t args1 args2);
+        (get_rewrite_direction Right2Left a) a args1 args2);
      generalize in match H1; clear H1;
      generalize in match H; clear H;
      generalize in match args2; clear args2;
      generalize in match args1; clear args1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0; simplify;
+     elim a 0; simplify;
       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
         apply H;
         exact H1
@@ -682,31 +680,32 @@ theorem apply_morphism_compatibility_Right2Left:
         exact H1
       ]
    | change in m1 with
-      (carrier_of_relation_class variance t →
+      (carrier_of_relation_class variance a →
         function_type_of_morphism_signature n Out);
      change in m2 with
-      (carrier_of_relation_class variance t →
+      (carrier_of_relation_class variance a →
         function_type_of_morphism_signature n Out);
      change in args1 with
-      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+      ((carrier_of_relation_class ? a) × (product_of_arguments n));
      change in args2 with
-      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+      ((carrier_of_relation_class ? a) × (product_of_arguments n));
      generalize in match H2; clear H2;
      elim args2 0; clear args2;
      elim args1; clear args1;
+     simplify in H2;
+     change in H2:(? ? %) with 
+       (relation_of_product_of_arguments Right2Left n b b1);
      elim H2; clear H2;
-     change in H4 with
-      (relation_of_product_of_arguments Right2Left n t2 t4);
      change with
-      (relation_of_relation_class unit Out (apply_morphism n Out (m1 t3) t4)
-        (apply_morphism n Out (m2 t1) t2));
+      (relation_of_relation_class unit Out (apply_morphism n Out (m1 a2) b1)
+        (apply_morphism n Out (m2 a1) b));
      generalize in match H3; clear H3;
-     generalize in match t3; clear t3;
-     generalize in match t1; clear t1;
+     generalize in match a1; clear a1;
+     generalize in match a2; clear a2;
      generalize in match H1; clear H1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0;
+     elim a 0;
       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
         simplify in H3;
         change in H1 with
@@ -771,14 +770,14 @@ theorem apply_morphism_compatibility_Left2Right:
   elim In 0; simplify; intros;
    [ change in H1 with
       (directed_relation_of_argument_class
-        (get_rewrite_direction Left2Right t) t args1 args2);
+        (get_rewrite_direction Left2Right a) a args1 args2);
      generalize in match H1; clear H1;
      generalize in match H; clear H;
      generalize in match args2; clear args2;
      generalize in match args1; clear args1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0; simplify;
+     elim a 0; simplify;
       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
         apply H;
         exact H1
@@ -804,31 +803,31 @@ theorem apply_morphism_compatibility_Left2Right:
         exact H1
       ]
    | change in m1 with
-      (carrier_of_relation_class variance t →
+      (carrier_of_relation_class variance a →
         function_type_of_morphism_signature n Out);
      change in m2 with
-      (carrier_of_relation_class variance t →
+      (carrier_of_relation_class variance a →
         function_type_of_morphism_signature n Out);
      change in args1 with
-      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+      ((carrier_of_relation_class ? a) × (product_of_arguments n));
      change in args2 with
-      ((carrier_of_relation_class ? t) × (product_of_arguments n));
+      ((carrier_of_relation_class ? a) × (product_of_arguments n));
      generalize in match H2; clear H2;
      elim args2 0; clear args2;
      elim args1; clear args1;
+     simplify in H2; change in H2:(? ? %) with
+       (relation_of_product_of_arguments Left2Right n b b1); 
      elim H2; clear H2;
-     change in H4 with
-      (relation_of_product_of_arguments Left2Right n t2 t4);
      change with
-      (relation_of_relation_class unit Out (apply_morphism n Out (m1 t1) t2)
-        (apply_morphism n Out (m2 t3) t4));
+      (relation_of_relation_class unit Out (apply_morphism n Out (m1 a1) b)
+        (apply_morphism n Out (m2 a2) b1));
      generalize in match H3; clear H3;
-     generalize in match t3; clear t3;
-     generalize in match t1; clear t1;
+     generalize in match a2; clear a2;
+     generalize in match a1; clear a1;
      generalize in match H1; clear H1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0;
+     elim a 0;
       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
         change in H1 with
          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
@@ -898,7 +897,7 @@ definition interp :
      rewrite <
        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
      exact c1
-   | split;
+   | simplify;split;
       [ rewrite <
          (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
         exact c1
@@ -929,7 +928,7 @@ definition interp_relation_class_list :
      rewrite <
        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
      exact c1
-  | split;
+  | simplify; split;
      [ rewrite <
         (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
        exact c1