Commit 6e94dcaa authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Ralf Jung
Browse files

Add [iSelect], and various tactics based on it

parent 79f2f36f
......@@ -116,6 +116,14 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
* Add notation `¬ P` for `P → False` to `bi_scope`.
* Add Coq side-condition `φ` to class `ElimAcc` (similar to what we already had
for `ElimInv` and `ElimModal`).
* Add a tactic `iSelect pat tac` (similar to `select` in std++) which runs the
tactic `tac H` with the name `H` of the last hypothesis of the intuitionistic
or spatial context matching `pat`. `iSelect` is used to implement:
+ `iRename select (pat)%I into name` which renames the matching hypothesis,
+ `iDestruct select (pat)%I as ...` which destructs the matching hypothesis,
+ `iClear select (pat)%I` which clears the matching hypothesis,
+ `iRevert select (pat)%I` which reverts the matching hypothesis,
+ `iFrame select (pat)%I` which cancels the matching hypothesis.
**Changes in `base_logic`:**
......
......@@ -66,11 +66,18 @@ Context management
mode [introduction patterns][ipat] `ipat1 ... ipatn`.
- `iClear (x1 ... xn) "selpat"` : clear the hypotheses given by the [selection
pattern][selpat] `selpat` and the Coq level hypotheses/variables `x1 ... xn`.
- `iClear select (pat)%I` : clear the last hypothesis of the intuitionistic
or spatial context that matches pattern `pat`.
- `iRevert (x1 ... xn) "selpat"` : revert the hypotheses given by the [selection
pattern][selpat] `selpat` into wands, and the Coq level hypotheses/variables
`x1 ... xn` into universal quantifiers. Intuitionistic hypotheses are wrapped
into the intuitionistic modality.
- `iRevert select (pat)%I` : revert the last hypothesis of the intuitionistic
or spatial context that matches pattern `pat`.
- `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
- `iRename select (pat)%I into "H"` : rename the last hypothesis of the
intuitionistic or spatial context that matches pattern `pat` into `H`. This
is particularly useful to give a name to an anonymous hypothesis.
- `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
implications/wands of a hypothesis `pm_trm`. See [proof mode terms][pm-trm] below.
- `iSpecialize pm_trm as #` : instantiate universal quantifiers and eliminate
......@@ -81,19 +88,23 @@ Context management
destruct it using the [introduction pattern][ipat] `ipat`. This tactic is
essentially the same as `iDestruct` with the difference that `pm_trm` is not
thrown away if possible.
- `iAssert P with "spat" as "H"` : generate a new subgoal `P` and add the
- `iAssert (P)%I with "spat" as "H"` : generate a new subgoal `P` and add the
hypothesis `P` to the current goal as `H`. The [specialization pattern][spat] `spat`
specifies which hypotheses will be consumed by proving `P`.
+ `iAssert P with "spat" as "ipat"` : like the above, but immediately destruct
+ `iAssert (P)%I with "spat" as "ipat"` : like the above, but immediately destruct
the generated hypothesis using the [introduction pattern][ipat] `ipat`. If `ipat`
is "intuitionistic" (most commonly, it starts with `#` or `%`), then all spatial
hypotheses are available in both the subgoal for `P` as well as the current
goal. An `ipat` is considered intuitionistic if all branches start with a
`#` (which causes `P` to be moved to the intuitionistic context) or with a
`%` (which causes `P` to be moved to the pure Coq context).
+ `iAssert P as %cpat` : assert `P` and destruct it using the Coq introduction
+ `iAssert (P)%I as %cpat` : assert `P` and destruct it using the Coq introduction
pattern `cpat`. All hypotheses can be used for proving `P` as well as for
proving the current goal.
- `iSelect (pat)%I tac` : run the tactic `tac H`, where `H` is the name of the
last hypothesis in the intuitionistic or spatial hypothesis context that
matches pattern `pat`. There is no backtracking to select the next hypothesis
in case `tac H` fails.
Introduction of logical connectives
-----------------------------------
......@@ -146,6 +157,9 @@ Elimination of logical connectives
for proving the resulting goal.
+ `iDestruct num as (x1 ... xn) "ipat"` / `iDestruct num as %cpat` :
introduce `num : nat` hypotheses and destruct the last introduced hypothesis.
+ `iDestruct select (pat)%I as ...` is the same as `iDestruct "H" as ...`,
where `H` is the name of the last hypothesis of the intuitionistic or
spatial context matching pattern `pat`.
In case all branches of `ipat` start with a `#` (which causes the hypothesis
to be moved to the intuitionistic context) or with an `%` (which causes the
......@@ -167,6 +181,8 @@ Separation logic-specific tactics
Notice that framing spatial hypotheses makes them disappear, but framing Coq
or intuitionistic hypotheses does not make them disappear.
This tactic solves the goal if everything in the conclusion has been framed.
- `iFrame select (pat)%I` : cancel the last hypothesis of the intuitionistic
of spatial context that matches pattern `pat`.
- `iCombine "H1 H2" as "ipat"` : combine `H1 : P1` and `H2 : P2` into `H: P1 ∗
P2` or something simplified but equivalent, then destruct the combined
hypthesis using `ipat`. Some examples of simplifications `iCombine` knows
......
......@@ -64,6 +64,19 @@ Tactic Notation "iMatchHyp" tactic1(tac) :=
| |- context[ environments.Esnoc _ ?x ?P ] => tac x P
end.
Tactic Notation "iSelect" open_constr(pat) tactic1(tac) :=
lazymatch goal with
| |- context[ environments.Esnoc _ ?x pat ] =>
(* Before runnig [tac] on the hypothesis name [x] we must first unify the
pattern [pat] with the term it matched against. This forces every evar
coming from [pat] (and in particular from the [_] it contains and from
the implicit arguments it uses) to be instantiated. If we do not do so
then shelved goals are produced for every such evar. *)
lazymatch iTypeOf x with
| Some (_,?T) => unify T pat; tac x
end
end.
(** * Start a proof *)
Tactic Notation "iStartProof" :=
lazymatch goal with
......@@ -141,6 +154,9 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
| _ => idtac (* subgoal *)
end].
Tactic Notation "iRename" "select" open_constr(pat) "into" constr(n) :=
iSelect pat ltac:(fun H => iRename H into n).
(** Elaborated selection patterns, unlike the type [sel_pat], contains
only specific identifiers, and no wildcards like `#` (with the
exception of the pure selection pattern `%`) *)
......@@ -199,6 +215,9 @@ Tactic Notation "iClear" constr(Hs) :=
Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
iClear Hs; clear xs.
Tactic Notation "iClear" "select" open_constr(pat) :=
iSelect pat ltac:(fun H => iClear H).
(** ** Simplification *)
Tactic Notation "iEval" tactic3(t) :=
iStartProof;
......@@ -454,6 +473,9 @@ Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
constr(t5) constr(t6) constr(t7) constr(t8)")" constr(Hs) :=
iFramePure t1; iFrame ( t2 t3 t4 t5 t6 t7 t8 ) Hs.
Tactic Notation "iFrame" "select" open_constr(pat) :=
iSelect pat ltac:(fun H => iFrame H).
(** * Basic introduction tactics *)
Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
(* In the case the goal starts with an [let x := _ in _], we do not
......@@ -737,6 +759,9 @@ Tactic Notation "iRevert" "(" ident(x1) ident(x2) ident(x3) ident(x4)
ident(x11) ident(x12) ident(x13) ident(x14) ident(x15) ")" constr(Hs) :=
iRevert Hs; iRevert ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ).
Tactic Notation "iRevert" "select" open_constr(pat) :=
iSelect pat ltac:(fun H => iRevert H).
(** * The specialize and pose proof tactics *)
Record iTrm {X As S} :=
ITrm { itrm : X ; itrm_vars : hlist As ; itrm_hyps : S }.
......@@ -2083,6 +2108,62 @@ Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
iDestructCore lem as true (fun H => iPure H as pat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" constr(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "("
simple_intropattern(x1) ")" constr(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as ( x1 ) ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "("
simple_intropattern(x1) simple_intropattern(x2) ")" constr(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as ( x1 x2 ) ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "("
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
")" constr(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as ( x1 x2 x3 ) ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "("
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) ")" constr(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as ( x1 x2 x3 x4 ) ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "("
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) ")" constr(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as ( x1 x2 x3 x4 x5 ) ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "("
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
")" constr(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as ( x1 x2 x3 x4 x5 x6 ) ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "("
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
simple_intropattern(x7) ")" constr(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 ) ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "("
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
simple_intropattern(x7) simple_intropattern(x7) ")" constr(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 ) ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "("
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
simple_intropattern(x7) simple_intropattern(x7) simple_intropattern(x8)
")" constr(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "("
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
simple_intropattern(x7) simple_intropattern(x7) simple_intropattern(x8)
simple_intropattern(x9) ")" constr(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 x9 ) ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "("
simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) simple_intropattern(x5) simple_intropattern(x6)
simple_intropattern(x7) simple_intropattern(x7) simple_intropattern(x8)
simple_intropattern(x9) simple_intropattern(x10) ")" constr(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ) ipat).
Tactic Notation "iDestruct" "select" open_constr(pat) "as" "%" simple_intropattern(ipat) :=
iSelect pat ltac:(fun H => iDestruct H as % ipat).
Tactic Notation "iPoseProof" open_constr(lem) "as" constr(pat) :=
iPoseProofCore lem as pat (fun H => iDestructHyp H as pat).
Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
......
......@@ -725,3 +725,15 @@ Tactic failure: iLöb: no 'BiLöb' instance found.
: string
The command has indeed failed with message:
H is already used.
"test_iRename_select1"
: string
The command has indeed failed with message:
No matching clauses for match.
"test_iDestruct_select2"
: string
The command has indeed failed with message:
Tactic failure: iPure: (φ n) not pure.
"test_iDestruct_select_no_backtracking"
: string
The command has indeed failed with message:
Tactic failure: iIntuitionistic: Q not persistent.
......@@ -1386,3 +1386,115 @@ Proof.
Abort.
End pure_name_tests.
Section tactic_tests.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Implicit Types φ : nat PROP.
Implicit Types Ψ : nat nat PROP.
Check "test_iRename_select1".
Lemma test_iRename_select1 P Q :
(P - Q) - P - Q.
Proof.
iIntros "#? #?".
iRename select P into "H1".
(* The following fails since there are no matching hypotheses. *)
Fail iRename select (_ _)%I into "?".
iRename select (_ - _)%I into "H2".
iDestruct ("H2" with "H1") as "$".
Qed.
Lemma test_iRename_select2 P Q :
(P - Q) - P - Q.
Proof.
iIntros "??".
iRename select P into "H1".
iRename select (_ - _)%I into "H2".
by iApply "H2".
Qed.
Lemma test_iDestruct_select1 P Q :
(P Q) - Q P.
Proof.
iIntros "?".
iDestruct select (_ _)%I as "[$ $]".
Qed.
Check "test_iDestruct_select2".
Lemma test_iDestruct_select2 φ P :
( x, P φ x) - x, φ x P.
Proof.
iIntros "?".
(* The following fails since [Φ n] is not pure. *)
Fail iDestruct select ( _, _)%I as (n) "[H1 %]".
iDestruct select ( _, _)%I as (n) "[H1 H2]".
iExists n. iFrame.
Qed.
Lemma test_iDestruct_select3 Ψ P :
( x y, P Ψ x y) - x y, Ψ x y P.
Proof.
iIntros "?".
iDestruct select ( _, _)%I as (n m) "[H1 H2]".
iExists n, m. iFrame.
Qed.
Lemma test_iDestruct_select4 φ :
( x, φ x) - ( x, φ x).
Proof.
iIntros "#?".
iDestruct select ( _, _)%I as (n) "H".
by iExists n.
Qed.
Lemma test_iDestruct_select5 (φ : nat Prop) P :
P - n, φ n - n, P ⌜φ n ⌜φ n.
Proof.
iIntros "??".
iDestruct select _%I as %[n H].
iExists n. iFrame. by iSplit.
Qed.
Check "test_iDestruct_select_no_backtracking".
Lemma test_iDestruct_select_no_backtracking P Q :
P - Q - Q.
Proof.
iIntros "??".
(* The following must fail since the pattern will match [Q], which cannot be
introduced in the intuitionistic context. This demonstrates that tactics
based on [iSelect] only act on the last hypothesis of the intuitionistic
or spatial context that matches the pattern, and they do not backtrack if
the requested action fails on the hypothesis. *)
Fail iDestruct select _ as "#X".
done.
Qed.
Lemma test_iDestruct_select_several_match P Q R :
P - Q - R - R.
Proof.
iIntros "???".
(* This demonstrates that the last matching hypothesis is used for all the
tactics based on [iSelect]. *)
iDestruct select ( _)%I as "$".
Qed.
Lemma test_iRevert_select_iClear_select P Q R :
P - Q - R - R.
Proof.
iIntros "???".
iClear select ( P)%I.
iRevert select _.
iClear select _.
iIntros "$".
Qed.
Lemma test_iFrame_select P Q R :
P - (Q R) - P Q R.
Proof.
iIntros "??".
iFrame select (_ _)%I.
iFrame select _.
Qed.
End tactic_tests.
Markdown is supported
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