Merge branch 'ci/rodolphe/tactics' into 'master'

Add [iSelect], and various tactics based on it

See merge request iris/iris!625

CHANGELOG.md

@@ -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`:**
 

docs/proof_mode.md

@@ -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

iris/proofmode/ltac_tactics.v

@@ -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) ")"

tests/proofmode.ref

@@ -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.

tests/proofmode.v

@@ -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.