From 48371b504295c8620d1d8e973b9b9ff750c5d6b6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 22 Dec 2016 10:46:39 +0100
Subject: [PATCH] Implement JH's idea of a "core of an assertion"
---
_CoqProject | 1 +
theories/base_logic/lib/core.v | 39 ++++++++++++++++++++++++++++++++++
2 files changed, 40 insertions(+)
create mode 100644 theories/base_logic/lib/core.v
diff --git a/_CoqProject b/_CoqProject
index e7841b5a0..6c5d46a47 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -84,6 +84,7 @@ theories/base_logic/lib/cancelable_invariants.v
theories/base_logic/lib/counter_examples.v
theories/base_logic/lib/fractional.v
theories/base_logic/lib/gen_heap.v
+theories/base_logic/lib/core.v
theories/program_logic/adequacy.v
theories/program_logic/lifting.v
theories/program_logic/weakestpre.v
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
new file mode 100644
index 000000000..910cbee7a
--- /dev/null
+++ b/theories/base_logic/lib/core.v
@@ -0,0 +1,39 @@
+From iris.base_logic Require Import base_logic.
+From iris.proofmode Require Import tactics.
+Import uPred.
+
+(** The "core" of an assertion is its maximal persistent part.
+ It can be defined entirely within the logic... at least
+ in the shallow embedding. *)
+
+Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
+ (∀ (Q : uPred M) `(!PersistentP Q, !P -∗ Q), Q)%I.
+
+Section core.
+ Context {M : ucmraT}.
+ Implicit Types P Q : uPred M.
+
+ Lemma coreP_intro P :
+ P -∗ coreP P.
+ Proof.
+ iIntros "HP". iIntros (Q HQ HPQ). by iApply HPQ.
+ Qed.
+
+ Global Instance coreP_persistent P :
+ PersistentP (coreP P).
+ Proof.
+ iIntros "HCP". iApply always_forall. iIntros (Q).
+ iApply always_forall. iIntros (HQ). iApply always_forall.
+ iIntros (HPQ). iApply HQ. unshelve iApply ("HCP" $! Q). done.
+ Qed.
+
+ Lemma corP_elim P :
+ PersistentP P → coreP P -∗ P.
+ Proof.
+ iIntros (?) "HCP". unshelve iApply ("HCP" $! P).
+ iIntros "P". done.
+ Qed.
+End core.
+
+
+
--
GitLab