auto => auto new

added depth=4 to some file in order to make it pass

diff --git a/matita/contribs/RELATIONAL/NLE/dec.ma b/matita/contribs/RELATIONAL/NLE/dec.ma
index 436dc7e62788ed5df336ef849fc223889a037e33..3b4e0203a9effc42642bc2bbfa8ff55b388390bf 100644 (file)
--- a/matita/contribs/RELATIONAL/NLE/dec.ma
+++ b/matita/contribs/RELATIONAL/NLE/dec.ma
@@ -18,12 +18,12 @@ include "NLE/props.ma".
 
 theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x.
  intros 2; elim y; clear y;
- [ auto
+ [ auto new
  | decompose;
    [ lapply linear nle_gen_succ_1 to H1. decompose.
-     subst. auto
+     subst. auto new depth=4
    | lapply linear nle_lt_or_eq to H1; decompose;
-     subst; auto
+     subst; auto new
    ]
  ].
 qed.

diff --git a/matita/contribs/RELATIONAL/NLE/fwd.ma b/matita/contribs/RELATIONAL/NLE/fwd.ma
index 6a78e0aac788bce7a77661c3bc93b213fec70b3b..7d8a9e3b3528b127769d3d9e130401baf3453554 100644 (file)
--- a/matita/contribs/RELATIONAL/NLE/fwd.ma
+++ b/matita/contribs/RELATIONAL/NLE/fwd.ma
@@ -25,7 +25,7 @@ theorem nle_gen_succ_1: \forall x,y. x < y \to
  [ apply (eq_gen_succ_zero ? ? H)
  | lapply linear eq_gen_succ_succ to H2 as H0.
    subst.
-   apply ex_intro; [|auto] (**)
+   apply ex_intro; [|auto new] (**)
  ].
 qed.
 
@@ -34,7 +34,7 @@ theorem nle_gen_succ_succ: \forall x,y. x < succ y \to x <= y.
  [ apply (eq_gen_succ_zero ? ? H)
  | lapply linear eq_gen_succ_succ to H2 as H0.
    lapply linear eq_gen_succ_succ to H3 as H2.
-   subst. auto
+   subst. auto new
  ].
 qed.
 
@@ -46,7 +46,7 @@ qed.
 
 theorem nle_gen_zero_2: \forall x. x <= zero \to x = zero.
  intros 1. elim x; clear x; intros;
- [ auto
+ [ auto new
  | apply (nle_gen_succ_zero ? ? H1)
  ].
 qed.
@@ -54,8 +54,8 @@ qed.
 theorem nle_gen_succ_2: \forall y,x. x <= succ y \to
                         x = zero \lor \exists z. x = succ z \land z <= y.
  intros 2; elim x; clear x; intros;
- [ auto
+ [ auto new
  | lapply linear nle_gen_succ_succ to H1.
-   right. apply ex_intro; [|auto] (**)
+   right. apply ex_intro; [|auto new] (**)
  ].
 qed.

diff --git a/matita/contribs/RELATIONAL/NLE/props.ma b/matita/contribs/RELATIONAL/NLE/props.ma
index 8745e160e4b94c6ae1e5e4d6565839a38f634732..066e056e0435f74c01f0dc43970bbce5a2575994 100644 (file)
--- a/matita/contribs/RELATIONAL/NLE/props.ma
+++ b/matita/contribs/RELATIONAL/NLE/props.ma
@@ -17,20 +17,20 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/props".
 include "NLE/fwd.ma".
 
 theorem nle_refl: \forall x. x <= x.
- intros 1; elim x; clear x; intros; auto.
+ intros 1; elim x; clear x; intros; auto new.
 qed.
 
 theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y.
- intros. elim H; clear H x y; intros; auto.
+ intros. elim H; clear H x y; intros; auto new.
 qed.
 
 theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y.
  intros 1. elim y; clear y; intros;
- [ lapply linear nle_gen_zero_2 to H. auto
+ [ lapply linear nle_gen_zero_2 to H. auto new
  | lapply linear nle_gen_succ_2 to H1. decompose;
-   [ subst. auto
+   [ subst. auto new
    | lapply linear H to H3 as H0. decompose;
-     subst; auto
+     subst; auto new
    ]
  ].
 qed.

diff --git a/matita/contribs/RELATIONAL/NPlus/fwd.ma b/matita/contribs/RELATIONAL/NPlus/fwd.ma
index b1f7f2ca303b92653a4adc47d87d607264b04fa4..ffb83245019fb19a92961cda2dd109b99f885f5f 100644 (file)
--- a/matita/contribs/RELATIONAL/NPlus/fwd.ma
+++ b/matita/contribs/RELATIONAL/NPlus/fwd.ma
@@ -22,7 +22,7 @@ include "NPlus/defs.ma".
 theorem nplus_gen_zero_1: \forall q,r. (zero + q == r) \to q = r.
  intros. elim H; clear H q r; intros;
  [ reflexivity
- | clear H1. auto
+ | clear H1. auto new
  ].
 qed.
 
@@ -33,12 +33,12 @@ theorem nplus_gen_succ_1: \forall p,q,r. ((succ p) + q == r) \to
  | clear H1.
    decompose.
    subst.
- ]; apply ex_intro; [| auto || auto ]. (**)
+ ]; apply ex_intro; [| auto new || auto new ]. (**)
 qed.
 
 theorem nplus_gen_zero_2: \forall p,r. (p + zero == r) \to p = r.
  intros. inversion H; clear H; intros;
- [ auto
+ [ auto new
  | clear H H1.
    lapply eq_gen_zero_succ to H2 as H0. apply H0
  ].
@@ -51,14 +51,14 @@ theorem nplus_gen_succ_2: \forall p,q,r. (p + (succ q) == r) \to
  | clear H1 H3 r.
    lapply linear eq_gen_succ_succ to H2 as H0.
    subst.
-   apply ex_intro; [| auto ] (**)
+   apply ex_intro; [| auto new ] (**)
  ].
 qed.
 
 theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to 
                           p = zero \land q = zero.
  intros. inversion H; clear H; intros;
- [ subst. auto
+ [ subst. auto new
  | clear H H1.
    lapply eq_gen_zero_succ to H3 as H0. apply H0
  ].
@@ -72,7 +72,7 @@ theorem nplus_gen_succ_3: \forall p,q,r. (p + q == (succ r)) \to
  | clear H1.
    lapply linear eq_gen_succ_succ to H3 as H0.
    subst.
- ]; apply ex_intro; [| auto || auto ] (**)
+ ]; apply ex_intro; [| auto new || auto new ] (**)
 qed.
 (*
 (* alternative proofs invoking nplus_gen_2 *)
@@ -81,7 +81,7 @@ variant nplus_gen_zero_3_alt: \forall p,q. (p + q == zero) \to
                               p = zero \land q = zero.
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
-   subst. auto
+   subst. auto new
  | clear H.
    lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
@@ -100,7 +100,7 @@ variant nplus_gen_succ_3_alt: \forall p,q,r. (p + q == (succ r)) \to
    decompose.
    lapply linear eq_gen_succ_succ to H1 as H0.
    subst
- ]; apply ex_intro; [| auto || auto ]. (**)
+ ]; apply ex_intro; [| auto new || auto new ]. (**)
 qed.
 *)
 (* other simplification lemmas *)
