Commit daef264e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Port the core to use the plainness modality and prove it is non-expansive.

parent 25076b74
...@@ -3,19 +3,9 @@ From iris.proofmode Require Import tactics. ...@@ -3,19 +3,9 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Import uPred. Import uPred.
(** The "core" of an assertion is its maximal persistent part. (** The "core" of an assertion is its maximal persistent part. *)
It can be defined entirely within the logic... at least
in the shallow embedding.
WARNING: The function "coreP" is NOT NON-EXPANSIVE.
This is because the turnstile is not non-expansive as a function
from iProp to (discreteC Prop).
To obtain a core that's non-expansive, we would have to add another
modality to the logic: a box that removes access to *all* resources,
not just restricts access to the core.
*)
Definition coreP {M : ucmraT} (P : uPred M) : uPred M := Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
( `(!Persistent Q), P Q Q)%I. ( `(!Persistent Q), (P Q) Q)%I.
Instance: Params (@coreP) 1. Instance: Params (@coreP) 1.
Typeclasses Opaque coreP. Typeclasses Opaque coreP.
...@@ -24,25 +14,26 @@ Section core. ...@@ -24,25 +14,26 @@ Section core.
Implicit Types P Q : uPred M. Implicit Types P Q : uPred M.
Lemma coreP_intro P : P - coreP P. Lemma coreP_intro P : P - coreP P.
Proof. rewrite /coreP. iIntros "HP". by iIntros (Q HQ ->). Qed. Proof. rewrite /coreP. iIntros "HP". iIntros (Q HQ) "HPQ". by iApply "HPQ". Qed.
Global Instance coreP_persistent P : Persistent (coreP P). Global Instance coreP_persistent P : Persistent (coreP P).
Proof. rewrite /coreP. apply _. Qed. Proof. rewrite /coreP. apply _. Qed.
Global Instance coreP_ne : NonExpansive (@coreP M).
Proof. solve_proper. Qed.
Global Instance coreP_proper : Proper (() ==> ()) (@coreP M).
Proof. solve_proper. Qed.
Global Instance coreP_mono : Proper (() ==> ()) (@coreP M). Global Instance coreP_mono : Proper (() ==> ()) (@coreP M).
Proof. Proof.
rewrite /coreP. iIntros (P P' ?) "H"; iIntros (Q ??). rewrite /coreP. iIntros (P P' HP) "H"; iIntros (Q ?) "#HPQ".
iApply ("H" $! Q with "[%]"). by etrans. iApply ("H" $! Q with "[]"). by rewrite HP.
Qed. Qed.
Global Instance coreP_proper : Proper (() ==> ()) (@coreP M).
Proof. intros P Q. rewrite !equiv_spec=>-[??]. by split; apply coreP_mono. Qed.
Lemma coreP_elim P : Persistent P coreP P - P. Lemma coreP_elim P : Persistent P coreP P - P.
Proof. rewrite /coreP. iIntros (?) "HCP". unshelve iApply ("HCP" $! P); auto. Qed. Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" $! P); auto. Qed.
Lemma coreP_wand P Q : Lemma coreP_wand P Q : (coreP P Q) (P Q).
(coreP P Q) (P Q).
Proof. Proof.
split. split.
- iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP". - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment