merge

1 files changed, 43 insertions, 0 deletions

diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 8ddfecb5f..4559a1757 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -342,3 +342,46 @@ Ltac revert_last_nondep :=
   end.
 
 Ltac reverse_nondep := repeat revert_last_nondep.
+
+Ltac simplify_repeated_ifs_step :=
+  match goal with
+  | [ |- context G[if ?b then ?x else ?y] ]
+    => let x' := match x with
+                 | context x'[b] => let x'' := context x'[true] in x''
+                 end in
+       let G' := context G[if b then x' else y] in
+       cut G'; [ destruct b; exact (fun z => z) | cbv iota ]
+  | [ |- context G[if ?b then ?x else ?y] ]
+    => let y' := match y with
+                 | context y'[b] => let y'' := context y'[false] in y''
+                 end in
+       let G' := context G[if b then x else y'] in
+       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 | .. ]).