From eefb7b4c9f5c4c531199c95e4bb72d8b8c88bc2e Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 7 Nov 2007 19:52:14 +0000
Subject: [PATCH] - bug fix in destruct - old subst tactic removed - some tests
 fixed

---
 helm/software/components/tactics/Makefile     |  3 +-
 .../components/tactics/destructTactic.ml      | 73 ++++---------------
 helm/software/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 ++--
 .../contribs/RELATIONAL/NPlus/monoid.ma       | 38 +++++-----
 .../contribs/RELATIONAL/NPlusList/props.ma    |  2 +-
 .../matita/contribs/RELATIONAL/ZEq/setoid.ma  |  2 +-
 .../matita/tests/dependent_injection.ma       |  2 +-
 helm/software/matita/tests/injection.ma       |  8 +-
 21 files changed, 130 insertions(+), 159 deletions(-)

diff --git a/helm/software/components/tactics/Makefile b/helm/software/components/tactics/Makefile
index 9a6c6d4d0..7c9f00db5 100644
--- a/helm/software/components/tactics/Makefile
+++ b/helm/software/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/helm/software/components/tactics/destructTactic.ml b/helm/software/components/tactics/destructTactic.ml
index bbfee8041..2ea9e047c 100644
--- a/helm/software/components/tactics/destructTactic.ml
+++ b/helm/software/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/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index a58752461..45bfa7e3b 100644
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/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/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma
index 08972e5e9..499cd5fdc 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma
+++ b/helm/software/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/helm/software/matita/contribs/LOGIC/Insert/fun.ma b/helm/software/matita/contribs/LOGIC/Insert/fun.ma
index f0cc5e514..7c7aba28a 100644
--- a/helm/software/matita/contribs/LOGIC/Insert/fun.ma
+++ b/helm/software/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/helm/software/matita/contribs/LOGIC/Insert/inv.ma b/helm/software/matita/contribs/LOGIC/Insert/inv.ma
index b612858a3..9053183f9 100644
--- a/helm/software/matita/contribs/LOGIC/Insert/inv.ma
+++ b/helm/software/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/helm/software/matita/contribs/LOGIC/Insert/props.ma b/helm/software/matita/contribs/LOGIC/Insert/props.ma
index 6daa22ea6..17148e27e 100644
--- a/helm/software/matita/contribs/LOGIC/Insert/props.ma
+++ b/helm/software/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/helm/software/matita/contribs/LOGIC/NTrack/inv.ma b/helm/software/matita/contribs/LOGIC/NTrack/inv.ma
index 6c57c2040..f272bd518 100644
--- a/helm/software/matita/contribs/LOGIC/NTrack/inv.ma
+++ b/helm/software/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/helm/software/matita/contribs/LOGIC/NTrack/props.ma b/helm/software/matita/contribs/LOGIC/NTrack/props.ma
index 7d41aebdf..bdd23748f 100644
--- a/helm/software/matita/contribs/LOGIC/NTrack/props.ma
+++ b/helm/software/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/helm/software/matita/contribs/LOGIC/Track/inv.ma b/helm/software/matita/contribs/LOGIC/Track/inv.ma
index 77d1107cd..d38d3f120 100644
--- a/helm/software/matita/contribs/LOGIC/Track/inv.ma
+++ b/helm/software/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/helm/software/matita/contribs/LOGIC/Track/pred.ma b/helm/software/matita/contribs/LOGIC/Track/pred.ma
index f9c172813..c4e65c05d 100644
--- a/helm/software/matita/contribs/LOGIC/Track/pred.ma
+++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma b/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma
index 9d46d6cac..013cd67f1 100644
--- a/helm/software/matita/contribs/RELATIONAL/NLE/inv.ma
+++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NLE/order.ma b/helm/software/matita/contribs/RELATIONAL/NLE/order.ma
index c50e7befd..cc3cc3030 100644
--- a/helm/software/matita/contribs/RELATIONAL/NLE/order.ma
+++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NLE/props.ma b/helm/software/matita/contribs/RELATIONAL/NLE/props.ma
index 3654b7d89..576a079ae 100644
--- a/helm/software/matita/contribs/RELATIONAL/NLE/props.ma
+++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma
index 66847cf93..03dd7d0ef 100644
--- a/helm/software/matita/contribs/RELATIONAL/NPlus/fun.ma
+++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma
index ea196cd6d..b6ac60873 100644
--- a/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma
+++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma
index 1ccd6417e..a521c9a1d 100644
--- a/helm/software/matita/contribs/RELATIONAL/NPlus/monoid.ma
+++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/NPlusList/props.ma b/helm/software/matita/contribs/RELATIONAL/NPlusList/props.ma
index 3f53d92cf..f7fc4305e 100644
--- a/helm/software/matita/contribs/RELATIONAL/NPlusList/props.ma
+++ b/helm/software/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/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma b/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma
index 6721926b1..37ca8f619 100644
--- a/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma
+++ b/helm/software/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/helm/software/matita/tests/dependent_injection.ma b/helm/software/matita/tests/dependent_injection.ma
index 2f4bbe820..e217a7652 100644
--- a/helm/software/matita/tests/dependent_injection.ma
+++ b/helm/software/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/helm/software/matita/tests/injection.ma b/helm/software/matita/tests/injection.ma
index 929e63cd5..2cc7110ff 100644
--- a/helm/software/matita/tests/injection.ma
+++ b/helm/software/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