add 'inv(ersion) select'

CHANGELOG.md

@@ -30,6 +30,8 @@ Coq 8.19 is newly supported by this version of std++.
 - Add lemma `join_app`.
 - Allow patterns and type annotations in `propset` notation, e.g.,
   `{[ (x, y) : nat * nat | x = y ]}`. (by Thibaut Pérami)
+- Add `inv select` and `inversion select` tactics that allow selecting the
+  to-be-inverted hypothesis with a pattern.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

stdpp/tactics.v

@@ -774,6 +774,9 @@ Tactic Notation "select" open_constr(pat) tactic3(tac) :=
       so then shelved goals are produced for every such evar. *)
   | H : pat |- _ => let T := (type of H) in unify T pat; tac H
   end.
+
+(** We provide [select] variants of some widely used tactics. *)
+
 (** [select_revert] reverts the first hypothesis matching [pat]. *)
 Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => revert H).
 
@@ -785,6 +788,15 @@ Tactic Notation "destruct" "select" open_constr(pat) :=
 Tactic Notation "destruct" "select" open_constr(pat) "as" simple_intropattern(ipat) :=
   select pat (fun H => destruct H as ipat).
 
+Tactic Notation "inversion" "select" open_constr(pat) :=
+  select pat (fun H => inversion H).
+Tactic Notation "inversion" "select" open_constr(pat) "as" simple_intropattern(ipat) :=
+  select pat (fun H => inversion H as ipat).
+Tactic Notation "inv" "select" open_constr(pat) :=
+  select pat (fun H => inv H).
+Tactic Notation "inv" "select" open_constr(pat) "as" simple_intropattern(ipat) :=
+  select pat (fun H => inv H as ipat).
+
 (** The tactic [is_closed_term t] succeeds if [t] is a closed term and fails otherwise.
 By closed we mean that [t] does not depend on any variable bound in the context.
 axioms are considered closed terms by this tactic (but Section

tests/tactics.v

@@ -79,13 +79,35 @@ Proof. intros P **. rename select (P _) into HP4. apply HP4. Qed.
 
 Goal ∀ P Q : Prop, True ∨ True → P ∨ Q → Q ∨ P.
 Proof.
-  intros P Q ??. (* should select the last hypothesis *)
+  intros P Q ??.
+  (* should select the last hypothesis *)
   destruct select (_ ∨ _); by constructor.
 Restart.
-  intros P Q ??. (* should select the last hypothesis *)
+  intros P Q ??.
+  (* should select the last hypothesis *)
   destruct select (_ ∨ _) as [H1|H2].
   - right. exact H1.
   - left. exact H2.
+Restart.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  inv select (_ ∨ _); by constructor.
+Restart.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  inv select (_ ∨ _) as [H1|H2].
+  - right. exact H1.
+  - left. exact H2.
+Restart.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  inversion select (_ ∨ _); by constructor.
+Restart.
+  intros P Q ??.
+  (* should select the last hypothesis *)
+  inversion select (_ ∨ _) as [H1|H2].
+  - right. exact H1.
+  - left. exact H2.
 Qed.
 
 (** [mk_evar] works on things that coerce to types. *)