From a6f215a9eb65e5341bbb9a3554d338cbdad7b54a Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Tue, 26 Jul 2022 16:00:05 +0200
Subject: [PATCH] Add case_match eqn: tactic for naming hypotheses generated by
 case_match

---
 CHANGELOG.md       |  2 ++
 tests/tactics.v    | 16 ++++++++++++++++
 theories/tactics.v |  9 ++++++---
 3 files changed, 24 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e67fcf4d..beadd84c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -24,6 +24,8 @@ Coq 8.11 is no longer supported.
 - Rename `map_disjoint_subseteq` → `kmap_subseteq` and
   `map_disjoint_subset` → `kmap_subset`.
 - Add `map_Exists` as an analogue to `map_Forall`. (by Michael Sammler)
+- Add `case_match eqn:H` that behaves like `case_match` but allows naming the
+  generated equality. (by Michael Sammler)
 
 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/tests/tactics.v b/tests/tactics.v
index 65b56cfd..8272a640 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -49,6 +49,22 @@ Proof.
   destruct_and?. Fail destruct_and!. assumption.
 Qed.
 
+(** Tests for [case_match] *)
+Goal ∀ n : nat, match n with | 0 => n = 0 | S n' => n = S n' end.
+Proof.
+  intros. by case_match.
+Restart.
+  intros. by case_match eqn:Heq; revert Heq. (* [revert Heq] checks that [Heq] exists *)
+Qed.
+
+Goal ∀ n m : nat, match n with | 0 => m = 0 | S n' => m = S n' end → n = m.
+Proof.
+  intros. by case_match.
+Restart.
+  intros. by case_match eqn:Heq; revert Heq. (* [revert Heq] checks that [Heq] exists *)
+Qed.
+
+(** Tests for [select] tactics *)
 Goal ∀ (n : nat), ∃ m : nat, True.
 Proof. intros ?. rename select nat into m. exists m. done. Qed.
 
diff --git a/theories/tactics.v b/theories/tactics.v
index 79a5be44..d4c143a6 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -163,11 +163,14 @@ Tactic Notation "destruct_or" "!" :=
 (** The tactic [case_match] destructs an arbitrary match in the conclusion or
 assumptions, and generates a corresponding equality. This tactic is best used
 together with the [repeat] tactical. *)
-Ltac case_match :=
+Tactic Notation "case_match" "eqn" ":" ident(Hd) :=
   match goal with
-  | H : context [ match ?x with _ => _ end ] |- _ => destruct x eqn:?
-  | |- context [ match ?x with _ => _ end ] => destruct x eqn:?
+  | H : context [ match ?x with _ => _ end ] |- _ => destruct x eqn:Hd
+  | |- context [ match ?x with _ => _ end ] => destruct x eqn:Hd
   end.
+Ltac case_match :=
+  let H := fresh in case_match eqn:H.
+
 
 (** The tactic [unless T by tac_fail] succeeds if [T] is not provable by
 the tactic [tac_fail]. *)
-- 
GitLab