Make the argument to `iEval` a selection pattern.

ProofMode.md

@@ -152,17 +152,19 @@ Rewriting / simplification
   equality in the proof mode goal / hypothesis `H`.
 - `iRewrite -pm_trm` / `iRewrite -pm_trm in "H"` : rewrite in reverse direction
   using an internal equality in the proof mode goal / hypothesis `H`.
-- `iEval (tac)` / `iEval (tac) in H` : performs a tactic `tac` on the proof mode
-  goal / hypothesis `H`. The tactic `tac` should be a reduction or rewriting
-  tactic like `simpl`, `cbv`, `lazy`, `rewrite` or `setoid_rewrite`. The `iEval`
-  tactic is implemented by running `tac` on `?evar ⊢ P` / `P ⊢ ?evar` where `P`
-  is the proof goal / hypothesis `H`. After running `tac`, `?evar` is unified
-  with the resulting `P`, which in turn becomes the new proof mode goal /
-  hypothesis `H`.
-  Note that parentheses around `tac` are needed.
-  If `H` is a list of hypothesis, then `iEval` will perform `tac` on each of them.
-- `iSimpl` / `iSimpl in H` : performs `simpl` on the proof mode goal /
-  hypothesis `H`. This is a shorthand for `iEval (simpl)`.
+- `iEval (tac)` / `iEval (tac) in "selpat"` : performs a tactic `tac`
+  on the proof mode goal / hypotheses given by the selection pattern
+  `selpat`. Using `%` as part of the selection pattern is unsupported.
+  The tactic `tac` should be a reduction or rewriting tactic like
+  `simpl`, `cbv`, `lazy`, `rewrite` or `setoid_rewrite`. The `iEval`
+  tactic is implemented by running `tac` on `?evar ⊢ P` / `P ⊢ ?evar`
+  where `P` is the proof goal / a hypothesis given by `selpat`. After
+  running `tac`, `?evar` is unified with the resulting `P`, which in
+  turn becomes the new proof mode goal / a hypothesis given by
+  `selpat`. Note that parentheses around `tac` are needed.
+- `iSimpl` / `iSimpl in "selpat"` : performs `simpl` on the proof mode
+  goal / hypotheses given by the selection pattern `selpat`. This is a
+  shorthand for `iEval (simpl)`.
 
 
 Iris

tests/proofmode.ref

@@ -111,6 +111,17 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   --------------------------------------∗
   ⌜S (S (S x)) = y⌝
   
+1 subgoal
+  
+  PROP : sbi
+  x, y, z : nat
+  ============================
+  "H1" : ⌜S (S (S x)) = y⌝
+  --------------------------------------□
+  "H2" : ⌜(1 + y)%nat = z⌝
+  --------------------------------------∗
+  ⌜S (S (S x)) = y⌝
+  
 "test_iFrame_later_1"
      : string
 1 subgoal

tests/proofmode.v

@@ -478,6 +478,11 @@ Lemma test_iSimpl_in_2 x y z :
   ⌜ S (S (S x)) = y ⌝ : PROP.
 Proof. iIntros "H1 H2". iSimpl in "H1 H2". Show. done. Qed.
 
+Lemma test_iSimpl_in3 x y z :
+  ⌜ (3 + x)%nat = y ⌝ -∗ ⌜ (1 + y)%nat = z ⌝ -∗
+  ⌜ S (S (S x)) = y ⌝ : PROP.
+Proof. iIntros "#H1 H2". iSimpl in "#". Show. done. Qed.
+
 Lemma test_iIntros_pure_neg : (⌜ ¬False ⌝ : PROP)%I.
 Proof. by iIntros (?). Qed.
 

theories/proofmode/ltac_tactics.v

@@ -107,40 +107,6 @@ Ltac iFresh :=
     constr:(IAnon n)
   end.
 
