X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=4c51d3a448e15a900e8b28f2118cb480139614fd;hb=bba3b7f83610c3babb797e8ce1e844a560303295;hp=bb8aacac69d4d929ce27f00665348004b349f54e;hpb=a180bddcd4a8f35de3d7292162ba05d0077723aa;p=helm.git

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index bb8aacac6..4c51d3a44 100644
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -18,8 +18,8 @@
 set "baseuri" "cic:/matita/technicalities/setoids".
 
 include "datatypes/constructors.ma".
-include "logic/connectives2.ma".
 include "logic/coimplication.ma".
+include "logic/connectives2.ma".
 
 (* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
 
@@ -150,8 +150,8 @@ definition morphism_theory_of_function :
     Morphism_Theory In' Out'.
   intros;
   apply (mk_Morphism_Theory ? ? f);
-  unfold In' in f; clear In';
-  unfold Out' in f; clear Out';
+  unfold In' in f ⊢ %; clear In';
+  unfold Out' in f ⊢ %; clear Out';
   generalize in match f; clear f;
   elim In;
    [ unfold make_compatibility_goal;
@@ -203,13 +203,29 @@ definition equality_morphism_of_symmetric_areflexive_transitive_relation:
  apply mk_Morphism_Theory;
   [ exact Aeq
   | unfold make_compatibility_goal;
-    simplify;
+    simplify; unfold ASetoidClass; simplify;
     intros;
     split;
     unfold transitive in H;
     unfold symmetric in sym;
     intro;
-    autobatch new
+      [ apply (H x2 x1 x3 ? ?);
+          [apply (sym x1 x2 ?).
+           apply (H1).
+          |apply (H x1 x x3 ? ?);
+            [apply (H3).
+            |apply (H2).
+            ]
+          ]
+      | apply (H x1 x3 x ? ?);
+         [apply (H x1 x2 x3 ? ?);
+            [apply (H1).
+            |apply (H3).
+            ]
+         |apply (sym x x3 ?).
+          apply (H2).
+         ]
+      ]
   ].
 qed.
 
@@ -220,14 +236,33 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation:
     (Morphism_Theory (cons ? ASetoidClass (singl ? ASetoidClass)) Iff_Relation_Class).
  intros;
  apply mk_Morphism_Theory;
- reduce;
+ normalize;
   [ exact Aeq
   | intros;
     split;
     intro;
     unfold transitive in H;
     unfold symmetric in sym;
-    autobatch depth=4.
+    [ apply (H x2 x1 x3 ? ?);
+        [apply (sym x1 x2 ?).
+         apply (H1).
+        |apply (H x1 x x3 ? ?);
+          [apply (H3).
+          |apply (H2).
+          ]
+        ]
+    | apply (H x1 x2 x ? ?);
+      [apply (H1).
+      |apply (H x2 x3 x ? ?);
+        [apply (H3).
+        |apply (sym x x3 ?).
+         apply (H x x3 x3 ? ?);
+          [apply (H2).
+          |apply (refl x3).
+          ]
+        ]
+      ]
+    ]
   ]
 qed.
 
@@ -240,11 +275,17 @@ definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
  apply mk_Morphism_Theory;
  [ simplify;
    apply Aeq
- | simplify;
+ | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
    intros;
    whd;
    intros;
-   autobatch
+   apply (H x2 x1 x3 ? ?);
+    [apply (H1).
+    |apply (H x1 x x3 ? ?);
+      [apply (H3).
+      |apply (H2).
+      ]
+    ]
  ].
 qed.
 
@@ -257,11 +298,17 @@ definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
  apply mk_Morphism_Theory;
  [ simplify;
    apply Aeq
- | simplify;
+ | simplify; unfold ASetoidClass1; simplify; unfold ASetoidClass2; simplify;
    intros;
    whd;
    intro;
-   autobatch
+   apply (H x2 x1 x3 ? ?);
+     [apply (H1).
+     |apply (H x1 x x3 ? ?);
+       [apply (H3).
+       |apply (H2).
+       ]
+     ]
  ].
 qed.
 
@@ -285,7 +332,7 @@ definition morphism_theory_of_predicate :
   | generalize in match f; clear f;
     unfold In'; clear In';
     elim In;
-     [ reduce;
+     [ normalize;
        intro;
        apply iff_refl
      | simplify;
@@ -301,6 +348,7 @@ theorem impl_trans: transitive ? impl.
  whd;
  unfold impl;
  intros;
+ apply (H1 ?).apply (H ?).apply (H2).
  autobatch.
 qed.
 
@@ -646,9 +694,10 @@ theorem apply_morphism_compatibility_Right2Left:
      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 t2 t4);
      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));
@@ -768,9 +817,9 @@ theorem apply_morphism_compatibility_Left2Right:
      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 t2 t4); 
      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));
@@ -850,7 +899,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
@@ -881,7 +930,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