From 199d011d354a602f1a8cf12acc899ce66b8fddf2 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 9 Apr 2020 10:19:23 +0200
Subject: [PATCH] Added select and select_revert tactics
---
CHANGELOG.md | 2 ++
theories/tactics.v | 19 +++++++++++++++++++
2 files changed, 21 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index bab4bf9a..231e356f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,8 @@ API-breaking change is listed.
## std++ master
+- Added the `select` and `revert select` tactics for selecting and
+ reverting a hypothesis based on a pattern.
- Extracted `list_numbers.v` from `list.v` and `numbers.v` for
functions, which operate on lists of numbers (`seq`, `seqZ`,
`sum_list(_with)` and `max_list(_with)`). `list_numbers.v` is
diff --git a/theories/tactics.v b/theories/tactics.v
index 55da19a4..5fd8ee7e 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -520,6 +520,25 @@ Ltac find_pat pat tac :=
tryif tac x then idtac else fail 2
end.
+
+(** [select] finds the first hypothesis matching [pat] and passes it
+to the continuation [tac]. Its main advantage over using [match goal
+with ] directly is that it is shorter. If [pat] matches multiple
+hypotheses, then [tac] will only be called on the first matching
+hypothesis. If [tac] fails, [select] will not backtrack on subsequent
+matching hypotheses.
+
+[select] is written in CPS and does not return the name of the
+hypothesis due to limitations in the Ltac1 tactic runtime (see
+https://gitter.im/coq/coq?at=5e96c82f85b01628f04bbb89). *)
+Tactic Notation "select" open_constr(pat) tactic(tac) :=
+ lazymatch goal with
+ (* The [unify] is necessary, otherwise holes in [pat] stay as side-conditions *)
+ | H : pat |- _ => let T := (type of H) in unify T pat; tac H
+ end.
+(** [select_revert] reverts the first hypothesis matching [pat]. *)
+Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => revert H).
+
(** Coq's [firstorder] tactic fails or loops on rather small goals already. In
particular, on those generated by the tactic [unfold_elem_ofs] which is used
to solve propositions on sets. The [naive_solver] tactic implements an
--
GitLab