-(** * Simplification *)
-Tactic Notation "iEval" tactic(t) :=
-  iStartProof;
-  eapply tac_eval;
-    [let x := fresh in intros x; t; unfold x; reflexivity
-    |].
-
-Ltac iEval_go t Hs :=
-  match Hs with
-  | [] => idtac
-  | ?H :: ?Hs =>
-    let H := pretty_ident H in
-    eapply tac_eval_in with _ H _ _ _;
-      [pm_reflexivity || fail "iEval:" H "not found"
-      |let x := fresh in intros x; t; unfold x; reflexivity
-      |pm_reflexivity
-      |iEval_go t Hs]
-  end.
-
-Tactic Notation "iEval" tactic(t) "in" constr(H) :=
-  iStartProof;
-  let Hs := words H in iEval_go t Hs.
-
-Tactic Notation "iSimpl" := iEval (simpl).
-Tactic Notation "iSimpl" "in" constr(H) := iEval (simpl) in H.
-
-(* It would be nice to also have an `iSsrRewrite`, however, for this we need to
-pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
-
-  https://sympa.inria.fr/sympa/arc/coq-club/2018-01/msg00000.html
-
-PMP told me (= Robbert) in person that this is not possible with the current
-Ltac, but it may be possible in Ltac2. *)
-
 (** * Context manipulation *)
 Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
   eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
@@ -151,9 +117,12 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
      let H2 := pretty_ident H2 in
      fail "iRename:" H2 "not fresh"|].
 
+(** Elaborated selection patterns, unlike the type [sel_pat], contains
+only specific identifiers, and no wildcards like `#` (with the
+exception of the pure selection pattern `%`) *)
 Inductive esel_pat :=
   | ESelPure
-  | ESelIdent : bool → ident → esel_pat.
+  | ESelIdent : (* whether the ident is intuitionistic *) bool → ident → esel_pat.
 
 Local Ltac iElaborateSelPat_go pat Δ Hs :=
   lazymatch pat with
@@ -175,6 +144,8 @@ Local Ltac iElaborateSelPat_go pat Δ Hs :=
       fail "iElaborateSelPat:" H "not found"
     end
   end.
+(** Converts a selection pattern (given as a string) to a list of
+elaborated selection patterns. *)
 Ltac iElaborateSelPat pat :=
   lazymatch goal with
   | |- envs_entails ?Δ _ =>
@@ -204,6 +175,39 @@ Tactic Notation "iClear" constr(Hs) :=
 Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
   iClear Hs; clear xs.
 
+(** ** Simplification *)
+Tactic Notation "iEval" tactic(t) :=
+  iStartProof;
+  eapply tac_eval;
+    [let x := fresh in intros x; t; unfold x; reflexivity
+    |].
+
+Local Ltac iEval_go t Hs :=
+  lazymatch Hs with
+  | [] => idtac
+  | ESelPure :: ?Hs => fail "iEval: %: unsupported selection pattern"
+  | ESelIdent _ ?H :: ?Hs =>
+    eapply tac_eval_in with _ H _ _ _;
+      [pm_reflexivity || let H := pretty_ident H in fail "iEval:" H "not found"
+      |let x := fresh in intros x; t; unfold x; reflexivity
+      |pm_reflexivity
+      |iEval_go t Hs]
+  end.
+
+Tactic Notation "iEval" tactic(t) "in" constr(Hs) :=
+  iStartProof; let Hs := iElaborateSelPat Hs in iEval_go t Hs.
+
+Tactic Notation "iSimpl" := iEval (simpl).
+Tactic Notation "iSimpl" "in" constr(H) := iEval (simpl) in H.
+
+(* It would be nice to also have an `iSsrRewrite`, however, for this we need to
+pass arguments to Ssreflect's `rewrite` like `/= foo /bar` in Ltac, see:
+
+  https://sympa.inria.fr/sympa/arc/coq-club/2018-01/msg00000.html
+
+PMP told me (= Robbert) in person that this is not possible with the current
+Ltac, but it may be possible in Ltac2. *)
+
 (** * Assumptions *)
 Tactic Notation "iExact" constr(H) :=
   eapply tac_assumption with _ H _ _; (* (i:=H) *)