From 609de3aaafdc16ab9e6075619afffc7352a33d2b Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 20 Jan 2021 12:03:23 +0100 Subject: [PATCH 1/2] add rename-by-pattern tactic --- CHANGELOG.md | 2 ++ tests/tactics.v | 3 +++ theories/tactics.v | 3 +++ 3 files changed, 8 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index e8d13a8e..cb181a52 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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`): diff --git a/tests/tactics.v b/tests/tactics.v index a606dbce..86953761 100644 --- a/tests/tactics.v +++ b/tests/tactics.v @@ -48,3 +48,6 @@ Proof. intros * HH. split_and!; [ destruct_and? HH; assumption | destruct_and?; assumption | ]. destruct_and?. Fail destruct_and!. assumption. Qed. + +Goal forall (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 b635bdf7..c1ac9116 100644 --- a/theories/tactics.v +++ b/theories/tactics.v @@ -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 -- GitLab From 0710439b2f4f24010e222c9d620b75790e6f98c3 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 20 Jan 2021 12:30:01 +0100 Subject: [PATCH 2/2] fmt --- tests/tactics.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/tactics.v b/tests/tactics.v index 86953761..c2170c89 100644 --- a/tests/tactics.v +++ b/tests/tactics.v @@ -1,6 +1,6 @@ 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,7 +41,7 @@ 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. @@ -49,5 +49,5 @@ Proof. destruct_and?. Fail destruct_and!. assumption. Qed. -Goal forall (n : nat), ∃ m : nat, True. +Goal ∀ (n : nat), ∃ m : nat, True. Proof. intros ?. rename select nat into m. exists m. done. Qed. -- GitLab