* Some simplifications to theorem in file totient1.ma.

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

diff --git a/matita/library/technicalities/setoids.ma b/matita/library/technicalities/setoids.ma
index 0f3bda302d116a7b8bfbf7a9a1736c9cfab70d23..bb8aacac69d4d929ce27f00665348004b349f54e 100644 (file)
--- a/matita/library/technicalities/setoids.ma
+++ b/matita/library/technicalities/setoids.ma
@@ -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,7 @@ definition equality_morphism_of_symmetric_areflexive_transitive_relation:
     unfold transitive in H;
     unfold symmetric in sym;
     intro;
-    auto new
+    autobatch new
   ].
 qed.
 
@@ -229,7 +227,7 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation:
     intro;
     unfold transitive in H;
     unfold symmetric in sym;
-    auto depth=4.
+    autobatch depth=4.
   ]
 qed.
 
@@ -246,7 +244,7 @@ definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
    intros;
    whd;
    intros;
-   auto
+   autobatch
  ].
 qed.
 
@@ -263,7 +261,7 @@ definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
    intros;
    whd;
    intro;
-   auto
+   autobatch
  ].
 qed.
 
@@ -303,7 +301,7 @@ theorem impl_trans: transitive ? impl.
  whd;
  unfold impl;
  intros;
- auto.
+ autobatch.
 qed.
 
 (*DA PORTARE: Add Relation Prop impl
@@ -612,26 +610,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 +719,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 +730,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 +782,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 +970,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.
 
 *)