core.v 1.65 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
Import uPred.

6
(** The "core" of an assertion is its maximal persistent part. *)
7
Definition coreP {M : ucmraT} (P : uPred M) : uPred M :=
8
  ( Q,  (Q   Q)   (P  Q)  Q)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10
Instance: Params (@coreP) 1.
Typeclasses Opaque coreP.
11
12
13
14
15

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

Ralf Jung's avatar
Ralf Jung committed
16
  Lemma coreP_intro P : P - coreP P.
17
  Proof. rewrite /coreP. iIntros "HP" (Q) "_ HPQ". by iApply "HPQ". Qed.
18

19
  Global Instance coreP_persistent P : Persistent (coreP P).
20
21
22
23
24
25
  Proof.
    rewrite /coreP /Persistent. iIntros "HC" (Q).
    iApply persistently_impl_plainly. iIntros "#HQ".
    iApply persistently_impl_plainly. iIntros "#HPQ".
    iApply "HQ". by iApply "HC".
  Qed.
26

27
28
29
30
31
  Global Instance coreP_ne : NonExpansive (@coreP M).
  Proof. solve_proper. Qed.
  Global Instance coreP_proper : Proper (() ==> ()) (@coreP M).
  Proof. solve_proper. Qed.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
32
33
  Global Instance coreP_mono : Proper (() ==> ()) (@coreP M).
  Proof.
34
35
    rewrite /coreP. iIntros (P P' HP) "H"; iIntros (Q) "#HQ #HPQ".
    iApply ("H" $! Q with "[]"); first done. by rewrite HP.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
36
37
  Qed.

38
  Lemma coreP_elim P : Persistent P  coreP P - P.
39
  Proof. rewrite /coreP. iIntros (?) "HCP". iApply ("HCP" $! P); auto. Qed.
40

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