- new tactic subst removes simple non recursive equalities from the context

- RELATIONAL updated to use the new tactic

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index efcd210713db9c3f2bafa06733f47d3108975883..54924ff4c87351c3cd04f4eb1a963841fbdd4f5b 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -83,7 +83,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Right of loc
   | Ring of loc
   | Split of loc
-  | Subst of loc * string
+  | Subst of loc
   | Symmetry of loc
   | Transitivity of loc * 'term
   (* Costruttori Aggiunti *)

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 425751b723b0236ccd2834b0153b43706e3837db..e1855014d27e351498d4b138ea95eea84cd9681e 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -152,7 +152,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Right _ -> "right"
   | Ring _ -> "ring"
   | Split _ -> "split"
-  | Subst (_, s) -> "subst " ^ s
+  | Subst _ -> "subst"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ term_pp term
   (* Tattiche Aggiunte *)

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index ac63812461ab3002c9eb4ee5e2a4c42f9ce7ef6c..4a92548454f56366c9e0dc357d277b2f3d9d5bd0 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -152,7 +152,7 @@ let tactic_of_ast ast =
   | GrafiteAst.Right _ -> Tactics.right
   | GrafiteAst.Ring _ -> Tactics.ring
   | GrafiteAst.Split _ -> Tactics.split
-  | GrafiteAst.Subst (_, hyp) -> Tactics.subst ~hyp
+  | GrafiteAst.Subst _ -> Tactics.subst
   | GrafiteAst.Symmetry _ -> Tactics.symmetry
   | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
   (* Implementazioni Aggiunte *)

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 151d8cebdb008d4ab83a22159b391f2ee1944d30..cdf01febd9da93bfc81ab797c31283033d696f8c 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -246,8 +246,8 @@ let disambiguate_tactic
         metasenv,GrafiteAst.Ring loc
     | GrafiteAst.Split loc ->
         metasenv,GrafiteAst.Split loc
-    | GrafiteAst.Subst (loc, hyp) ->
-        metasenv, GrafiteAst.Subst (loc, hyp)
+    | GrafiteAst.Subst loc ->
+        metasenv, GrafiteAst.Subst loc
     | GrafiteAst.Symmetry loc ->
         metasenv,GrafiteAst.Symmetry loc
     | GrafiteAst.Transitivity (loc, term) -> 

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 9e9be81e2e675a4165c795ab3ca4ae1be94eaf72..16f7998d19a7ee528d53f46f822b9e0a9d02a3cf 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -233,8 +233,8 @@ EXTEND
         GrafiteAst.Ring loc
     | IDENT "split" ->
         GrafiteAst.Split loc
-    | IDENT "subst"; id = IDENT ->
-        GrafiteAst.Subst (loc, id)    
+    | IDENT "subst" ->
+        GrafiteAst.Subst loc    
     | IDENT "symmetry" ->
         GrafiteAst.Symmetry loc
     | IDENT "transitivity"; t = tactic_term ->

diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml
index c697acaedaeeb79d08940d912abd3ced915b40d6..fd6e7c59f35d8e2b1b4798eac51bf7d445427cf9 100644 (file)
--- a/components/tactics/equalityTactics.ml
+++ b/components/tactics/equalityTactics.ml
@@ -191,7 +191,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit
     in
      (proof',goals)
   with (* FG: this should be PET.Fail _ *)
-     TC.TypeCheckerFailure _ -> PET.apply_tactic (P.letout_tac ()) status
+     TC.TypeCheckerFailure _ -> PET.apply_tactic P.letout_tac status
  in
   ProofEngineTypes.mk_tactic (_rewrite_tac ~direction ~pattern equality)
   
@@ -362,7 +362,7 @@ let transitivity_tac ~term =
   ProofEngineTypes.mk_tactic (transitivity_tac ~term)
 ;;
 
-(* FG *)
+(* FG: subst tactic *********************************************************)
 
 let msg0 = lazy "Subst: not found in context"
 let msg1 = lazy "Subst: not a simple equality"
@@ -402,3 +402,26 @@ let subst_tac ~hyp =
       PET.apply_tactic tac status
    in
    PET.mk_tactic subst_tac
+
+(* FG: This should be replaced by T.try_tactic *)
+let try_tactic ~tactic =
+   let try_tactic status =
+      try PET.apply_tactic tactic status with
+         | PET.Fail _ -> PET.apply_tactic T.id_tac status
+   in
+   PET.mk_tactic try_tactic
+
+let subst_tac =
+   let subst hyp = try_tactic ~tactic:(subst_tac hyp) in
+   let map = function
+      | Some (C.Name s, _) -> Some (subst s)
+      | _                  -> None
+   in
+   let subst_tac status =
+      let (proof, goal) = status in
+      let (_, metasenv, _, _) = proof in
+      let _, context, _ = CicUtil.lookup_meta goal metasenv in
+      let tactics = PEH.list_rev_map_filter map context in
+      PET.apply_tactic (T.seq ~tactics) status
+   in
+   PET.mk_tactic subst_tac

diff --git a/components/tactics/equalityTactics.mli b/components/tactics/equalityTactics.mli
index 31ad7eedfd50d7ff0e64f1ff6499283f35098adf..4edb5747a5d1fedf0f3dd436b83ca97cf8eaeb47 100644 (file)
--- a/components/tactics/equalityTactics.mli
+++ b/components/tactics/equalityTactics.mli
@@ -41,4 +41,5 @@ val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic
 
 (* FG *)
 
-val subst_tac: hyp:string -> ProofEngineTypes.tactic
+(* rewrites and clears all simple equalities in the context *)
+val subst_tac: ProofEngineTypes.tactic

diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 5fb8d4ae1eb56f88522cb14133c1a7c846a60e69..9baf829ea940d2bad3c61d71ebfdea8781043f34 100644 (file)
--- a/components/tactics/primitiveTactics.ml
+++ b/components/tactics/primitiveTactics.ml
@@ -571,7 +571,7 @@ let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fres
 
 module C = Cic
 
-let letout_tac () =
+let letout_tac =
    let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
    let term = C.Sort C.Set in
    let letout_tac (proof, goal) =

diff --git a/components/tactics/primitiveTactics.mli b/components/tactics/primitiveTactics.mli
index 0f003bb4c0b0cbd94ce1e4419038af6f245714bd..ce5194ad133e4c1435ed6932189c86628f60916d 100644 (file)
--- a/components/tactics/primitiveTactics.mli
+++ b/components/tactics/primitiveTactics.mli
@@ -81,4 +81,4 @@ val elim_intros_tac:
 
 (* inserts a hole in the context *)
 val letout_tac:
-  unit -> ProofEngineTypes.tactic 
+  ProofEngineTypes.tactic 

diff --git a/components/tactics/tacticals.ml b/components/tactics/tacticals.ml
index ceb2d2de88cb28fc8a7554ee87c1167e5c846af8..88e2f4b9e371a3ce156c71de33c765889781da50 100644 (file)
--- a/components/tactics/tacticals.ml
+++ b/components/tactics/tacticals.ml
@@ -242,7 +242,7 @@ struct
 
   (* This applies tactic and catches its possible failure *)
   let try_tactic ~tactic =
-   let rec try_tactic ~tactic status =
+   let try_tactic status =
     info (lazy "in Tacticals.try_tactic");
     try
      S.apply_tactic tactic status
@@ -252,7 +252,7 @@ struct
         "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
       S.apply_tactic S.id_tactic status
    in
-    S.mk_tactic (try_tactic ~tactic)
+    S.mk_tactic try_tactic
 
   (* This tries tactics until one of them doesn't _solve_ the goal *)
   (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)

diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index a77b3475f8a0679e5ce7b49aaea55fadef9aa7d0..4517db0b5eff1bfdfb7d11553ecc1c2910073fc7 100644 (file)
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Aug 28 17:29:50 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Aug 29 11:37:38 CEST 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic
@@ -80,7 +80,7 @@ val ring : ProofEngineTypes.tactic
 val set_goal : int -> ProofEngineTypes.tactic
 val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 val split : ProofEngineTypes.tactic
-val subst : hyp:string -> ProofEngineTypes.tactic
+val subst : ProofEngineTypes.tactic
 val symmetry : ProofEngineTypes.tactic
 val transitivity : term:Cic.term -> ProofEngineTypes.tactic
 val unfold :

diff --git a/matita/contribs/RELATIONAL/NLE/dec.ma b/matita/contribs/RELATIONAL/NLE/dec.ma
index 6bdb81946269bb7313a9d95f0ab2197962ddd4bb..436dc7e62788ed5df336ef849fc223889a037e33 100644 (file)
--- a/matita/contribs/RELATIONAL/NLE/dec.ma
+++ b/matita/contribs/RELATIONAL/NLE/dec.ma
@@ -21,11 +21,9 @@ theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x.
  [ auto
  | decompose;
    [ lapply linear nle_gen_succ_1 to H1. decompose.
-     rewrite > H1. clear H1 n. auto
+     subst. auto
    | lapply linear nle_lt_or_eq to H1; decompose;
-     [ auto
-     | rewrite > H. clear H n. auto
-     ]
+     subst; auto
    ]
  ].
 qed.

diff --git a/matita/contribs/RELATIONAL/NLE/fwd.ma b/matita/contribs/RELATIONAL/NLE/fwd.ma
index 19ad50b9b2aa7c11cae590a0f3ec987ec194e96d..6a78e0aac788bce7a77661c3bc93b213fec70b3b 100644 (file)
--- a/matita/contribs/RELATIONAL/NLE/fwd.ma
+++ b/matita/contribs/RELATIONAL/NLE/fwd.ma
@@ -24,7 +24,7 @@ theorem nle_gen_succ_1: \forall x,y. x < y \to
  intros. inversion H; clear H; intros;
  [ apply (eq_gen_succ_zero ? ? H)
  | lapply linear eq_gen_succ_succ to H2 as H0.
-   rewrite > H0. clear H0.
+   subst.
    apply ex_intro; [|auto] (**)
  ].
 qed.
@@ -34,8 +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.
-   rewrite > H0. rewrite > H2. clear H0 H2.
-   auto
+   subst. auto
  ].
 qed.
 

diff --git a/matita/contribs/RELATIONAL/NLE/props.ma b/matita/contribs/RELATIONAL/NLE/props.ma
index e961f5a9ced40c39a053ab7d7d07f88455a91bc8..8745e160e4b94c6ae1e5e4d6565839a38f634732 100644 (file)
--- a/matita/contribs/RELATIONAL/NLE/props.ma
+++ b/matita/contribs/RELATIONAL/NLE/props.ma
@@ -28,11 +28,9 @@ 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_succ_2 to H1. decompose;
-   [ rewrite > H1. clear H1. auto
+   [ subst. auto
    | lapply linear H to H3 as H0. decompose;
-     [ rewrite > H1. clear H1 x. auto
-     | rewrite < H. clear H n. auto
-     ]
+     subst; auto
    ]
  ].
 qed.

diff --git a/matita/contribs/RELATIONAL/NPlus/fwd.ma b/matita/contribs/RELATIONAL/NPlus/fwd.ma
index 350a53f622b6d71bd8763bef5f37e72534c2a922..b1f7f2ca303b92653a4adc47d87d607264b04fa4 100644 (file)
--- a/matita/contribs/RELATIONAL/NPlus/fwd.ma
+++ b/matita/contribs/RELATIONAL/NPlus/fwd.ma
@@ -32,7 +32,7 @@ theorem nplus_gen_succ_1: \forall p,q,r. ((succ p) + q == r) \to
  [
  | clear H1.
    decompose.
-   rewrite > H1. clear H1 n2
+   subst.
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
 
@@ -50,7 +50,7 @@ theorem nplus_gen_succ_2: \forall p,q,r. (p + (succ q) == r) \to
  [ lapply eq_gen_succ_zero to H as H0. apply H0
  | clear H1 H3 r.
    lapply linear eq_gen_succ_succ to H2 as H0.
-   rewrite > H0. clear H0 q.
+   subst.
    apply ex_intro; [| auto ] (**)
  ].
 qed.
@@ -58,8 +58,7 @@ qed.
 theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to 
                           p = zero \land q = zero.
  intros. inversion H; clear H; intros;
- [ rewrite < H1. clear H1 p.
-   auto
+ [ subst. auto
  | clear H H1.
    lapply eq_gen_zero_succ to H3 as H0. apply H0
  ].
@@ -69,10 +68,10 @@ theorem nplus_gen_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;
- [ rewrite < H1. clear H1 p
+ [ subst.
  | clear H1.
    lapply linear eq_gen_succ_succ to H3 as H0.
-   rewrite > H0. clear H0 r.
+   subst.
  ]; apply ex_intro; [| auto || auto ] (**)
 qed.
 (*
@@ -82,8 +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.
-   rewrite > H0. clear H0 p.
-   auto
+   subst. auto
  | clear H.
    lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
@@ -96,12 +94,12 @@ variant nplus_gen_succ_3_alt: \forall p,q,r. (p + q == (succ r)) \to
                                          q = succ s \land p + s == r.
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
-   rewrite > H0. clear H0 p
+   subst
  | clear H.
    lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
    lapply linear eq_gen_succ_succ to H1 as H0.
-   rewrite > H0. clear H0 r.
+   subst
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
 *)
@@ -110,21 +108,21 @@ qed.
 theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
-   rewrite > H0. clear H0 p
+   subst
  | lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
    lapply linear eq_gen_succ_succ to H2 as H0.
-   rewrite < H0 in H3. clear H0 a
+   subst
  ]; auto.
 qed.
 
 theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
  intros 1. elim p; clear p; intros;
  [ lapply linear nplus_gen_zero_1 to H as H0.
-   rewrite > H0. clear H0 q
+   subst
  | lapply linear nplus_gen_succ_1 to H1 as H0.
    decompose.
    lapply linear eq_gen_succ_succ to H2 as H0.
-   rewrite < H0 in H3. clear H0 a
+   subst
  ]; auto.
 qed.

diff --git a/matita/contribs/RELATIONAL/NPlus/props.ma b/matita/contribs/RELATIONAL/NPlus/props.ma
index a40187c65740bdf57362a887d94fda6fcf68b1de..5e7cc1b7f592c8bca10f3516ad9d1398cf4fb5c3 100644 (file)
--- a/matita/contribs/RELATIONAL/NPlus/props.ma
+++ b/matita/contribs/RELATIONAL/NPlus/props.ma
@@ -24,20 +24,20 @@ theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to
                       (succ p) + q == (succ r).
  intros 2. elim q; clear q;
  [ lapply linear nplus_gen_zero_2 to H as H0.
-   rewrite > H0. clear H0 p
+   subst
  | lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
-   rewrite > H2. clear H2 r
+   subst
  ]; auto.
 qed.
 
 theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r.
  intros 2. elim q; clear q;
  [ lapply linear nplus_gen_zero_2 to H as H0.
-   rewrite > H0. clear H0 p
+   subst
  | lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
-   rewrite > H2. clear H2 r
+   subst
  ]; auto.
 qed.
 
@@ -45,18 +45,14 @@ 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.
- rewrite > H1. clear H1 r.
- auto.
+ decompose. subst. auto.
 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.
- rewrite > H1. clear H1 r.
- auto.
+ decompose. subst. auto.
 qed.
 
 theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to 
@@ -64,13 +60,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_gen_zero_2 to H as H0.
-   rewrite > H0. clear H0 p
+   subst.
  | lapply linear nplus_gen_succ_2 to H1 as H0.
-   decompose.
-   rewrite > H3. rewrite > H3 in H2. clear H3 r1.
+   decompose. subst.
    lapply linear nplus_gen_succ_1 to H2 as H0.
-   decompose.
-   rewrite > H2. clear H2 r2.
+   decompose. subst.
    lapply linear H to H4, H3 as H0.
    decompose.
  ]; apply ex_intro; [| auto || auto ]. (**)
@@ -81,13 +75,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_gen_zero_2 to H as H0.
-   rewrite > H0. clear H0 p1
+   subst
  | lapply linear nplus_gen_succ_2 to H1 as H0.
-   decompose.
-   rewrite > H3. rewrite > H3 in H2. clear H3 r1.
+   decompose. subst.
    lapply linear nplus_gen_succ_2 to H2 as H0.
-   decompose.
-   rewrite > H2. clear H2 r2.
+   decompose. subst.
    lapply linear H to H4, H3 as H0.
    decompose.
  ]; apply ex_intro; [| auto || auto ]. (**)
@@ -97,12 +89,10 @@ theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to
                     \forall r2. (p + q == r2) \to r1 = r2.
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
-   rewrite > H0 in H1. clear H0 p
+   subst
  | lapply linear nplus_gen_succ_2 to H1 as H0.
-   decompose.
-   rewrite > H3. clear H3 r1.
+   decompose. subst.
    lapply linear nplus_gen_succ_2 to H2 as H0.
-   decompose.
-   rewrite > H2. clear H2 r2.
+   decompose. subst.
  ]; auto.
 qed.

