From cf5540f056d6d4fa1612e08d41253d1d009f5d44 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 7 Nov 2007 19:52:14 +0000 Subject: [PATCH] - bug fix in destruct - old subst tactic removed - some tests fixed --- components/tactics/Makefile | 3 +- components/tactics/destructTactic.ml | 73 ++++--------------- components/tactics/tactics.mli | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma | 19 +++++ matita/contribs/LOGIC/Insert/fun.ma | 4 +- matita/contribs/LOGIC/Insert/inv.ma | 12 +-- matita/contribs/LOGIC/Insert/props.ma | 20 ++--- matita/contribs/LOGIC/NTrack/inv.ma | 16 ++-- matita/contribs/LOGIC/NTrack/props.ma | 18 ++--- matita/contribs/LOGIC/Track/inv.ma | 12 +-- matita/contribs/LOGIC/Track/pred.ma | 26 +++---- matita/contribs/RELATIONAL/NLE/inv.ma | 10 +-- matita/contribs/RELATIONAL/NLE/order.ma | 4 +- matita/contribs/RELATIONAL/NLE/props.ma | 2 +- matita/contribs/RELATIONAL/NPlus/fun.ma | 2 +- matita/contribs/RELATIONAL/NPlus/inv.ma | 14 ++-- matita/contribs/RELATIONAL/NPlus/monoid.ma | 38 +++++----- matita/contribs/RELATIONAL/NPlusList/props.ma | 2 +- matita/contribs/RELATIONAL/ZEq/setoid.ma | 2 +- matita/tests/dependent_injection.ma | 2 +- matita/tests/injection.ma | 8 +- 21 files changed, 130 insertions(+), 159 deletions(-) diff --git a/components/tactics/Makefile b/components/tactics/Makefile index 9a6c6d4d0..7c9f00db5 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -33,12 +33,11 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) all: # we omit dependencies since it is a pain when distributing -tactics_mli_deps=tactics.ml *Tactics.mli *Tactic.mli fourierR.mli ring.mli paramodulation/indexing.mli +tactics_mli_deps = tactics.ml *Tactics.mli *Tactic.mli fourierR.mli ring.mli paramodulation/indexing.mli tactics.mli: tactics.ml $(H)echo " OCAMLC -i $$(tactics_mli_deps) > $@" $(H)echo "(* GENERATED FILE, DO NOT EDIT. STAMP:`date` *)" > $@ $(H)$(OCAMLC) -I paramodulation -i tactics.ml >> $@ -# FG: tactics.ml was (wrongly) $(tactics_mli_deps) UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions) STR=$(shell $(OCAMLFIND) query str) diff --git a/components/tactics/destructTactic.ml b/components/tactics/destructTactic.ml index bbfee8041..2ea9e047c 100644 --- a/components/tactics/destructTactic.ml +++ b/components/tactics/destructTactic.ml @@ -45,54 +45,6 @@ let debug = true let debug_print = if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ()) -(* funzione generale di rilocazione dei riferimenti locali *) - -let relocate_term map t = - let rec map_xnss k xnss = - let imap (uri, t) = uri, map_term k t in - List.map imap xnss - and map_mss k mss = - let imap = function - | None -> None - | Some t -> Some (map_term k t) - in - List.map imap mss - and map_fs len k fs = - let imap (name, i, ty, bo) = name, i, map_term k ty, map_term (k + len) bo in - List.map imap fs - and map_cfs len k cfs = - let imap (name, ty, bo) = name, map_term k ty, map_term (k + len) bo in - List.map imap cfs - and map_term k = function - | C.Rel m -> if m < k then C.Rel m else C.Rel (map (m - k)) - | C.Sort _ as t -> t - | C.Implicit _ as t -> t - | C.Var (uri, xnss) -> C.Var (uri, map_xnss k xnss) - | C.Const (uri, xnss) -> C.Const (uri, map_xnss k xnss) - | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, map_xnss k xnss) - | C.MutConstruct (uri, tyno, consno, xnss) -> - C.MutConstruct (uri, tyno, consno, map_xnss k xnss) - | C.Meta (i, mss) -> C.Meta(i, map_mss k mss) - | C.Cast (te, ty) -> C.Cast (map_term k te, map_term k ty) - | C.Appl ts -> C.Appl (List.map (map_term k) ts) - | C.MutCase (sp, i, outty, t, pl) -> - C.MutCase (sp, i, map_term k outty, map_term k t, List.map (map_term k) pl) - | C.Prod (n, s, t) -> C.Prod (n, map_term k s, map_term (succ k) t) - | C.Lambda (n, s, t) -> C.Lambda (n, map_term k s, map_term (succ k) t) - | C.LetIn (n, s, t) -> C.LetIn (n, map_term k s, map_term (succ k) t) - | C.Fix (i, fs) -> C.Fix (i, map_fs (List.length fs) k fs) - | C.CoFix (i, cfs) -> C.CoFix (i, map_cfs (List.length cfs) k cfs) - in - map_term 0 t - -let id n = n - -let after continuation aftermap beforemap = - continuation ~map:(fun n -> aftermap (beforemap n)) - -let after2 continuation aftermap beforemap ~map = - continuation ~map:(fun n -> map (aftermap (beforemap n))) - (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori diversi *) @@ -322,7 +274,7 @@ let rec recur_on_child_tac name = let rec search_name i = function | [] -> T.id_tac | Some (Cic.Name n, _) :: _ when n = name -> - destruct ~first_time:false ~term:(Cic.Rel i) + destruct ~first_time:false (Cic.Rel i) | _ :: tl -> search_name (succ i) tl in PET.apply_tactic (search_name 1 context) status @@ -532,10 +484,7 @@ and subst_tac ~lterm ~direction ~where ~continuation = in PET.mk_tactic subst_tac -(* ~term vive nel contesto della tattica una volta ~mappato - * ~continuation riceve la mappa assoluta - *) -and destruct ~first_time ~term = +and destruct ?(simplified = false) ~first_time term = let are_convertible hd1 hd2 metasenv context = fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph) in @@ -625,13 +574,17 @@ and destruct ~first_time ~term = | _, C.Rel i2 when DTI.does_not_occur i2 t1 -> mk_subst_chain `RightToLeft i2 t1 t2 (* else part *) - | _ when not first_time -> T.id_tac - | _ (* when first_time *) -> + | _ when first_time && simplified -> raise exn_nothingtodo + | _ when simplified (* && not first time *) -> T.id_tac + | _ (* when not simplified *) -> T.then_ ~start:(simpl_in_term context term) - ~continuation:(destruct ~first_time:false ~term) + ~continuation:(destruct ~simplified:true ~first_time term) end - | _ when not first_time -> T.id_tac - | _ (* when first_time *) -> raise exn_nothingtodo + | _ when first_time && simplified -> raise exn_nothingtodo + | _ when simplified (* && not first time *) -> T.id_tac + | _ (* when not simplified *) -> + T.then_ ~start:(simpl_in_term context term) + ~continuation:(destruct ~simplified:true ~first_time term) in PET.apply_tactic tac status in @@ -644,7 +597,7 @@ let lazy_destruct_tac ~first_time ~lterm = let _,context,_ = CicUtil.lookup_meta goal metasenv in let term, _, _ = lterm context metasenv CU.empty_ugraph in let tactic = - if exists context term then destruct ~first_time ~term else T.id_tac + if exists context term then destruct ~first_time term else T.id_tac in PET.apply_tactic tactic status in @@ -653,7 +606,7 @@ let lazy_destruct_tac ~first_time ~lterm = (* destruct performs either injection or discriminate *) (* equivalent to Coq's "analyze equality" *) let destruct_tac = function - | Some term -> destruct ~first_time:true ~term + | Some term -> destruct ~first_time:true term | None -> let destruct_all status = let (proof, goal) = status in diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index a58752461..45bfa7e3b 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Nov 6 16:23:06 CET 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Nov 7 13:24:27 CET 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma index 08972e5e9..499cd5fdc 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma @@ -27,6 +27,25 @@ theorem nf2_sort: n) t2)).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (TSort n) t)) (refl_equal T (TSort n)) t2 (pr2_gen_sort c t2 n H))))). +theorem nf2_csort_lref: + \forall (n: nat).(\forall (i: nat).(nf2 (CSort n) (TLRef i))) +\def + \lambda (n: nat).(\lambda (i: nat).(\lambda (t2: T).(\lambda (H: (pr2 (CSort +n) (TLRef i) t2)).(let H0 \def (pr2_gen_lref (CSort n) t2 i H) in (or_ind (eq +T t2 (TLRef i)) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i (CSort n) +(CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift (S +i) O u))))) (eq T (TLRef i) t2) (\lambda (H1: (eq T t2 (TLRef i))).(eq_ind_r +T (TLRef i) (\lambda (t: T).(eq T (TLRef i) t)) (refl_equal T (TLRef i)) t2 +H1)) (\lambda (H1: (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i (CSort +n) (CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift +(S i) O u)))))).(ex2_2_ind C T (\lambda (d: C).(\lambda (u: T).(getl i (CSort +n) (CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift +(S i) O u)))) (eq T (TLRef i) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda +(H2: (getl i (CSort n) (CHead x0 (Bind Abbr) x1))).(\lambda (H3: (eq T t2 +(lift (S i) O x1))).(eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(eq T +(TLRef i) t)) (getl_gen_sort n i (CHead x0 (Bind Abbr) x1) H2 (eq T (TLRef i) +(lift (S i) O x1))) t2 H3))))) H1)) H0))))). + theorem nf2_abst: \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (b: B).(\forall (v: T).(\forall (t: T).((nf2 (CHead c (Bind b) v) t) \to (nf2 c (THead (Bind diff --git a/matita/contribs/LOGIC/Insert/fun.ma b/matita/contribs/LOGIC/Insert/fun.ma index f0cc5e514..7c7aba28a 100644 --- a/matita/contribs/LOGIC/Insert/fun.ma +++ b/matita/contribs/LOGIC/Insert/fun.ma @@ -27,8 +27,8 @@ qed. theorem insert_inj: \forall S1,i,P, Q. Insert S1 i P Q \to \forall S2. Insert S2 i P Q \to S1 = S2. intros 5; elim H; clear H i P Q; - [ lapply linear insert_inv_zero to H1; subst; autobatch - | lapply linear insert_inv_succ to H3; decompose; subst; autobatch + [ lapply linear insert_inv_zero to H1; destruct; autobatch + | lapply linear insert_inv_succ to H3; decompose; destruct; autobatch ]. qed. *) diff --git a/matita/contribs/LOGIC/Insert/inv.ma b/matita/contribs/LOGIC/Insert/inv.ma index b612858a3..9053183f9 100644 --- a/matita/contribs/LOGIC/Insert/inv.ma +++ b/matita/contribs/LOGIC/Insert/inv.ma @@ -20,18 +20,18 @@ set "baseuri" "cic:/matita/LOGIC/Insert/inv". include "Insert/defs.ma". (* theorem insert_inv_zero: \forall S,P,Q. Insert S zero P Q \to Q = abst P S. - intros; inversion H; clear H; intros; subst; autobatch. + intros; inversion H; clear H; intros; destruct; autobatch. qed. theorem insert_inv_succ: \forall S,Q1,Q2,i. Insert S (succ i) Q1 Q2 \to \exists P1,P2,R. Insert S i P1 P2 \land Q1 = abst P1 R \land Q2 = abst P2 R. - intros; inversion H; clear H; intros; subst; autobatch depth = 6 size = 8. + intros; inversion H; clear H; intros; destruct; autobatch depth = 6 size = 8. qed. theorem insert_inv_leaf_1: \forall Q,S,i. Insert S i leaf Q \to i = zero \land Q = S. - intros. inversion H; clear H; intros; subst. autobatch. + intros. inversion H; clear H; intros; destruct. autobatch. qed. theorem insert_inv_abst_1: \forall P,Q,R,S,i. Insert S i (abst P R) Q \to @@ -39,17 +39,17 @@ theorem insert_inv_abst_1: \forall P,Q,R,S,i. Insert S i (abst P R) Q \to \exists n, c1. i = succ n \land Q = abst c1 R \land Insert S n P c1. - intros. inversion H; clear H; intros; subst; autobatch depth = 6 size = 8. + intros. inversion H; clear H; intros; destruct; autobatch depth = 6 size = 8. qed. theorem insert_inv_leaf_2: \forall P,S,i. Insert S i P leaf \to False. - intros. inversion H; clear H; intros; subst. + intros. inversion H; clear H; intros; destruct. qed. theorem insert_inv_abst_2: \forall P,i. \forall R,S:Sequent. Insert S i P R \to i = zero \land P = leaf \land R = S. - intros. inversion H; clear H; intros; subst; + intros. inversion H; clear H; intros; destruct; [ autobatch | clear H1. lapply linear insert_inv_leaf_2 to H. decompose ]. diff --git a/matita/contribs/LOGIC/Insert/props.ma b/matita/contribs/LOGIC/Insert/props.ma index 6daa22ea6..17148e27e 100644 --- a/matita/contribs/LOGIC/Insert/props.ma +++ b/matita/contribs/LOGIC/Insert/props.ma @@ -25,9 +25,9 @@ theorem insert_conf: \forall P,Q1,S1,i1. Insert S1 i1 P Q1 \to Insert S2 j2 Q1 Q \land Insert S1 j1 Q2 Q. intros 5. elim H; clear H i1 P Q1; [ elim H1; clear H1 i2 c Q2; decompose; autobatch depth = 7 size = 8 - | lapply linear insert_inv_abst_1 to H3. decompose; subst; + | lapply linear insert_inv_abst_1 to H3. decompose; destruct; [ autobatch depth = 7 size = 8 - | lapply linear H2 to H4. decompose. subst. autobatch depth = 6 size = 8 + | lapply linear H2 to H4. decompose. destruct. autobatch depth = 6 size = 8 ] ]. qed. @@ -37,10 +37,10 @@ theorem insert_trans: \forall P1,Q1,S1,i1. Insert S1 i1 P1 Q1 \to \exists P2,j1,j2. Insert S2 j2 P1 P2 \land Insert S1 j1 P2 Q2. intros 5. elim H; clear H i1 P1 Q1; - [ lapply linear insert_inv_abst_1 to H1. decompose; subst; autobatch depth = 6 size = 7 - | lapply linear insert_inv_abst_1 to H3. decompose; subst; + [ lapply linear insert_inv_abst_1 to H1. decompose; destruct; autobatch depth = 6 size = 7 + | lapply linear insert_inv_abst_1 to H3. decompose; destruct; [ clear H2. autobatch depth = 7 size = 8 - | lapply linear H2 to H4. decompose. subst. autobatch depth = 6 size = 8 + | lapply linear H2 to H4. decompose. destruct. autobatch depth = 6 size = 8 ] ]. qed. @@ -51,10 +51,10 @@ theorem insert_conf_rev: \forall P1,Q,S1,i1. Insert S1 i1 P1 Q \to \exists Q1,Q2,j1,j2. Insert S2 j2 Q2 P1 \land Insert S1 j1 Q1 P2. intros 5; elim H; clear H i1 P1 Q; - [ inversion H1; clear H1; intros; subst; autobatch depth = 7 size = 8 - | inversion H3; clear H3; intros; subst; + [ inversion H1; clear H1; intros; destruct; autobatch depth = 7 size = 8 + | inversion H3; clear H3; intros; destruct; [ autobatch depth = 7 size = 8 - | clear H3; lapply linear H2 to H; decompose; subst; + | clear H3; lapply linear H2 to H; decompose; destruct; autobatch depth = 8 size = 10 ] ]. @@ -65,8 +65,8 @@ theorem insert_conf_rev_full: \forall P1,Q,S1,i1. Insert S1 i1 P1 Q \to (S1 = S2 \land i1 = i2 \land P1 = P2) \lor \exists Q1,Q2,j1,j2. Insert S2 j2 Q2 P1 \land Insert S1 j1 Q1 P2. - intros; lapply insert_conf_rev to H, H1; decompose; subst; - [ lapply linear insert_inj to H, H1; subst; autobatch depth = 4 + intros; lapply insert_conf_rev to H, H1; decompose; destruct; + [ lapply linear insert_inj to H, H1; destruct; autobatch depth = 4 | autobatch depth = 7 size = 8 ]. qed. diff --git a/matita/contribs/LOGIC/NTrack/inv.ma b/matita/contribs/LOGIC/NTrack/inv.ma index 6c57c2040..f272bd518 100644 --- a/matita/contribs/LOGIC/NTrack/inv.ma +++ b/matita/contribs/LOGIC/NTrack/inv.ma @@ -18,26 +18,26 @@ include "NTrack/defs.ma". (* theorem ntrack_inv_lref: \forall Q,S,i. NTrack Q (lref i) S \to \exists P. Insert S i P Q. - intros; inversion H; clear H; intros; subst; autobatch. + intros; inversion H; clear H; intros; destruct; autobatch. qed. theorem ntrack_inv_parx: \forall P,S,h. NTrack P (parx h) S \to S = pair (posr h) (posr h). - intros; inversion H; clear H; intros; subst; autobatch. + intros; inversion H; clear H; intros; destruct; autobatch. qed. theorem ntrack_inv_impw: \forall P,p,S. NTrack P (impw p) S \to \exists B,a,b. S = pair (impl a b) B \land NTrack P p (pair lleaf B). - intros; inversion H; clear H; intros; subst; autobatch depth = 5. + intros; inversion H; clear H; intros; destruct; autobatch depth = 5. qed. theorem ntrack_inv_impr: \forall P,p,S. NTrack P (impr p) S \to \exists a,b:Formula. S = pair lleaf (impl a b) \land NTrack P p (pair a b). - intros; inversion H; clear H; intros; subst; autobatch depth = 4. + intros; inversion H; clear H; intros; destruct; autobatch depth = 4. qed. theorem ntrack_inv_impi: \forall P,p,q,r,S. NTrack P (impi p q r) S \to @@ -47,20 +47,20 @@ theorem ntrack_inv_impi: \forall P,p,q,r,S. NTrack P (impi p q r) S \to NTrack P q (pair b B) \land NTrack Q r (pair lleaf D) \land Insert (pair A B) i P Q. - intros; inversion H; clear H; intros; subst; autobatch depth = 12 width = 5 size = 16. + intros; inversion H; clear H; intros; destruct; autobatch depth = 12 width = 5 size = 16. qed. theorem ntrack_inv_scut: \forall P,q,r,S. NTrack P (scut q r) S \to False. - intros; inversion H; clear H; intros; subst. + intros; inversion H; clear H; intros; destruct. qed. theorem ntrack_inv_lleaf_impl: \forall Q,p,a,b. NTrack Q p (pair lleaf (impl a b)) \to (\exists P,i. p = lref i \land Insert (pair lleaf (impl a b)) i P Q) \lor (\exists r. p = impr r \land NTrack Q r (pair a b)). - intros; inversion H; clear H; intros; subst; + intros; inversion H; clear H; intros; destruct; [ autobatch depth = 5 - | subst; autobatch depth = 4 + | destruct; autobatch depth = 4 ]. qed. *) diff --git a/matita/contribs/LOGIC/NTrack/props.ma b/matita/contribs/LOGIC/NTrack/props.ma index 7d41aebdf..bdd23748f 100644 --- a/matita/contribs/LOGIC/NTrack/props.ma +++ b/matita/contribs/LOGIC/NTrack/props.ma @@ -24,12 +24,12 @@ theorem ntrack_weak: \forall R,p,P,Q,S,i. intros 2; elim p; clear p; [ lapply linear ntrack_inv_lref to H as H0; decompose; lapply linear insert_trans to H, H1; decompose; autobatch - | lapply linear ntrack_inv_parx to H; subst; autobatch - | lapply linear ntrack_inv_impw to H1; decompose; subst; + | lapply linear ntrack_inv_parx to H; destruct; autobatch + | lapply linear ntrack_inv_impw to H1; decompose; destruct; lapply linear H to H4, H2; decompose; autobatch - | lapply linear ntrack_inv_impr to H1; decompose; subst; + | lapply linear ntrack_inv_impr to H1; decompose; destruct; lapply linear H to H4, H2; decompose; autobatch - | lapply linear ntrack_inv_impi to H3; decompose; subst; + | lapply linear ntrack_inv_impi to H3; decompose; destruct; lapply insert_conf to H4, H6; clear H6; decompose; lapply H to H9, H4; clear H H9; lapply linear H1 to H8, H4; lapply linear H2 to H7, H6; decompose; autobatch width = 4 @@ -42,13 +42,13 @@ theorem ntrack_comp: \forall R,q,p,P,Q,S,i. \exists r. NTrack P r S. intros 2; elim q; clear q; [ lapply linear ntrack_inv_lref to H1 as H0; decompose; - lapply linear insert_conf_rev_full to H1,H2; decompose; subst; autobatch - | lapply linear ntrack_inv_parx to H1; subst; autobatch - | lapply linear ntrack_inv_impw to H2; decompose; subst; + lapply linear insert_conf_rev_full to H1,H2; decompose; destruct; autobatch + | lapply linear ntrack_inv_parx to H1; destruct; autobatch + | lapply linear ntrack_inv_impw to H2; decompose; destruct; lapply linear H to H1, H5, H3; decompose; autobatch - | lapply linear ntrack_inv_impr to H2; decompose; subst; + | lapply linear ntrack_inv_impr to H2; decompose; destruct; lapply linear H to H1, H5, H3; decompose; autobatch - | lapply linear ntrack_inv_impi to H4; decompose; subst; + | lapply linear ntrack_inv_impi to H4; decompose; destruct; lapply insert_trans to H5, H7; clear H7; decompose; lapply ntrack_weak to H3, H6; decompose; lapply H to H3, H10, H5; clear H H10; lapply linear H1 to H3, H9, H5; diff --git a/matita/contribs/LOGIC/Track/inv.ma b/matita/contribs/LOGIC/Track/inv.ma index 77d1107cd..d38d3f120 100644 --- a/matita/contribs/LOGIC/Track/inv.ma +++ b/matita/contribs/LOGIC/Track/inv.ma @@ -20,26 +20,26 @@ include "Track/defs.ma". theorem track_inv_lref: \forall Q,S,i. Track Q (lref i) S \to \exists p1,p2,P. Insert p1 p2 S i P Q. - intros; inversion H; clear H; intros; subst; autobatch depth = 4. + intros; inversion H; clear H; intros; destruct; autobatch depth = 4. qed. theorem track_inv_prin: \forall P,S,h. Track P (prin h) S \to S = pair (posr h) (posr h). - intros; inversion H; clear H; intros; subst; autobatch. + intros; inversion H; clear H; intros; destruct; autobatch. qed. theorem track_inv_impw: \forall P,p,S. Track P (impw p) S \to \exists B,a,b. S = pair (impl a b) B \land Track P p (pair lleaf B). - intros; inversion H; clear H; intros; subst; autobatch depth = 5. + intros; inversion H; clear H; intros; destruct; autobatch depth = 5. qed. theorem track_inv_impr: \forall Q,p,S. Track Q (impr p) S \to \exists a,b:Formula. S = pair lleaf (impl a b) \land Track Q p (pair a b). - intros; inversion H; clear H; intros; subst; autobatch depth = 4. + intros; inversion H; clear H; intros; destruct; autobatch depth = 4. qed. theorem track_inv_impi: \forall P,p,q,r,S. Track P (impi p q r) S \to @@ -48,7 +48,7 @@ theorem track_inv_impi: \forall P,p,q,r,S. Track P (impi p q r) S \to Track P p (pair A a) \land Track P q (pair b B) \land Track (abst P p q (pair A B)) r (pair lleaf D). - intros; inversion H; clear H; intros; subst; autobatch depth = 9 width = 4 size = 12. + intros; inversion H; clear H; intros; destruct; autobatch depth = 9 width = 4 size = 12. qed. theorem track_inv_scut: \forall P,q,r,S. Track P (scut q r) S \to @@ -56,5 +56,5 @@ theorem track_inv_scut: \forall P,q,r,S. Track P (scut q r) S \to S = pair A B \land Track P q (pair A c) \land Track P r (pair c B). - intros; inversion H; clear H; intros; subst; autobatch depth = 6 size = 8. + intros; inversion H; clear H; intros; destruct; autobatch depth = 6 size = 8. qed. diff --git a/matita/contribs/LOGIC/Track/pred.ma b/matita/contribs/LOGIC/Track/pred.ma index f9c172813..c4e65c05d 100644 --- a/matita/contribs/LOGIC/Track/pred.ma +++ b/matita/contribs/LOGIC/Track/pred.ma @@ -24,20 +24,20 @@ theorem track_pred: \forall Q1,Q2,p1,p2,S1,S2. [Q1, p1, S1] => [Q2, p2, S2] \to intros 7; elim H; clear H Q1 Q2 p1 p2 S1 S2; [ autobatch | autobatch - | lapply linear track_inv_impw to H3; decompose; subst; autobatch - | lapply linear track_inv_impr to H3; decompose; subst; autobatch - | lapply linear track_inv_impi to H7; decompose; subst; autobatch size = 7 - | lapply linear track_inv_scut to H5; decompose; subst; autobatch - | lapply linear track_inv_scut to H4; decompose; subst; + | lapply linear track_inv_impw to H3; decompose; destruct; autobatch + | lapply linear track_inv_impr to H3; decompose; destruct; autobatch + | lapply linear track_inv_impi to H7; decompose; destruct; autobatch size = 7 + | lapply linear track_inv_scut to H5; decompose; destruct; autobatch + | lapply linear track_inv_scut to H4; decompose; destruct; lapply linear track_inv_lref to H6; decompose; autobatch - | lapply linear track_inv_scut to H4; decompose; subst; + | lapply linear track_inv_scut to H4; decompose; destruct; lapply linear track_inv_lref to H5; decompose; autobatch - | lapply linear track_inv_scut to H3; decompose; subst; - lapply linear track_inv_prin to H5; subst; autobatch - | lapply linear track_inv_scut to H3; decompose; subst; - lapply linear track_inv_prin to H4; subst; autobatch - | lapply linear track_inv_scut to H3; decompose; subst; - lapply linear track_inv_impw to H4; decompose; subst; - lapply linear track_inv_impr to H5; decompose; subst; autobatch + | lapply linear track_inv_scut to H3; decompose; destruct; + lapply linear track_inv_prin to H5; destruct; autobatch + | lapply linear track_inv_scut to H3; decompose; destruct; + lapply linear track_inv_prin to H4; destruct; autobatch + | lapply linear track_inv_scut to H3; decompose; destruct; + lapply linear track_inv_impw to H4; decompose; destruct; + lapply linear track_inv_impr to H5; decompose; destruct; autobatch ]. qed. diff --git a/matita/contribs/RELATIONAL/NLE/inv.ma b/matita/contribs/RELATIONAL/NLE/inv.ma index 9d46d6cac..013cd67f1 100644 --- a/matita/contribs/RELATIONAL/NLE/inv.ma +++ b/matita/contribs/RELATIONAL/NLE/inv.ma @@ -18,23 +18,23 @@ include "NLE/defs.ma". theorem nle_inv_succ_1: \forall x,y. x < y \to \exists z. y = succ z \land x <= z. - intros. inversion H; clear H; intros; subst. autobatch. + intros. inversion H; clear H; intros; destruct. autobatch. qed. theorem nle_inv_succ_succ: \forall x,y. x < succ y \to x <= y. - intros. inversion H; clear H; intros; subst. autobatch. + intros. inversion H; clear H; intros; destruct. autobatch. qed. theorem nle_inv_succ_zero: \forall x. x < zero \to False. - intros. inversion H; clear H; intros; subst. + intros. inversion H; clear H; intros; destruct. qed. theorem nle_inv_zero_2: \forall x. x <= zero \to x = zero. - intros. inversion H; clear H; intros; subst. autobatch. + intros. inversion H; clear H; intros; destruct. autobatch. qed. theorem nle_inv_succ_2: \forall y,x. x <= succ y \to x = zero \lor \exists z. x = succ z \land z <= y. - intros. inversion H; clear H; intros; subst; + intros. inversion H; clear H; intros; destruct; autobatch depth = 4. qed. diff --git a/matita/contribs/RELATIONAL/NLE/order.ma b/matita/contribs/RELATIONAL/NLE/order.ma index c50e7befd..cc3cc3030 100644 --- a/matita/contribs/RELATIONAL/NLE/order.ma +++ b/matita/contribs/RELATIONAL/NLE/order.ma @@ -24,7 +24,7 @@ theorem nle_trans: \forall x,y. x <= y \to \forall z. y <= z \to x <= z. intros 3. elim H; clear H x y; [ autobatch - | lapply linear nle_inv_succ_1 to H3. decompose. subst. + | lapply linear nle_inv_succ_1 to H3. decompose. destruct. autobatch ]. qed. @@ -38,7 +38,7 @@ theorem nle_irrefl: \forall x. x < x \to False. qed. theorem nle_irrefl_ei: \forall x, z. z <= x \to z = succ x \to False. - intros 3. elim H; clear H x z; subst. autobatch. + intros 3. elim H; clear H x z; destruct. autobatch. qed. theorem nle_irrefl_smart: \forall x. x < x \to False. diff --git a/matita/contribs/RELATIONAL/NLE/props.ma b/matita/contribs/RELATIONAL/NLE/props.ma index 3654b7d89..576a079ae 100644 --- a/matita/contribs/RELATIONAL/NLE/props.ma +++ b/matita/contribs/RELATIONAL/NLE/props.ma @@ -26,6 +26,6 @@ theorem nle_gt_or_le: \forall x, y. y > x \lor y <= x. | decompose; [ lapply linear nle_inv_succ_1 to H1 | lapply linear nle_lt_or_eq to H1 - ]; decompose; subst; autobatch depth = 4 + ]; decompose; destruct; autobatch depth = 4 ]. qed. diff --git a/matita/contribs/RELATIONAL/NPlus/fun.ma b/matita/contribs/RELATIONAL/NPlus/fun.ma index 66847cf93..03dd7d0ef 100644 --- a/matita/contribs/RELATIONAL/NPlus/fun.ma +++ b/matita/contribs/RELATIONAL/NPlus/fun.ma @@ -28,7 +28,7 @@ theorem nplus_mono: \forall p,q,r1. (p + q == r1) \to intros 4. elim H; clear H q r1; [ lapply linear nplus_inv_zero_2 to H1 | lapply linear nplus_inv_succ_2 to H3. decompose - ]; subst; autobatch. + ]; destruct; autobatch. qed. theorem nplus_inj_1: \forall p1, q, r. (p1 + q == r) \to diff --git a/matita/contribs/RELATIONAL/NPlus/inv.ma b/matita/contribs/RELATIONAL/NPlus/inv.ma index ea196cd6d..b6ac60873 100644 --- a/matita/contribs/RELATIONAL/NPlus/inv.ma +++ b/matita/contribs/RELATIONAL/NPlus/inv.ma @@ -26,29 +26,29 @@ theorem nplus_inv_succ_1: \forall p,q,r. ((succ p) + q == r) \to \exists s. r = (succ s) \land p + q == s. intros. elim H; clear H q r; intros; [ autobatch depth = 4 - | clear H1. decompose. subst. autobatch depth = 4 + | clear H1. decompose. destruct. autobatch depth = 4 ] qed. theorem nplus_inv_zero_2: \forall p,r. (p + zero == r) \to p = r. - intros. inversion H; clear H; intros; subst. autobatch. + intros. inversion H; clear H; intros; destruct. autobatch. qed. theorem nplus_inv_succ_2: \forall p,q,r. (p + (succ q) == r) \to \exists s. r = (succ s) \land p + q == s. - intros. inversion H; clear H; intros; subst. + intros. inversion H; clear H; intros; destruct. autobatch depth = 4. qed. theorem nplus_inv_zero_3: \forall p,q. (p + q == zero) \to p = zero \land q = zero. - intros. inversion H; clear H; intros; subst. autobatch. + intros. inversion H; clear H; intros; destruct. autobatch. qed. theorem nplus_inv_succ_3: \forall p,q,r. (p + q == (succ r)) \to \exists s. p = succ s \land (s + q == r) \lor q = succ s \land p + s == r. - intros. inversion H; clear H; intros; subst; + intros. inversion H; clear H; intros; destruct; autobatch depth = 4. qed. @@ -57,13 +57,13 @@ qed. theorem nplus_inv_succ_2_3: \forall p,q,r. (p + (succ q) == (succ r)) \to p + q == r. intros. - lapply linear nplus_inv_succ_2 to H. decompose. subst. autobatch. + lapply linear nplus_inv_succ_2 to H. decompose. destruct. autobatch. qed. theorem nplus_inv_succ_1_3: \forall p,q,r. ((succ p) + q == (succ r)) \to p + q == r. intros. - lapply linear nplus_inv_succ_1 to H. decompose. subst. autobatch. + lapply linear nplus_inv_succ_1 to H. decompose. destruct. autobatch. qed. theorem nplus_inv_eq_2_3: \forall p,q. (p + q == q) \to p = zero. diff --git a/matita/contribs/RELATIONAL/NPlus/monoid.ma b/matita/contribs/RELATIONAL/NPlus/monoid.ma index 1ccd6417e..a521c9a1d 100644 --- a/matita/contribs/RELATIONAL/NPlus/monoid.ma +++ b/matita/contribs/RELATIONAL/NPlus/monoid.ma @@ -32,7 +32,7 @@ theorem nplus_comm: \forall p, q, x. (p + q == x) \to intros 4; elim H; clear H q x; [ lapply linear nplus_inv_zero_1 to H1 | lapply linear nplus_inv_succ_1 to H3. decompose - ]; subst; autobatch. + ]; destruct; autobatch. qed. theorem nplus_comm_rew: \forall p,q,r. (p + q == r) \to q + p == r. @@ -44,11 +44,11 @@ theorem nplus_ass: \forall p1, p2, r1. (p1 + p2 == r1) \to \forall r3. (p2 + p3 == r3) \to \forall s3. (p1 + r3 == s3) \to s1 = s3. intros 4. elim H; clear H p2 r1; - [ lapply linear nplus_inv_zero_1 to H2. subst. - lapply nplus_mono to H1, H3. subst. autobatch - | lapply linear nplus_inv_succ_1 to H3. decompose. subst. - lapply linear nplus_inv_succ_1 to H4. decompose. subst. - lapply linear nplus_inv_succ_2 to H5. decompose. subst. autobatch + [ lapply linear nplus_inv_zero_1 to H2. destruct. + lapply nplus_mono to H1, H3. destruct. autobatch + | lapply linear nplus_inv_succ_1 to H3. decompose. destruct. + lapply linear nplus_inv_succ_1 to H4. decompose. destruct. + lapply linear nplus_inv_succ_2 to H5. decompose. destruct. autobatch ]. qed. @@ -69,18 +69,18 @@ theorem nplus_comm_1: \forall p1, q, r1. (p1 + q == r1) \to intros 4. elim H; clear H q r1; [ lapply linear nplus_inv_zero_2 to H1 | lapply linear nplus_inv_succ_2 to H3. - lapply linear nplus_inv_succ_2 to H4. decompose. subst. + lapply linear nplus_inv_succ_2 to H4. decompose. destruct. lapply linear nplus_inv_succ_2 to H5. decompose - ]; subst; autobatch. + ]; destruct; autobatch. qed. theorem nplus_comm_1_rew: \forall p1,q,r1. (p1 + q == r1) \to \forall p2,r2. (p2 + q == r2) \to \forall s. (p1 + r2 == s) \to (p2 + r1 == s). intros 4. elim H; clear H q r1; - [ lapply linear nplus_inv_zero_2 to H1. subst - | lapply linear nplus_inv_succ_2 to H3. decompose. subst. - lapply linear nplus_inv_succ_2 to H4. decompose. subst + [ lapply linear nplus_inv_zero_2 to H1. destruct + | lapply linear nplus_inv_succ_2 to H3. decompose. destruct. + lapply linear nplus_inv_succ_2 to H4. decompose. destruct ]; autobatch. qed. @@ -89,14 +89,14 @@ theorem nplus_shift_succ_sx: \forall p,q,r. (p + (succ q) == r) \to (succ p) + q == r. intros. lapply linear nplus_inv_succ_2 to H as H0. - decompose. subst. auto new timeout=100. + decompose. destruct. 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_inv_succ_1 to H as H0. - decompose. subst. auto new timeout=100. + decompose. destruct. auto new timeout=100. qed. theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to @@ -104,11 +104,11 @@ theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to \exists q. (q1 + q2 == q) \land p + q == r2. intros 2; elim q1; clear q1; intros; [ lapply linear nplus_inv_zero_2 to H as H0. - subst. + destruct. | lapply linear nplus_inv_succ_2 to H1 as H0. - decompose. subst. + decompose. destruct. lapply linear nplus_inv_succ_1 to H2 as H0. - decompose. subst. + decompose. destruct. lapply linear H to H4, H3 as H0. decompose. ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**) @@ -119,11 +119,11 @@ theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to \exists p. (p1 + p2 == p) \land p + q == r2. intros 2; elim q; clear q; intros; [ lapply linear nplus_inv_zero_2 to H as H0. - subst + destruct | lapply linear nplus_inv_succ_2 to H1 as H0. - decompose. subst. + decompose. destruct. lapply linear nplus_inv_succ_2 to H2 as H0. - decompose. subst. + decompose. destruct. lapply linear H to H4, H3 as H0. decompose. ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**) diff --git a/matita/contribs/RELATIONAL/NPlusList/props.ma b/matita/contribs/RELATIONAL/NPlusList/props.ma index 3f53d92cf..f7fc4305e 100644 --- a/matita/contribs/RELATIONAL/NPlusList/props.ma +++ b/matita/contribs/RELATIONAL/NPlusList/props.ma @@ -22,7 +22,7 @@ axiom npluslist_gen_cons: \forall l,q,r. (* intros. inversion H; clear H; intros; [ id - | subst. + | destruct. *) theorem npluslist_inj_2: \forall ns1,ns2,n. diff --git a/matita/contribs/RELATIONAL/ZEq/setoid.ma b/matita/contribs/RELATIONAL/ZEq/setoid.ma index 6721926b1..37ca8f619 100644 --- a/matita/contribs/RELATIONAL/ZEq/setoid.ma +++ b/matita/contribs/RELATIONAL/ZEq/setoid.ma @@ -30,7 +30,7 @@ qed. theorem zeq_trans: \forall z1,z2. z1 = z2 \to \forall z3. z2 = z3 \to z1 = z3. intros 3. elim H. clear H z1 z2. - inversion H3. clear H3. intros. subst. + inversion H3. clear H3. intros. destruct. lapply (nplus_total n5 n6). decompose. lapply (nplus_total n4 n9). decompose. apply zeq. diff --git a/matita/tests/dependent_injection.ma b/matita/tests/dependent_injection.ma index 2f4bbe820..e217a7652 100644 --- a/matita/tests/dependent_injection.ma +++ b/matita/tests/dependent_injection.ma @@ -35,7 +35,7 @@ theorem injection_test3: ∀t,t'. tnode nat t tempty = tnode nat t' tempty → t = t'. intros. destruct H. - assumption. + reflexivity. qed. theorem injection_test3: diff --git a/matita/tests/injection.ma b/matita/tests/injection.ma index 929e63cd5..2cc7110ff 100644 --- a/matita/tests/injection.ma +++ b/matita/tests/injection.ma @@ -27,7 +27,7 @@ inductive t0 : Type := theorem injection_test0: ∀n,n',m,m'. k0 n m = k0 n' m' → m = m'. intros; destruct H; - assumption. + reflexivity. qed. inductive t : Type → Type := @@ -37,7 +37,7 @@ inductive t : Type → Type := theorem injection_test1: ∀n,n'. k n = k n' → n = n'. intros; destruct H; - assumption. + reflexivity. qed. inductive tt (A:Type) : Type -> Type := @@ -47,7 +47,7 @@ inductive tt (A:Type) : Type -> Type := theorem injection_test2: ∀n,n',m,m'. k1 bool n n' = k1 bool m m' → n' = m'. intros; destruct H; - assumption. + reflexivity. qed. inductive ttree : Type → Type := @@ -58,5 +58,5 @@ theorem injection_test4: ∀n,n',m,m'. k1 bool (S n) (S (S m)) = k1 bool (S n') (S (S (S m'))) → m = S m'. intros; destruct H; - assumption. + reflexivity. qed. -- 2.39.2