auto => auto new everywhere + minor updates to make more tests pass

diff --git a/matita/tests/bad_tests/auto.ma b/matita/tests/bad_tests/auto.ma
index 12fa478bbcf1934296a7047ca8a126d68f3355b0..24226600c6669657629fb9afdd9a274034d72bcb 100755 (executable)
--- a/matita/tests/bad_tests/auto.ma
+++ b/matita/tests/bad_tests/auto.ma
@@ -24,4 +24,4 @@ alias symbol "plus" (instance 0) = "Coq's natural plus".
 alias symbol "times" (instance 0) = "Coq's natural times".
 theorem a : \forall x,y:nat. x*x+(S y) = O - x.
 intros.
-auto depth = 4 width = 3 use_paramod = false.
+auto new depth = 4 width = 3 use_paramod = false.

diff --git a/matita/tests/coercions.ma b/matita/tests/coercions.ma
index 1d841d16ebc2f3cad7299d9ec30cf9198ffa81c8..8e7582a147113a99b67e93e6bf484fe2865efb26 100644 (file)
--- a/matita/tests/coercions.ma
+++ b/matita/tests/coercions.ma
@@ -59,10 +59,14 @@ definition double2:
 \def 
   \lambda f:int \to int. \lambda x : pos .f (nat2int (pos2nat x)).
 
+(* This used to test eq_f as a coercion. However, posing both eq_f and sym_eq
+   as coercions made the qed time of some TPTP problems reach infty.
+   Thus eq_f is no longer a coercion (nor is sym_eq).
 theorem coercion_svelta : \forall T,S:Type.\forall f:T \to S.\forall x,y:T.x=y \to f y = f x.
   intros.
   apply ((\lambda h:f y = f x.h) H).
 qed.
+*)
 
 variant pos2nat' : ? \def pos2nat.
 

diff --git a/matita/tests/demodulation_coq.ma b/matita/tests/demodulation_coq.ma
index aa9d5f185369a04e4c94b9d1795c81070649ef69..57fccac5da2bddc1f1f5e95bfec41a98e840d303 100644 (file)
--- a/matita/tests/demodulation_coq.ma
+++ b/matita/tests/demodulation_coq.ma
@@ -22,10 +22,11 @@ alias symbol "plus" = "Coq's natural plus".
 alias symbol "eq" = "Coq's leibnitz's equality".
 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
-
+alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
 
 theorem p0 : \forall m:nat. m+O = m.
-intro. demodulate.
+intro. demodulate.reflexivity.
+qed.
 
 theorem p: \forall m.1*m = m.
 intros.demodulate.reflexivity.

diff --git a/matita/tests/elim.ma b/matita/tests/elim.ma
index 67d7fada10a01b0ac27c98625c1d6770127c4c99..4681d83597a0de52fde58a85dcde4da2b859e372 100644 (file)
--- a/matita/tests/elim.ma
+++ b/matita/tests/elim.ma
@@ -76,5 +76,5 @@ theorem t': \forall x,y. \forall H: sum x y O.
  simplify. intros.
  generalize in match H1.
  rewrite < H2; rewrite < H3.intro.
- rewrite > H4.auto.
+ rewrite > H4.auto new.
 qed.

diff --git a/matita/tests/fguidi.ma b/matita/tests/fguidi.ma
index c6eb2a9d860585466af29e3811e6d409cd16bafb..44e344ab202f65be837bb0bb2826b30f8a221e12 100644 (file)
--- a/matita/tests/fguidi.ma
+++ b/matita/tests/fguidi.ma
@@ -42,11 +42,11 @@ definition pred: nat \to nat \def
       ]. 
 
 theorem eq_gen_S_O: \forall x. (S x = O) \to \forall P:Prop. P.
-intros. apply False_ind. cut (is_S O). auto paramodulation. elim H. exact I.
+intros. apply False_ind. cut (is_S O). auto new. elim H. exact I.
 qed.
 
 theorem eq_gen_S_O_cc: (\forall P:Prop. P) \to \forall x. (S x = O).
-intros. auto.
+intros. auto new.
 qed.
 
 theorem eq_gen_S_S: \forall m,n. (S m) = (S n) \to m = n. 
@@ -83,7 +83,7 @@ theorem le_gen_S_x_aux: \forall m,x,y. (le y x) \to (y = S m) \to
                         (\exists n. x = (S n) \land (le m n)).
 intros 4. elim H. 
 apply eq_gen_S_O. exact m. elim H1. auto paramodulation.
