Add [especialize], [forward], [eforward]

At the request of Andres

1 files changed, 26 insertions, 0 deletions

diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index cca98c471..4559a1757 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -359,3 +359,29 @@ Ltac simplify_repeated_ifs_step :=
        cut G'; [ destruct b; exact (fun z => z) | cbv iota ]
   end.
 Ltac simplify_repeated_ifs := repeat simplify_repeated_ifs_step.
+
+(** Like [specialize] but allows holes that get filled with evars. *)
+Tactic Notation "especialize" open_constr(H) := specialize H.
+
+(** [forward H] specializes non-dependent binders in a hypothesis [H]
+    with side-conditions.  Side-conditions come after the main goal,
+    like with [replace] and [rewrite].
+
+    [eforward H] is like [forward H], but also specializes dependent
+    binders with evars.
+
+    Both tactics do nothing on hypotheses they cannot handle. *)
+Ltac forward_step H :=
+  match type of H with
+  | ?A -> ?B => let a := fresh in cut A; [ intro a; specialize (H a); clear a | ]
+  end.
+Ltac eforward_step H :=
+  match type of H with
+  | _ => forward_step H
+  | forall x : ?A, _
+    => let x_or_fresh := fresh x in
+       evar (x_or_fresh : A);
+       specialize (H x_or_fresh); subst x_or_fresh
+  end.
+Ltac forward H := try (forward_step H; [ forward H | .. ]).
+Ltac eforward H := try (eforward_step H; [ eforward H | .. ]).