tactique Subst

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2894 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 51 insertions, 0 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2d68161c99..fdb579729b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1500,3 +1500,42 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls =
         (fun l -> validation_gen nlvalid l)
     in
     (repackage sigr gl,validation_fun)
+
+
+(* Substitutions tactics (JCF) *)
+
+exception FoundHyp of identifier
+
+let is_eq_x x c =
+  let eqpat = build_coq_eq_pattern () in
+  (is_matching eqpat c) &&
+  (let (_,y,_) = match_eq eqpat c in
+   match kind_of_term y with Var y -> x = y | _ -> false)
+
+let subst x gl = 
+  let varx = mkVar x in
+  let hyps = pf_hyps_types gl in
+  let hyp = 
+    try
+      let test (id,c) = if is_eq_x x c then raise (FoundHyp id) in
+      List.iter test hyps;
+      errorlabstrm "subst" (str "cannot find any equality over " ++ pr_id x)
+    with FoundHyp id ->
+      id
+  in
+  let dephyps = 
+    let test (id,c) = 
+      if id <> hyp && occur_term varx c then id else failwith "caught" 
+    in
+    map_succeed test hyps
+  in
+  let dephyps = List.rev dephyps in
+  tclTHENLIST [
+    generalize (List.map mkVar dephyps);
+    thin dephyps;
+    rewriteLR (mkVar hyp);
+    intros_using dephyps;
+    clear [hyp];
+    tclTRY (clear [x])
+  ] gl
+
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 9e715751eb..20ff6e4724 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -124,3 +124,8 @@ val explicit_hint_base : goal sigma -> hint_base -> rewriting_rule list
 val autorewrite :
   hint_base list -> tactic list option -> option_step 
     -> tactic list option -> bool -> int -> tactic
+
+
+(* Subst *)
+
+val subst : identifier -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 3c6ea9ab3b..c211892133 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -214,3 +214,10 @@ VERNAC COMMAND EXTEND DeriveDependentInversionClear
 | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
   -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
 END
+
+(* Subst *)
+
+TACTIC EXTEND Subst
+| [ "Subst" ident(x) ] -> [ subst x ]
+END
+