-cut (n = m). elim Hcut. apply ex_intro. exact n1. auto paramodulation. auto. (* paramodulation non trova la prova *)
+cut (n = m). elim Hcut. apply ex_intro. exact n1. auto paramodulation. auto new. (* paramodulation non trova la prova *)
 qed.
 
 theorem le_gen_S_x: \forall m,x. (le (S m) x) \to 

diff --git a/matita/tests/hard_refine.ma b/matita/tests/hard_refine.ma
index b528414df502b68b3d423c4dbfa501996a744c1d..1b194559c28b97918b8d184c57027f1aab23c9e9 100644 (file)
--- a/matita/tests/hard_refine.ma
+++ b/matita/tests/hard_refine.ma
@@ -52,16 +52,16 @@ letin k3 \def (eq_ind_r A (add (multiply ? (inverse ?)) (multiply b n1)) (\lambd
 focus 633. clearbody k3.
 exact
 (eq_ind A b (\lambda x:A.(eq A x b)) (refl_equal A b) (add (multiply a b) b) (eq_ind A (multiply b n1) (\lambda x:A.(eq A x (add (multiply a b) b))) (eq_ind_r A (add a n1) (\lambda x:A.(eq A (multiply b x) (add (multiply a b) b))) (eq_ind_r A (multiply n1 b) (\lambda x:A.(eq A (multiply b (add a n1)) (add (multiply a b) x))) (H5 b a n1) b (eq_ind A (multiply b n1) (\lambda x:A.(eq A b (multiply n1 x))) (eq_ind A (multiply b n1) (\lambda x:A.(eq A x (multiply n1 (multiply b n1)))) (eq_ind_r A (add b b) (\lambda x:A.(eq A (multiply b n1) (multiply n1 x))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b x) (multiply n1 (add b b)))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b (add n1 n1)) (multiply x (add b b)))) (eq_ind_r A (add (multiply b (add n1 n1)) (multiply b (add n1 n1))) (\lambda x:A.(eq A (multiply b (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (multiply b (add n1 n1)) (add (multiply b (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A x (add (multiply b (add n1 n1)) (add (multiply n1 b) (multiply n1 b))))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (add (multiply n1 b) (multiply n1 b)) (add x (add (multiply n1 b) (multiply n1 b))))) (eq_ind A (multiply (add (multiply n1 b) (multiply n1 b)) n1) (\lambda x:A.(eq A x (add (add (multiply n1 b) (multiply n1 b)) (add (multiply n1 b) (multiply n1 b))))) (H7 (multiply n1 b)) (add (multiply n1 b) (multiply n1 b)) (H8 (multiply n1 b))) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply (add n1 n1) (add b b)) (H5 (add n1 n1) b b)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) (multiply b n1) (eq_ind_r A (multiply n1 (add b b)) (\lambda x:A.(eq A x (add b b))) (eq_ind A (multiply (add b b) n1) (\lambda x:A.(eq A (multiply n1 (add b b)) x)) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply n1 (add b b)) (multiply (add b b) x))) (eq_ind_r A (add (multiply n1 (add b b)) (multiply n1 (add b b))) (\lambda x:A.(eq A (multiply n1 (add b b)) x)) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A (multiply n1 (add b b)) (add (multiply n1 (add b b)) x))) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A x (add (multiply n1 (add b b)) (add (multiply b n1) (multiply b n1))))) (eq_ind_r A (add (multiply b n1) (multiply b n1)) (\lambda x:A.(eq A (add (multiply b n1) (multiply b n1)) (add x (add (multiply b n1) (multiply b n1))))) (eq_ind A (multiply (add (multiply b n1) (multiply b n1)) n1) (\lambda x:A.(eq A x (add (add (multiply b n1) (multiply b n1)) (add (multiply b n1) (multiply b n1))))) (H7 (multiply b n1)) (add (multiply b n1) (multiply b n1)) (H8 (multiply b n1))) (multiply n1 (add b b)) (H5 n1 b b)) (multiply n1 (add b b)) (H5 n1 b b)) (multiply n1 (add b b)) (H5 n1 b b)) (multiply (add b b) (add n1 n1)) (H5 (add b b) n1 n1)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) (add b b) (H8 b)) (multiply b n1) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b x) (multiply n1 (add b b)))) (eq_ind A (add n1 n1) (\lambda x:A.(eq A (multiply b (add n1 n1)) (multiply x (add b b)))) (eq_ind_r A (add (multiply b (add n1 n1)) (multiply b (add n1 n1))) (\lambda x:A.(eq A (multiply b (add n1 n1)) x)) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (multiply b (add n1 n1)) (add (multiply b (add n1 n1)) x))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A x (add (multiply b (add n1 n1)) (add (multiply n1 b) (multiply n1 b))))) (eq_ind_r A (add (multiply n1 b) (multiply n1 b)) (\lambda x:A.(eq A (add (multiply n1 b) (multiply n1 b)) (add x (add (multiply n1 b) (multiply n1 b))))) (eq_ind A (multiply (add (multiply n1 b) (multiply n1 b)) n1) (\lambda x:A.(eq A x (add (add (multiply n1 b) (multiply n1 b)) (add (multiply n1 b) (multiply n1 b))))) (H7 (multiply n1 b)) (add (multiply n1 b) (multiply n1 b)) (H8 (multiply n1 b))) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply b (add n1 n1)) (H5 b n1 n1)) (multiply (add n1 n1) (add b b)) (H5 (add n1 n1) b b)) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))) n1 (eq_ind A (multiply (add n1 n1) n1) (\lambda x:A.(eq A x n1)) (H6 n1 n1) (add n1 n1) (H8 n1))))) b ?) b ?)) n1 ?) b ?)).
