diff options
author | 2004-03-10 14:08:16 +0000 | |
---|---|---|
committer | 2004-03-10 14:08:16 +0000 | |
commit | 2df60ce176688e66c18c88c04fe6c7f5a56dc5d1 (patch) | |
tree | 3aa7e772a43405a08e8d0f247dbc2107de53c97d | |
parent | c3d267824da8e03a630a088a677ebf5d3a2d0f94 (diff) |
Ajout tactiques stepl et stepr de Nimègue
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5447 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | tactics/extratactics.ml4 | 96 |
1 files changed, 96 insertions, 0 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 6eab2a769..daf3bb465 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -231,3 +231,99 @@ TACTIC EXTEND Subst | [ "Subst" ] -> [ subst_all ] END +(** Nijmegen "step" tactic for setoid rewriting *) + +open Tacticals +open Tactics +open Tactics +open Libnames +open Rawterm +open Summary +open Libobject +open Lib + +(* Registered lemmas are expected to be of the form + x R y -> y == z -> x R z (in the right table) + x R y -> x == z -> z R y (in the left table) +*) + +let transitivity_right_table = ref [] +let transitivity_left_table = ref [] + +(* [step] tries to apply a rewriting lemma; then apply [tac] intended to + complete to proof of the last hypothesis (assumed to state an equality) *) + +let step left x tac = + let l = + List.map (fun lem -> + tclTHENLAST + (apply_with_bindings (constr_of_reference lem, ImplicitBindings [x])) + tac) + !(if left then transitivity_left_table else transitivity_right_table) + in + tclFIRST l + +(* Main function to push lemmas in persistent environment *) + +let cache_transitivity_lemma (_,(left,lem)) = + if left then + transitivity_left_table := lem :: !transitivity_left_table + else + transitivity_right_table := lem :: !transitivity_right_table + +let subst_transitivity_lemma (_,subst,(b,ref)) = (b,subst_global subst ref) + +let (inTransitivity,_) = + declare_object {(default_object "TRANSITIVITY-STEPS") with + cache_function = cache_transitivity_lemma; + open_function = (fun i o -> if i=1 then cache_transitivity_lemma o); + subst_function = subst_transitivity_lemma; + classify_function = (fun (_,o) -> Substitute o); + export_function = (fun x -> Some x) } + +(* Synchronisation with reset *) + +let freeze () = !transitivity_left_table, !transitivity_right_table + +let unfreeze (l,r) = + transitivity_left_table := l; + transitivity_right_table := r + +let init () = + transitivity_left_table := []; + transitivity_right_table := [] + +let _ = + declare_summary "transitivity-steps" + { freeze_function = freeze; + unfreeze_function = unfreeze; + init_function = init; + survive_module = false; + survive_section = false } + +(* Main entry points *) + +let add_transitivity_lemma left ref = + add_anonymous_leaf (inTransitivity (left,Nametab.global ref)) + +(* Vernacular syntax *) + +TACTIC EXTEND Stepl +| ["Stepl" constr(c) "by" tactic(tac) ] -> [ step true c (snd tac) ] +| ["Stepl" constr(c) ] -> [ step true c tclIDTAC ] +END + +TACTIC EXTEND Stepr +| ["Stepr" constr(c) "by" tactic(tac) ] -> [ step false c (snd tac) ] +| ["Stepr" constr(c) ] -> [ step false c tclIDTAC ] +END + +VERNAC COMMAND EXTEND AddStepl +| [ "Declare" "Left" "Step" global(id) ] -> + [ add_transitivity_lemma true id ] +END + +VERNAC COMMAND EXTEND AddStepr +| [ "Declare" "Right" "Step" global(id) ] -> + [ add_transitivity_lemma false id ] +END |