From 2bea47fca9a2a4d1303d2a915cd0f8c3ec4ec206 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 23 Apr 2022 23:29:23 +0200
Subject: [PATCH 1/4] `iRevert` of a pure hypotheses generates a wand instead
 of implication.

---
 iris/proofmode/coq_tactics.v  | 10 ++++++++--
 iris/proofmode/ltac_tactics.v |  5 ++++-
 2 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index a2708b041..060f818cd 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -170,8 +170,14 @@ Proof.
       rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
 Qed.
 
-Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → envs_entails Δ Q).
-Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
+Lemma tac_pure_revert Δ φ P Q :
+  FromAffinely P ⌜ φ ⌝ →
+  envs_entails Δ (P -∗ Q) →
+  (φ → envs_entails Δ Q).
+Proof.
+  rewrite /FromAffinely envs_entails_eq. intros <- -> ?.
+  by rewrite pure_True // affinely_True_emp affinely_emp left_id.
+Qed.
 
 (** * Intuitionistic *)
 Lemma tac_intuitionistic Δ i j p P P' Q :
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index f4da0ed78..b651b3fbf 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -651,7 +651,10 @@ Local Tactic Notation "iForallRevert" ident(x) :=
   first [let A := type of x in idtac|fail 1 "iRevert:" x "not in scope"];
   let A := type of x in
   lazymatch type of A with
-  | Prop => revert x; first [apply tac_pure_revert|err x]
+  | Prop =>
+     revert x; first
+       [eapply tac_pure_revert; [iSolveTC (* [FromAffinely], should never fail *)|]
+       |err x]
   | _ => revert x; first [apply tac_forall_revert|err x]
   end.
 
-- 
GitLab


From e440e51b6e00c3f6cff715f6753ba7e3c641048e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 23 Apr 2022 23:30:00 +0200
Subject: [PATCH 2/4] Tests.

---
 tests/proofmode.ref | 23 +++++++++++++++++++++++
 tests/proofmode.v   | 16 ++++++++++++++++
 2 files changed, 39 insertions(+)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index ce21d1c9d..58739cd69 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -396,6 +396,29 @@ No applicable tactic.
   "HQ" : Q
   --------------------------------------∗
   ▷ P ∗ Q
+"test_iRevert_pure"
+     : string
+1 goal
+  
+  PROP : bi
+  φ : Prop
+  P : PROP
+  ============================
+  "H" : <affine> ⌜φ⌝ -∗ P
+  --------------------------------------∗
+  <affine> ⌜φ⌝ -∗ P
+"test_iRevert_pure_affine"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  φ : Prop
+  P : PROP
+  ============================
+  "H" : ⌜φ⌝ -∗ P
+  --------------------------------------∗
+  ⌜φ⌝ -∗ P
 "elim_mod_accessor"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 8ad3f6da4..e83bd50bf 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1146,6 +1146,22 @@ Proof.
   iIntros (?) "HP HQ". iModIntro. Show. by iFrame.
 Qed.
 
+Check "test_iRevert_pure".
+Lemma test_iRevert_pure (φ : Prop) P :
+  φ → (<affine> ⌜ φ ⌝ -∗ P) -∗ P.
+Proof.
+  (* Check that iRevert creates a wand instead of an implication *)
+  iIntros (Hφ) "H". iRevert (Hφ). Show. done.
+Qed.
+
+Check "test_iRevert_pure_affine".
+Lemma test_iRevert_pure_affine `{!BiAffine PROP} (φ : Prop) P :
+  φ → (⌜ φ ⌝ -∗ P) -∗ P.
+Proof.
+  (* If the BI is affine, no affine modality should be added *)
+  iIntros (Hφ) "H". iRevert (Hφ). Show. done.
+Qed.
+
 End tests.
 
 Section parsing_tests.
-- 
GitLab


From 5f73bf42c53d5ca23890709be2bb1add966c9acb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 23 Apr 2022 23:36:24 +0200
Subject: [PATCH 3/4] CHANGELOG.

---
 CHANGELOG.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 518d58d5d..ac6566191 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,6 +21,7 @@ lemma.
    the conclusion. The old behavior can be emulated with`iExFalso. iExact "H".`
 * `iInduction` now supports induction schemes that involve `Forall` and
   `Forall2` (for example, for trees with finite branching).
+* `iRevert` of a pure hypothesis generates a wand instead of an implication.
 
 **Changes in `base_logic`:**
 
-- 
GitLab


From 83256c1d0a15b2ce1506dccbb79a969452feeb22 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 1 May 2022 17:21:46 +0000
Subject: [PATCH 4/4] Apply 1 suggestion(s) to 1 file(s)

---
 CHANGELOG.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ac6566191..10fbc83ae 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,7 +21,8 @@ lemma.
    the conclusion. The old behavior can be emulated with`iExFalso. iExact "H".`
 * `iInduction` now supports induction schemes that involve `Forall` and
   `Forall2` (for example, for trees with finite branching).
-* `iRevert` of a pure hypothesis generates a wand instead of an implication.
+* Change `iRevert` of a pure hypothesis to generate a magic wand instead of an
+  implication.
 
 **Changes in `base_logic`:**
 
-- 
GitLab