A way to specialize universally quantified hypothesis: if H is

   H: forall (n:nat)(b:bool), P n b 
then "narrow H with 0 true" will leave H: P 0 true. 

The name for this tactic should ideally be "specialize", but this one
already exists (old stuff, same idea but no "in place" modification, 
not documented anymore, still used in users contribs). 





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

1 files changed, 16 insertions, 0 deletions

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 6c5c0e011..61a6c8e77 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -55,6 +55,22 @@ Ltac f_equal :=
    | _ => idtac
   end.
 
+(* Specializing universal hypothesis. 
+   The word "specialize" is already used for a not-documented-anymore 
+   tactic still used in some users contribs. Any idea for a better name?
+*)
+
+Tactic Notation "narrow" hyp(H) "with" constr(x) := 
+ generalize (H x); clear H; intro H.
+Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) := 
+ generalize (H x y); clear H; intro H.
+Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z):= 
+ generalize (H x y z); clear H; intro H.
+Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t):= 
+ generalize (H x y z t); clear H; intro H.
+Tactic Notation "narrow" hyp(H) "with" constr(x) constr(y) constr(z) constr(t) constr(u):= 
+ generalize (H x y z t u); clear H; intro H.
+
 (* Rewriting in all hypothesis several times everywhere *)
 
 Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.