-auto.
-auto.
-auto.
-auto.
+auto new.
+auto new.
+auto new.
+auto new.
 unfocus.
-auto.
+auto new.
 unfocus.
-auto.
+auto new.
 unfocus.
-auto.
+auto new.
 unfocus.
-auto.
+auto new.
 qed.

diff --git a/matita/tests/inversion.ma b/matita/tests/inversion.ma
index 3e49e06685d22818abd961fec9774f7708b4ab79..35963ab7392bf2b99fba801b6fb3ebf54795fc42 100644 (file)
--- a/matita/tests/inversion.ma
+++ b/matita/tests/inversion.ma
@@ -42,7 +42,7 @@ theorem t: \forall x,y. \forall H: sum x y O.
  simplify. intros.
  generalize in match H1.
  rewrite < H2; rewrite < H3.intro.
- rewrite > H4.auto.
+ rewrite > H4.auto new.
 qed.
 
 theorem t1: \forall x,y. sum x y O \to x = y.
@@ -57,5 +57,5 @@ apply (sum_ind ? (\lambda a,b,K. y=a \to O=b \to x=a) ? ? ? s).*)
 inversion s.
 intros.simplify.
 intros.
-rewrite > H. rewrite < H2.  auto.
+rewrite > H. rewrite < H2.  auto new.
 qed.

diff --git a/matita/tests/inversion2.ma b/matita/tests/inversion2.ma
index f3bc943aa230c491f3d11e84f0c4c65f7b31fc08..5fc9c93350c857d1c553cc844a9debcb200cff67 100644 (file)
--- a/matita/tests/inversion2.ma
+++ b/matita/tests/inversion2.ma
@@ -59,5 +59,5 @@ theorem test_inversion: \forall n. le n O \to n=O.
   (* elim H. BUG DI UNSHARING *)
   (*apply (ledx_ind (\lambda x.\lambda y.  n=x \to O=y \to x=y) ? ? ? ? H).*)
     simplify. intros. reflexivity.    
-    simplify. intros. discriminate H3.
+    simplify. intros. destruct H3.
 qed.

diff --git a/matita/tests/naiveparamod.ma b/matita/tests/naiveparamod.ma
index 37011c733e4fb9486e3ec161b7d0635a27d405c9..7a3e3914ed980427f7d58e5c5ba701d631afba11 100644 (file)
--- a/matita/tests/naiveparamod.ma
+++ b/matita/tests/naiveparamod.ma
@@ -30,7 +30,7 @@ theorem prova1:
   C.
   intros (A B C S a w h b wb).
   (* exact (h s (a b) b wb II). *)
