diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-08 14:49:11 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-08 14:49:11 -0700 |
| commit | 0c687b54156b415684a78ae6d702f5efc41aca87 (patch) | |
| tree | c28a83ed67f69c362f606f8df4559e37237ebe7c /src/Util/Tactics.v | |
| parent | 23b0ea1c4e4ca01f82b1648933f312fba52a1bc7 (diff) | |
Add useful tactics and util lemmas
Diffstat (limited to 'src/Util/Tactics.v')
| -rw-r--r-- | src/Util/Tactics.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 304ae3c20..4630e4ab7 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -260,3 +260,30 @@ Ltac side_conditions_before_to_side_conditions_after tac_in H := here, after evars are instantiated, and not above. *) move H after H'; clear H' | .. ]. + +(** Do something with every hypothesis. *) +Ltac do_with_hyp' tac := + match goal with + | [ H : _ |- _ ] => tac H + end. + +(** Rewrite with any applicable hypothesis. *) +Tactic Notation "rewrite_hyp" "*" := do_with_hyp' ltac:(fun H => rewrite H). +Tactic Notation "rewrite_hyp" "->" "*" := do_with_hyp' ltac:(fun H => rewrite -> H). +Tactic Notation "rewrite_hyp" "<-" "*" := do_with_hyp' ltac:(fun H => rewrite <- H). +Tactic Notation "rewrite_hyp" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite !H). +Tactic Notation "rewrite_hyp" "->" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H). +Tactic Notation "rewrite_hyp" "<-" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H). +Tactic Notation "rewrite_hyp" "!*" := progress rewrite_hyp ?*. +Tactic Notation "rewrite_hyp" "->" "!*" := progress rewrite_hyp -> ?*. +Tactic Notation "rewrite_hyp" "<-" "!*" := progress rewrite_hyp <- ?*. + +Tactic Notation "rewrite_hyp" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite H in * ). +Tactic Notation "rewrite_hyp" "->" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite -> H in * ). +Tactic Notation "rewrite_hyp" "<-" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite <- H in * ). +Tactic Notation "rewrite_hyp" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite !H in * ). +Tactic Notation "rewrite_hyp" "->" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H in * ). +Tactic Notation "rewrite_hyp" "<-" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H in * ). +Tactic Notation "rewrite_hyp" "!*" "in" "*" := progress rewrite_hyp ?* in *. +Tactic Notation "rewrite_hyp" "->" "!*" "in" "*" := progress rewrite_hyp -> ?* in *. +Tactic Notation "rewrite_hyp" "<-" "!*" "in" "*" := progress rewrite_hyp <- ?* in *. |