autobatch => [auto]

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

diff --git a/matita/library/technicalities/setoids.ma b/matita/library/technicalities/setoids.ma
index e589a33d047e65a16aa02e5a47469ecd193fe022..b945931c14dab117679f714a0a3c3d7e3aa1cd72 100644 (file)
--- a/matita/library/technicalities/setoids.ma
+++ b/matita/library/technicalities/setoids.ma
@@ -62,19 +62,19 @@ definition relation_class_of_argument_class : Argument_Class → Relation_Class.
 qed.
 
 definition carrier_of_relation_class : ∀X. X_Relation_Class X → Type.
- intros (X x); cases x; clear x; [2,4:clear x1] clear X; assumption.
+ intros (X x); cases x (A o o o o A o o A o o o A o A); exact A.
 qed.
 
 definition relation_of_relation_class:
  ∀X,R. carrier_of_relation_class X R → carrier_of_relation_class X R → Prop.
- intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ]
+intros 2; cases R; simplify; [1,2,3,4: assumption | apply (eq T) ]
 qed.
 
 lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
  ∀R.
   carrier_of_relation_class ? (relation_class_of_argument_class R) =
    carrier_of_relation_class ? R.
- intro; cases R; reflexivity.
+intro; cases R; reflexivity.
 qed.
 
 inductive nelistT (A : Type) : Type :=
@@ -155,9 +155,7 @@ definition morphism_theory_of_function :
   generalize in match f; clear f;
   elim In;
    [ unfold make_compatibility_goal;
-     simplify;
-     intros;
-     whd;
+     whd; intros;
      reflexivity
    | simplify;
      intro;
@@ -211,7 +209,23 @@ definition equality_morphism_of_symmetric_areflexive_transitive_relation:
     unfold transitive in H;
     unfold symmetric in sym;
     intro;
-    auto 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.
 
@@ -229,7 +243,26 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation:
     intro;
     unfold transitive in H;
     unfold symmetric in sym;
-    auto 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.
 
@@ -246,7 +279,13 @@ definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
    intros;
    whd;
    intros;
-   auto
+   apply (H x2 x1 x3 ? ?);
+    [apply (H1).
+    |apply (H x1 x x3 ? ?);
+      [apply (H3).
+      |apply (H2).
+      ]
+    ]
  ].
 qed.
 
@@ -263,7 +302,13 @@ definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
    intros;
    whd;
    intro;
-   auto
+   apply (H x2 x1 x3 ? ?);
+     [apply (H1).
+     |apply (H x1 x x3 ? ?);
+       [apply (H3).
+       |apply (H2).
+       ]
+     ]
  ].
 qed.
 
@@ -303,7 +348,8 @@ theorem impl_trans: transitive ? impl.
  whd;
  unfold impl;
  intros;
- auto.
+ apply (H1 ?).apply (H ?).apply (H2).
+ autobatch.
 qed.
 
 (*DA PORTARE: Add Relation Prop impl
@@ -530,7 +576,7 @@ qed.
 
 definition get_rewrite_direction: rewrite_direction → Argument_Class → rewrite_direction.
  intros (dir R);
- cases (variance_of_argument_class R);
+ cases (variance_of_argument_class R) (a);
   [ exact dir
   | cases a;
      [ exact dir                      (* covariant *)
@@ -569,12 +615,12 @@ definition relation_of_product_of_arguments:
   | 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));
-    cases p;
-    cases p1;
+    cases p (c p2);
+    cases p1 (c1 p3);
    apply And;
     [ exact
-      (directed_relation_of_argument_class (get_rewrite_direction r t) t a a1)
-    | exact (R b b1)
+      (directed_relation_of_argument_class (get_rewrite_direction r t) t c c1)
+    | exact (R p2 p3)
     ]
   ]
 qed. 
@@ -612,26 +658,21 @@ theorem apply_morphism_compatibility_Right2Left:
      generalize in match args1; clear args1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0;
+     elim t 0; simplify;
       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
-        simplify in H;
-        simplify in H1;
-        simplify;
         apply H;
         exact H1
       | intros 8 (v T1 r Hr m1 m2 args1 args2);
-        cases v;
+        cases v; 
+        simplify;
         intros (H H1);
-        simplify in H1;
-        apply H;
-        exact H1
+        apply (H ? ? H1);
       | intros;
         apply H1;
         exact H2
       | intros 7 (v);
-        cases v;
+        cases v; simplify;
         intros (H H1);
-        simplify in H1;
         apply H;
         exact H1
       | intros;
@@ -726,10 +767,9 @@ theorem apply_morphism_compatibility_Left2Right:
         directed_relation_of_relation_class Left2Right ?
          (apply_morphism ? ? m1 args1)
          (apply_morphism ? ? m2 args2).
-  intro;
-  elim In;
-   [ simplify in m1 m2 args1 args2 ⊢ %;
-     change in H1 with
+  intro; 
+  elim In 0; simplify; intros;
+   [ change in H1 with
       (directed_relation_of_argument_class
         (get_rewrite_direction Left2Right t) t args1 args2);
      generalize in match H1; clear H1;
@@ -738,11 +778,8 @@ theorem apply_morphism_compatibility_Left2Right:
      generalize in match args1; clear args1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0;
+     elim t 0; simplify;
       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
-        simplify in H;
-        simplify in H1;
-        simplify;
         apply H;
         exact H1
       | intros 8 (v T1 r Hr m1 m2 args1 args2);
@@ -793,7 +830,6 @@ theorem apply_morphism_compatibility_Left2Right:
      generalize in match m1; clear m1;
      elim t 0;
       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
-        simplify in H3;
         change in H1 with
          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
      | intro v;
@@ -982,39 +1018,39 @@ Qed.
 (* impl IS A MORPHISM *)
 
 Add Morphism impl with signature iff ==> iff ==> iff as Impl_Morphism.
-unfold impl; tauto.
+unfold impl; tautobatch.
 Qed.
 
 (* and IS A MORPHISM *)
 
 Add Morphism and with signature iff ==> iff ==> iff as And_Morphism.
- tauto.
+ tautobatch.
 Qed.
 
 (* or IS A MORPHISM *)
 
 Add Morphism or with signature iff ==> iff ==> iff as Or_Morphism.
- tauto.
+ tautobatch.
 Qed.
 
 (* not IS A MORPHISM *)
 
 Add Morphism not with signature iff ==> iff as Not_Morphism.
- tauto.
+ tautobatch.
 Qed.
 
 (* THE SAME EXAMPLES ON impl *)
 
 Add Morphism and with signature impl ++> impl ++> impl as And_Morphism2.
- unfold impl; tauto.
+ unfold impl; tautobatch.
 Qed.
 
 Add Morphism or with signature impl ++> impl ++> impl as Or_Morphism2.
- unfold impl; tauto.
+ unfold impl; tautobatch.
 Qed.
 
 Add Morphism not with signature impl -→ impl as Not_Morphism2.
- unfold impl; tauto.
+ unfold impl; tautobatch.
 Qed.
 
 *)