Skip to content
Snippets Groups Projects
Commit 3897126a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'ci/msammler/case_match_eqn' into 'master'

Add case_match eqn: tactic for naming hypotheses generated by case_match

See merge request iris/stdpp!388
parents ba7cf37b a6f215a9
No related branches found
No related tags found
No related merge requests found
......@@ -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`).
......
......@@ -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.
......
......@@ -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]. *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment