core.v 973 Bytes
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
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.

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

Ralf Jung's avatar
Ralf Jung committed
19
  Global Instance coreP_persistent P : PersistentP (coreP P).
20
21
22
23
24
25
  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.

Ralf Jung's avatar
Ralf Jung committed
26
  Lemma coreP_elim P : PersistentP P  coreP P - P.
27
  Proof.
Ralf Jung's avatar
Ralf Jung committed
28
    iIntros (?) "HCP". unshelve iApply ("HCP" $! P). iIntros "P". done.
29
30
31
32
33
  Qed.
End core.