Commit cf7c2c41 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'robbert/destruct_select' into 'master'

Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.

See merge request iris/stdpp!352
parents d9e55d3d 924782c8
...@@ -14,6 +14,7 @@ Coq 8.10 is no longer supported by this release. ...@@ -14,6 +14,7 @@ Coq 8.10 is no longer supported by this release.
- Rename `Is_true_false``Is_true_false_2` and `eq_None_ne_Some``eq_None_ne_Some_1`. - Rename `Is_true_false``Is_true_false_2` and `eq_None_ne_Some``eq_None_ne_Some_1`.
- Rename `decide_iff``decide_ext` and `bool_decide_iff``bool_decide_ext`. - Rename `decide_iff``decide_ext` and `bool_decide_iff``bool_decide_ext`.
- Remove a spurious `Global Arguments Pos.of_nat : simpl never`. - Remove a spurious `Global Arguments Pos.of_nat : simpl never`.
- Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.
The following `sed` script should perform most of the renaming The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`). (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
......
...@@ -55,6 +55,17 @@ Proof. intros ?. rename select nat into m. exists m. done. Qed. ...@@ -55,6 +55,17 @@ Proof. intros ?. rename select nat into m. exists m. done. Qed.
Goal (P : nat Prop), P 3 P 4 P 4. Goal (P : nat Prop), P 3 P 4 P 4.
Proof. intros P **. rename select (P _) into HP4. apply HP4. Qed. Proof. intros P **. rename select (P _) into HP4. apply HP4. Qed.
Goal P Q : Prop, True True P Q Q P.
Proof.
intros P Q ??. (* should select the last hypothesis *)
destruct select (_ _); by constructor.
Restart.
intros P Q ??. (* should select the last hypothesis *)
destruct select (_ _) as [H1|H2].
- right. exact H1.
- left. exact H2.
Qed.
(** Regression tests for [naive_solver]. *) (** Regression tests for [naive_solver]. *)
Lemma naive_solver_issue_115 (P : nat Prop) (x : nat) : Lemma naive_solver_issue_115 (P : nat Prop) (x : nat) :
( x', P x' x' = 10) P x x + 1 = 11. ( x', P x' x' = 10) P x x + 1 = 11.
......
...@@ -599,6 +599,11 @@ Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => rever ...@@ -599,6 +599,11 @@ Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => rever
Tactic Notation "rename" "select" open_constr(pat) "into" ident(name) := Tactic Notation "rename" "select" open_constr(pat) "into" ident(name) :=
select pat (fun H => rename H into name). select pat (fun H => rename H into name).
Tactic Notation "destruct" "select" open_constr(pat) :=
select pat (fun H => destruct H).
Tactic Notation "destruct" "select" open_constr(pat) "as" simple_intropattern(ipat) :=
select pat (fun H => destruct H as ipat).
(** The tactic [is_closed_term t] succeeds if [t] is a closed term and fails otherwise. (** The tactic [is_closed_term t] succeeds if [t] is a closed term and fails otherwise.
By closed we mean that [t] does not depend on any variable bound in the context. By closed we mean that [t] does not depend on any variable bound in the context.
axioms are considered closed terms by this tactic (but Section axioms are considered closed terms by this tactic (but Section
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment