aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-08-10 15:20:17 -0700
committerGravatar Jason Gross <jagro@google.com>2016-08-10 15:20:17 -0700
commiteaa9ff12d57aa82876036e04f128501c6c0b3afa (patch)
tree4268069185a1efa761c8b10e04cff6318d31cdab
parentcc62a73fda1cbf096ac7f5bfc23a5e1c868bc997 (diff)
Add [especialize], [forward], [eforward]
At the request of Andres
-rw-r--r--src/Util/Tactics.v26
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 | .. ]).