diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/equality.ml | 39 | ||||
-rw-r--r-- | tactics/equality.mli | 5 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 7 |
3 files changed, 51 insertions, 0 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 2d68161c9..fdb579729 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 9e715751e..20ff6e472 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 3c6ea9ab3..c21189213 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 + |