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

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