Commit dd919077 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'msammler/select_tac' into 'master'

Added select and select_revert tactics

See merge request iris/stdpp!142
parents 2f540354 199d011d
......@@ -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
......@@ -520,6 +520,25 @@ Ltac find_pat pat tac :=
tryif tac x then idtac else fail 2
(** [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 *)
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
(** [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
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment