From 648f1521fa36f3c19cca3b3a29bbf3e8146eca4e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 10 Oct 2006 13:10:08 +0000 Subject: [PATCH] auto => auto new added depth=4 to some file in order to make it pass --- matita/contribs/RELATIONAL/NLE/dec.ma | 6 +++--- matita/contribs/RELATIONAL/NLE/fwd.ma | 10 +++++----- matita/contribs/RELATIONAL/NLE/props.ma | 10 +++++----- matita/contribs/RELATIONAL/NPlus/fwd.ma | 20 ++++++++++---------- matita/contribs/RELATIONAL/NPlus/props.ma | 16 ++++++++-------- 5 files changed, 31 insertions(+), 31 deletions(-) diff --git a/matita/contribs/RELATIONAL/NLE/dec.ma b/matita/contribs/RELATIONAL/NLE/dec.ma index 436dc7e62..3b4e0203a 100644 --- 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 6a78e0aac..7d8a9e3b3 100644 --- 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 8745e160e..066e056e0 100644 --- 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 b1f7f2ca3..ffb832450 100644 --- 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 5e7cc1b7f..0c3379f62 100644 --- 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. -- 2.39.2