Merge branch 'robbert/rewrite_pure_intro_pat' into 'master'

Consider intro pattern `IRewrite` (->/<-) to be intuitionistic

See merge request iris/iris!856

CHANGELOG.md

@@ -10,6 +10,12 @@ lemma.
 * Add a construction `bi_tc` to create transitive closures of
   PROP-level binary relations.
 
+**Changes in `proofmode`:**
+
+* The proof mode introduction patterns "<-" and "->" are considered
+  intuitionistic. This means that tactics such as `iDestruct ... as "->"` will
+  not dispose of hypotheses to perform the rewrite.
+
 ## Iris 4.0.0 (2022-08-18)
 
 The highlight of Iris 4.0 is the *later credits* mechanism, which provides a new

docs/proof_mode.md

@@ -162,11 +162,11 @@ Elimination of logical connectives
     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
-  hypothesis to be moved to the pure Coq context), then one can use all
-  hypotheses for proving the premises of `pm_trm`, as well as for proving the
-  resulting goal. Note that in this case the hypotheses still need to be
-  subdivided among the spatial premises.
+  to be moved to the intuitionistic context), with an `%` (which causes the
+  hypothesis to be moved to the pure Coq context), or with an `->`/`<-` (which
+  performs a rewrite), then one can use all hypotheses for proving the premises
+  of `pm_trm`, as well as for proving the resulting goal. Note that in this case
+  the hypotheses still need to be subdivided among the spatial premises.
 
 Separation logic-specific tactics
 ---------------------------------

iris/proofmode/intro_patterns.v

@@ -168,6 +168,7 @@ End intro_pat.
 Fixpoint intro_pat_intuitionistic (p : intro_pat) :=
   match p with
   | IPure _ => true
+  | IRewrite _ => true
   | IIntuitionistic _ => true
   | IList pps => forallb (forallb intro_pat_intuitionistic) pps
   | ISimpl => true

tests/proofmode.v

@@ -870,6 +870,15 @@ Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
   x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P.
 Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
 
+Lemma test_iDestruct_rewrite_not_consume P (x1 x2 : nat) :
+  (P -∗ ⌜ x1 = x2 ⌝) →
+  P -∗ ⌜ x1 = x2 ⌝ ∗ P.
+Proof.
+  iIntros (lemma) "HP". iDestruct (lemma with "HP") as "->".
+  auto. (* Make sure that "HP" has not been consumed; [auto] would fail
+  otherwise. *)
+Qed.
+
 Lemma test_iNext_affine `{!BiInternalEq PROP} P Q :
   <affine> ▷ (Q ≡ P) -∗ <affine> ▷ Q -∗ <affine> ▷ P.
 Proof. iIntros "#HPQ HQ !>". iNext. by iRewrite "HPQ" in "HQ". Qed.