core.v 1.87 KB
Newer Older
1
2
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
3
Set Default Proof Using "Type".
4
5
6
7
Import uPred.

(** The "core" of an assertion is its maximal persistent part.
    It can be defined entirely within the logic... at least
8
9
10
11
12
13
14
15
    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.
*)
16
17

Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
18
  ( `(!PersistentP Q), P  Q  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
19
20
Instance: Params (@coreP) 1.
Typeclasses Opaque coreP.
21
22
23
24
25

Section core.
  Context {M : ucmraT}.
  Implicit Types P Q : uPred M.

Ralf Jung's avatar
Ralf Jung committed
26
  Lemma coreP_intro P : P - coreP P.
27
  Proof. rewrite /coreP. iIntros "HP". by iIntros (Q HQ ->). Qed.
28

Ralf Jung's avatar
Ralf Jung committed
29
  Global Instance coreP_persistent P : PersistentP (coreP P).
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  Proof. rewrite /coreP. apply _. Qed.
31

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
32
33
  Global Instance coreP_mono : Proper (() ==> ()) (@coreP M).
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
    rewrite /coreP. iIntros (P P' ?) "H"; iIntros (Q ??).
35
    iApply ("H" $! Q with "[%]"). by etrans.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
36
37
38
  Qed.

  Global Instance coreP_proper : Proper (() ==> ()) (@coreP M).
Robbert Krebbers's avatar
Robbert Krebbers committed
39
  Proof. intros P Q. rewrite !equiv_spec=>-[??]. by split; apply coreP_mono. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
40

Ralf Jung's avatar
Ralf Jung committed
41
  Lemma coreP_elim P : PersistentP P  coreP P - P.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
  Proof. rewrite /coreP. iIntros (?) "HCP". unshelve iApply ("HCP" $! P); auto. Qed.
43

44
45
46
47
48
  Lemma coreP_wand P Q :
    (coreP P  Q)  (P   Q).
  Proof.
    split.
    - iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
Ralf Jung's avatar
Ralf Jung committed
49
      iAlways. by iApply HP.
50
51
52
53
    - iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
      iDestruct (coreP_elim with "HcQ") as "#HQ". done.
  Qed.
End core.