From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 9 Oct 2006 15:33:47 +0000 (+0000)
Subject: auto => auto new everywhere + minor updates to make more tests pass
X-Git-Tag: 0.4.95@7852~921
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3ee4674162a39cb65b08d492278738008057566d;p=helm.git

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 12fa478bb..24226600c 100755
--- 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 1d841d16e..8e7582a14 100644
--- 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 aa9d5f185..57fccac5d 100644
--- 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 67d7fada1..4681d8359 100644
--- 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 c6eb2a9d8..44e344ab2 100644
--- 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 b528414df..1b194559c 100644
--- 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 3e49e0668..35963ab73 100644
--- 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 f3bc943aa..5fc9c9335 100644
--- 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 37011c733..7a3e3914e 100644
--- 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 8368263d2..f5cfc7c31 100644
--- 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 0eac7556e..b19984d7d 100644
--- 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 2b174af64..e9960a507 100644
--- 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 cdf54906d..1399f8be2 100644
--- 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.