@@ -113,7 +113,7 @@ theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
    decompose.
    lapply linear eq_gen_succ_succ to H2 as H0.
    subst
- ]; auto.
+ ]; auto new.
 qed.
 
 theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
@@ -124,5 +124,5 @@ theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
    decompose.
    lapply linear eq_gen_succ_succ to H2 as H0.
    subst
- ]; auto.
+ ]; auto new.
 qed.

diff --git a/matita/contribs/RELATIONAL/NPlus/props.ma b/matita/contribs/RELATIONAL/NPlus/props.ma
index 5e7cc1b7f592c8bca10f3516ad9d1398cf4fb5c3..0c3379f624d6a1d8ec2f0f0ba5a4b1e608b3f1ad 100644 (file)
--- a/matita/contribs/RELATIONAL/NPlus/props.ma
+++ b/matita/contribs/RELATIONAL/NPlus/props.ma
@@ -17,7 +17,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/props".
 include "NPlus/fwd.ma".
 
 theorem nplus_zero_1: \forall q. zero + q == q.
- intros. elim q; clear q; auto.
+ intros. elim q; clear q; auto new.
 qed.
 
 theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to 
@@ -28,7 +28,7 @@ theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to
  | lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
    subst
- ]; auto.
+ ]; auto new.
 qed.
 
 theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r.
@@ -38,21 +38,21 @@ theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r.
  | lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
    subst
- ]; auto.
+ ]; auto new.
 qed.
 
 theorem nplus_shift_succ_sx: \forall p,q,r. 
                              (p + (succ q) == r) \to (succ p) + q == r.
  intros.
  lapply linear nplus_gen_succ_2 to H as H0.
- decompose. subst. auto.
+ decompose. subst. auto new.
 qed.
 
 theorem nplus_shift_succ_dx: \forall p,q,r. 
                              ((succ p) + q == r) \to p + (succ q) == r.
  intros.
  lapply linear nplus_gen_succ_1 to H as H0.
- decompose. subst. auto.
+ decompose. subst. auto new.
 qed.
 
 theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to 
@@ -67,7 +67,7 @@ theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to
    decompose. subst.
    lapply linear H to H4, H3 as H0.
    decompose.
- ]; apply ex_intro; [| auto || auto ]. (**)
+ ]; apply ex_intro; [| auto new || auto new ]. (**)
 qed.
 
 theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to 
@@ -82,7 +82,7 @@ theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to
    decompose. subst.
    lapply linear H to H4, H3 as H0.
    decompose.
- ]; apply ex_intro; [| auto || auto ]. (**)
+ ]; apply ex_intro; [| auto new || auto new ]. (**)
 qed.
 
 theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to 
@@ -94,5 +94,5 @@ theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to
    decompose. subst.
    lapply linear nplus_gen_succ_2 to H2 as H0.
    decompose. subst.
- ]; auto.
+ ]; auto new.
 qed.