Add case_match eqn: tactic for naming hypotheses generated by case_match

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`).

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.
 

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]. *)