-  auto width = 5 depth = 3. (* look at h parameters! *)
+  auto new width = 5 depth = 3. (* look at h parameters! *)
   qed.
   
 (* c'e' qualcosa di imperativo, se si cambia l'rdine delle ipotesi poi sclera *)

diff --git a/matita/tests/paramodulation/BOO075-1.ma b/matita/tests/paramodulation/BOO075-1.ma
index 8368263d26632ab2839a0028d4c8b2fb952b5e68..f5cfc7c31c45c37dd0df4c6ada0081e3c14d507e 100644 (file)
--- a/matita/tests/paramodulation/BOO075-1.ma
+++ b/matita/tests/paramodulation/BOO075-1.ma
@@ -82,4 +82,4 @@ auto paramodulation timeout=600.
 try assumption.
 print proofterm.
 qed.
-(* -------------------------------------------------------------------------- *)
\ No newline at end of file
+(* -------------------------------------------------------------------------- *)

diff --git a/matita/tests/paramodulation/irratsqrt2.ma b/matita/tests/paramodulation/irratsqrt2.ma
index 0eac7556ec7de46508cf388481a375107dc8fae9..b19984d7dfa214912573ba013d85361dff4f99ad 100644 (file)
--- a/matita/tests/paramodulation/irratsqrt2.ma
+++ b/matita/tests/paramodulation/irratsqrt2.ma
@@ -25,14 +25,14 @@ theorem prova :
   \forall H1: \forall x.P x \to O = x.
    O = S (S (S (S (S O)))).
    intros.
-   auto.
+   auto new.
  qed.
  
 theorem example2:
 \forall x: nat. (x+S O)*(x-S O) = x*x - S O.
 intro;
 apply (nat_case x);
- [ auto timeout = 1.|intro.auto timeout = 1.]
+ [ auto new timeout = 1.|intro.auto new timeout = 1.]
 qed.
 
 theorem irratsqrt2_byhand:
@@ -55,7 +55,7 @@ theorem irratsqrt2_byhand:
   two = o.
   intros.
   cut (divides two a);
-    [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.auto.]
+    [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.auto new.]
     |elim (H6 ? ? Hcut).
      cut (divides two b);
        [ apply (H10 ? Hcut Hcut1).
@@ -89,7 +89,7 @@ theorem irratsqrt2_byhand':
   two = o.
   intros.
   cut (divides two a);
-    [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.auto.]
+    [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.auto new.]
     |(*elim (H6 ? ? Hcut). *)
      cut (divides two b);
        [ apply (H10 ? Hcut Hcut1).
@@ -126,7 +126,7 @@ theorem irratsqrt2:
   \forall H6:\forall x.divides x a \to divides x b \to x = o.
   two = o.
 intros.
-auto depth = 5 timeout = 180.
+auto new depth = 5 timeout = 180.
 qed.
 
 (* time: 146s *)
@@ -136,19 +136,19 @@ qed.
 
   cut (divides two a);[|
     (* apply H8;apply (H7 two (m a a) (m b b));symmetry;assumption. *)
-    auto depth = 4 width = 3 use_paramod = false. ]
-  (*auto depth = 5.*)
+    auto new depth = 4 width = 3 use_paramod = false. ]
+  (*auto new depth = 5.*)
   
   apply H10;
   [ assumption.
-  |(*auto depth = 4.*) apply H8;   
-         (*auto.*)
+  |(*auto new depth = 4.*) apply H8;   
+         (*auto new.*)
          apply (H7 ? ? (m (f two a) (f two a)));
          apply (H5 two ? ?);
          cut ((\lambda x:A.m x (m two ?)=m x (m b b))?);
          [|||simplify;
          auto paramodulation.
-         (*auto.*)
+         (*auto new.*)
          rewrite < H9.
          rewrite < (H6 two a Hcut) in \vdash (? ? ? %).
          rewrite < H2.apply eq_f.

diff --git a/matita/tests/replace.ma b/matita/tests/replace.ma
index 2b174af6478ff4917ac71137a11cc104af6c5d8b..e9960a507de28d4ee7e3dcb344e2b2e373df12d4 100644 (file)
--- a/matita/tests/replace.ma
+++ b/matita/tests/replace.ma
@@ -30,7 +30,7 @@ theorem t: \forall x:nat. x * (x + 0) = (0 + x) * (x + x * 0).
  rewrite < (plus_n_O x).
  reflexivity.
  reflexivity.
- auto.
+ auto new.
 qed.
 
 (* This test tests "replace in match t" where t contains some metavariables *)

diff --git a/matita/tests/test3.ma b/matita/tests/test3.ma
index cdf54906d1937e4cc0c309886bfdb480af80dfca..1399f8be20e745f5d45629f694392c7b7da8f6af 100644 (file)
--- a/matita/tests/test3.ma
+++ b/matita/tests/test3.ma
@@ -27,5 +27,5 @@ alias symbol "times" (instance 0) = "Coq's natural times".
 
 theorem b:\forall p:nat. p * 0=0.
 intro.
-auto.
+auto new.
 qed.