From 5334813e44dbafdd86d6edd36d5f8c7f7a37a9ff Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 20 Mar 2017 10:46:29 +0100
Subject: [PATCH] Show an interesting lemma about the core
---
theories/base_logic/lib/core.v | 11 ++++++++++-
1 file changed, 10 insertions(+), 1 deletion(-)
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index 4cf762d77..8376ee688 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -40,5 +40,14 @@ Section core.
Lemma coreP_elim P : PersistentP P → coreP P -∗ P.
Proof. rewrite /coreP. iIntros (?) "HCP". unshelve iApply ("HCP" $! P); auto. Qed.
-End core.
+ Lemma coreP_wand P Q :
+ (coreP P ⊢ Q) ↔ (P ⊢ □ Q).
+ Proof.
+ split.
+ - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
+ iClear "∗". iAlways. by iApply HP.
+ - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
+ iDestruct (coreP_elim with "HcQ") as "#HQ". done.
+ Qed.
+End core.
--
GitLab