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

Merge branch 'ralf/rename-by-pat' into 'master'

add rename-by-pattern tactic

See merge request iris/stdpp!218
parents 96cb4bc9 0710439b
No related branches found
No related tags found
No related merge requests found
......@@ -43,6 +43,8 @@ Coq 8.8 and 8.9 are no longer supported.
- Rename `seq_S_end_app` to `seq_S`. (The lemma `seq_S` is also in Coq's stdlib
since Coq 8.12.)
- Remove `omega` import and hint database in `tactics` file.
- Add `rename select <pat> into <name>` tactic to find a hypothesis by pattern
and give it a fixed name.
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
......
From stdpp Require Import tactics.
Goal forall P1 P2 P3 P4 (P: Prop),
Goal P1 P2 P3 P4 (P: Prop),
P1 (Is_true (P2 || P3)) P4
(P1 P)
(P2 P)
......@@ -12,7 +12,7 @@ Proof.
destruct_or? HH; [ exact (X1 HH) | exact (X2 HH) | exact (X3 HH) | exact (X4 HH) ].
Qed.
Goal forall P1 P2 P3 P4 (P: Prop),
Goal P1 P2 P3 P4 (P: Prop),
P1 P2
P3 P4
(P1 P3 P)
......@@ -25,7 +25,7 @@ Proof.
destruct_or?; [ exact (X1 HH1 HH2) | exact (X3 HH1 HH2) | exact (X2 HH1 HH2) | exact (X4 HH1 HH2) ].
Qed.
Goal forall P1 P2 P3 P4 (P: Prop),
Goal P1 P2 P3 P4 (P: Prop),
id (P1 P2)
id (P3 P4)
(P1 P3 P)
......@@ -41,10 +41,13 @@ Proof.
[ exact (X1 HH1 HH2) | exact (X2 HH1 HH2) | exact (X3 HH1 HH2) | exact (X4 HH1 HH2) ].
Qed.
Goal forall P1 P2 P3 P4,
Goal P1 P2 P3 P4,
P1 (Is_true (P2 && P3)) P4
P1 P2 P3.
Proof.
intros * HH. split_and!; [ destruct_and? HH; assumption | destruct_and?; assumption | ].
destruct_and?. Fail destruct_and!. assumption.
Qed.
Goal (n : nat), m : nat, True.
Proof. intros ?. rename select nat into m. exists m. done. Qed.
......@@ -537,6 +537,9 @@ Tactic Notation "select" open_constr(pat) tactic3(tac) :=
(** [select_revert] reverts the first hypothesis matching [pat]. *)
Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => revert H).
Tactic Notation "rename" "select" open_constr(pat) "into" ident(name) :=
select pat (fun H => rename H into name).
(** Coq's [firstorder] tactic fails or loops on rather small goals already. In
particular, on those generated by the tactic [unfold_elem_ofs] which is used
to solve propositions on sets. The [naive_solver] tactic implements an
......
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