diff --git a/matita/contribs/prova.ma b/matita/contribs/prova.ma
index 407db9b6658f907ba5b0d8718e6524773858421f..457899a8ce8d4c9d3c0a6a5950557214a41fb7e3 100644 (file)
--- a/matita/contribs/prova.ma
+++ b/matita/contribs/prova.ma
@@ -19,9 +19,9 @@ include "nat/nat.ma".
 theorem pippo: \forall (P,Q,R:nat \to Prop).
                \forall x,y. x=y \to P x \to Q x \to R x.
                intros.
-               try rewrite > P in Q.  
+               rewrite > P in Q.  
 (*             
-theorem pippo2: \forall (P,Q,R:nat \to Prop).
-                \forall x,y. x=y \to P x \to Q x \to R x.
-                intros. rewrite > H in y.
-*)
+theorem pippo: \forall (P,Q,R:nat \to Prop).
+               \forall x,y. x=y \to P x \to Q x \to R x.
+               intros. rewrite > H in y.
+*)
\ No newline at end of file

diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index 53a20ac6a78e3c07404d442cb8b7a0de17c7b661..cd26700ab703a885027108ae4bd5fa217dea8830 100644 (file)
--- a/matita/help/C/sec_tactics.xml
+++ b/matita/help/C/sec_tactics.xml
@@ -1578,6 +1578,46 @@ its constructor takes no arguments.</para>
       </variablelist>
     </para>
   </sect1>
+  
+  <sect1 id="tac_subst">
+    <title>subst</title>
+    <titleabbrev>subst</titleabbrev>
+    <para><userinput>subst</userinput></para>
+    <para>
+      <variablelist>
+        <varlistentry role="tactic.synopsis">
+          <term>Synopsis:</term>
+          <listitem>
+            <para><emphasis role="bold">subst</emphasis></para>
+          </listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Pre-conditions:</term>
+          <listitem><para>
+           None.
+         </para></listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>Action:</term>
+          <listitem><para>
+           For each premise of the form 
+           <command>H: x = t</command> or <command>H: t = x</command>
+           where <command>x</command> is a local variable and 
+           <command>t</command> does not depend on <command>x</command>,
+           the tactic rewrites <command>H</command> wherever 
+           <command>x</command> appears clearing <command>H</command> and
+           <command>x</command> afterwards.
+         </para></listitem>
+        </varlistentry>
+        <varlistentry>
+          <term>New sequents to prove:</term>
+          <listitem><para>
+           The one opened by the applied tactics.
+          </para></listitem>
+        </varlistentry>
+      </variablelist>
+    </para>
+  </sect1>
   <sect1 id="tac_symmetry">
     <title>symmetry</title>
     <titleabbrev>symmetry</titleabbrev>

diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml
index e44a53068e7bd6a17bcde0c95b23dca929c30e63..2709769ba91f38b12439ea48465495daf1de079b 100644 (file)
--- a/matita/help/C/tactic_quickref.xml
+++ b/matita/help/C/tactic_quickref.xml
@@ -270,6 +270,15 @@
           </link>
         </entry>
       </row>
+      <row>
+        <entry/>
+        <entry>|</entry>
+        <entry>
+          <link linkend="tac_subst">
+            <emphasis role="bold">subst</emphasis>
+          </link>
+        </entry>
+      </row>
       <row>
         <entry/>
         <entry>|</entry>

diff --git a/matita/matita.lang b/matita/matita.lang
index b7198579c4eac2c5b67401d1a2f09a295f6cfcab..13c88e48054c678477bea0ceeb60a3eab7c128fa 100644 (file)
--- a/matita/matita.lang
+++ b/matita/matita.lang
@@ -123,6 +123,7 @@
     <keyword>symmetry</keyword>
     <keyword>simplify</keyword>
     <keyword>split</keyword>
+    <keyword>subst</keyword>
     <keyword>to</keyword>
     <keyword>transitivity</keyword>
     <keyword>unfold</keyword>