From 16c90c692cc90c64719e766f3a75977747144efd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 8 Mar 2018 13:53:22 +0100
Subject: [PATCH] Revert "Use implication in core so that we can test it.", add
 a dedicated test

This reverts commit daaabf410c1b32376a1059102975bca462787029.  We have tests for
testcase, we shouldn't depend on using arcane features in our definitions for
this purpose.  Also, this exposes that there still is a bug somewhere (see the
FIXME).
---
 theories/bi/lib/core.v     | 20 ++++++++++++++------
 theories/tests/proofmode.v |  4 ++++
 2 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/theories/bi/lib/core.v b/theories/bi/lib/core.v
index 3ad3caa5d..ce4ab4647 100644
--- a/theories/bi/lib/core.v
+++ b/theories/bi/lib/core.v
@@ -7,7 +7,9 @@ Import bi.
     i.e. the conjunction of all persistent assertions that are weaker
     than P (as in, implied by P). *)
 Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP :=
-  (∀ Q : PROP, ■ (Q -∗ <pers> Q) → ■ (P -∗ Q) → Q)%I.
+  (* TODO: Looks like we want notation for affinely-plainly; that lets us avoid
+  using conjunction/implication here. *)
+  (∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q)%I.
 Instance: Params (@coreP) 1.
 Typeclasses Opaque coreP.
 
@@ -16,14 +18,20 @@ Section core.
   Implicit Types P Q : PROP.
 
   Lemma coreP_intro P : P -∗ coreP P.
-  Proof. rewrite /coreP. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
+  Proof.
+    rewrite /coreP. iIntros "HP" (Q) "_ HPQ".
+    (* FIXME: Cannot apply HPQ directly. This works if we move it to the
+    persistent context, but why should we? *)
+    iDestruct (affinely_plainly_elim with "HPQ") as "HPQ".
+    by iApply "HPQ".
+  Qed.
 
   Global Instance coreP_persistent P : Persistent (coreP P).
   Proof.
     rewrite /coreP /Persistent. iIntros "HC" (Q).
-    iApply persistently_impl_plainly. iIntros "#HQ".
-    iApply persistently_impl_plainly. iIntros "#HPQ".
-    iApply "HQ". by iApply ("HC" with "[#] [#]").
+    iApply persistently_wand_affinely_plainly. iIntros "#HQ".
+    iApply persistently_wand_affinely_plainly. iIntros "#HPQ".
+    iApply "HQ". iApply "HC"; auto.
   Qed.
 
   Global Instance coreP_ne : NonExpansive (coreP (PROP:=PROP)).
@@ -35,7 +43,7 @@ Section core.
   Proof. solve_proper. Qed.
 
   Lemma coreP_elim P : Persistent P → coreP P -∗ P.
-  Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" with "[#] [#]"); auto. Qed.
+  Proof. rewrite /coreP. iIntros (?) "HCP". iApply "HCP"; auto. Qed.
 
   (* TODO: Can we generalize this to non-affine BIs? *)
   Lemma coreP_wand `{!BiAffine PROP} P Q : (coreP P ⊢ Q) ↔ (P ⊢ <pers> Q).
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 7c58ce313..c897f5dfa 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -419,4 +419,8 @@ Qed.
 Lemma test_iAssumption_False_no_loop : ∃ R, R ⊢ ∀ P, P.
 Proof. eexists. iIntros "?" (P). done. Qed.
 
+Lemma test_apply_affine_impl `{!BiPlainly PROP} (P : PROP) :
+  P -∗ (∀ Q : PROP, ■ (Q -∗ <pers> Q) → ■ (P -∗ Q) → Q).
+Proof. iIntros "HP" (Q) "_ #HPQ". by iApply "HPQ". Qed.
+
 End tests.
-- 
GitLab