From ab64d3675ad1bfa4d7b5330268e1101886dde10d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 Apr 2024 14:08:29 +0200
Subject: [PATCH] add 'inv(ersion) select'

---
 CHANGELOG.md    |  2 ++
 stdpp/tactics.v | 12 ++++++++++++
 tests/tactics.v | 26 ++++++++++++++++++++++++--
 3 files changed, 38 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f18adbf9..cec2faf0 100644
--- a/CHANGELOG.md
+++ b/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`).
diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index 0d29cfe1..f3639f00 100644
--- a/stdpp/tactics.v
+++ b/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
diff --git a/tests/tactics.v b/tests/tactics.v
index bd7050ea..847bf3b9 100644
--- a/tests/tactics.v
+++ b/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. *)
-- 
GitLab