X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=d9fd301fcf2e9f075596c455a20e72db2a2d4c6b;hb=8ef11a4b981e6da3d60f353386b17f7692dc0ecd;hp=362b9fb5b740abc924761aa1159b3ebbb12ad640;hpb=9fe4caa4ba466250017b5ac1b36fc6e94d7e3860;p=helm.git

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index 362b9fb5b..d9fd301fc 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 *)
 
@@ -209,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.
 
@@ -227,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.
 
@@ -244,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.
 
@@ -261,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.
 
@@ -301,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
@@ -970,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.
 
 *)