core.v 994 Bytes
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
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.