diff options
| author | letouzey | 2007-11-01 16:57:15 +0000 |
|---|---|---|
| committer | letouzey | 2007-11-01 16:57:15 +0000 |
| commit | 72a011e85063a8030f3f112a99e09c2390795b8d (patch) | |
| tree | c4faf86fb0f03ca02848606886961848f00a073f | |
| parent | 96da00b87ef2d4238fc550900e0c8f6762772810 (diff) | |
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
| -rw-r--r-- | theories/Init/Tactics.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 6c5c0e0119..61a6c8e77f 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 *. |