From 890f733dd3d1144de1c697a689ea165dc2adcc20 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 26 Oct 2006 11:31:22 +0000 Subject: [PATCH] More timeout added to autos here and there. --- .../matita/contribs/CoRN/algebra/Setoids.ma | 2 +- .../contribs/PREDICATIVE-TOPOLOGY/class_eq.ma | 4 ++-- .../matita/contribs/RELATIONAL/NLE/dec.ma | 6 +++--- .../matita/contribs/RELATIONAL/NLE/props.ma | 10 +++++----- .../matita/contribs/RELATIONAL/NPlus/props.ma | 16 ++++++++-------- 5 files changed, 19 insertions(+), 19 deletions(-) diff --git a/helm/software/matita/contribs/CoRN/algebra/Setoids.ma b/helm/software/matita/contribs/CoRN/algebra/Setoids.ma index 6b7bf781d..5fc3725cc 100644 --- a/helm/software/matita/contribs/CoRN/algebra/Setoids.ma +++ b/helm/software/matita/contribs/CoRN/algebra/Setoids.ma @@ -1248,7 +1248,7 @@ apply f. apply n1. apply m1. apply eq_symmetric_unfolded.assumption. apply eq_symmetric_unfolded.assumption. apply H. -auto new. +auto new timeout=100. qed. (* diff --git a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma index be5f789a3..b86e5f296 100644 --- a/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma +++ b/helm/software/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma @@ -23,10 +23,10 @@ theorem ceq_trans: \forall C. \xforall c1,c2. ceq C c1 c2 \to intros. (* -apply ceq_intro; apply cle_trans; [|auto new|auto new||auto new|auto new]. +apply ceq_intro; apply cle_trans; [|auto new timeout=100|auto new timeout=100||auto new timeout=100|auto new timeout=100]. qed. theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1. -intros; elim H; clear H.; auto new. +intros; elim H; clear H.; auto new timeout=100. qed. *) diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/dec.ma b/helm/software/matita/contribs/RELATIONAL/NLE/dec.ma index 3b4e0203a..7c45ab488 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/dec.ma +++ b/helm/software/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 new + [ auto new timeout=100 | decompose; [ lapply linear nle_gen_succ_1 to H1. decompose. - subst. auto new depth=4 + subst. auto new timeout=100 depth=4 | lapply linear nle_lt_or_eq to H1; decompose; - subst; auto new + subst; auto new timeout=100 ] ]. qed. diff --git a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma index 066e056e0..bd76c2754 100644 --- a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma +++ b/helm/software/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 new. + intros 1; elim x; clear x; intros; auto new timeout=100. qed. theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y. - intros. elim H; clear H x y; intros; auto new. + intros. elim H; clear H x y; intros; auto new timeout=100. 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 new + [ lapply linear nle_gen_zero_2 to H. auto new timeout=100 | lapply linear nle_gen_succ_2 to H1. decompose; - [ subst. auto new + [ subst. auto new timeout=100 | lapply linear H to H3 as H0. decompose; - subst; auto new + subst; auto new timeout=100 ] ]. qed. diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma index 0c3379f62..2c908d1d0 100644 --- a/helm/software/matita/contribs/RELATIONAL/NPlus/props.ma +++ b/helm/software/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 new. + intros. elim q; clear q; auto new timeout=100. 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 new. + ]; auto new timeout=100. 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 new. + ]; auto new timeout=100. 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 new. + decompose. subst. auto new timeout=100. 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 new. + decompose. subst. auto new timeout=100. 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 new || auto new ]. (**) + ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**) 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 new || auto new ]. (**) + ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**) 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 new. + ]; auto new timeout=100. qed. -- 2.39.2