core.v 1.27 KB
Newer Older
1
2
3
4
5
6
7
8
9
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 :=
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
10
  ( `(!PersistentP Q, P  Q), Q)%I.
11
12
13
14
15

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.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
26
27
28
29
30
31
32
33
  Global Instance coreP_mono : Proper (() ==> ()) (@coreP M).
  Proof.
    unfold coreP. iIntros (?? ENT) "H *". unshelve iApply ("H" $! Q). by etrans.
  Qed.

  Global Instance coreP_proper : Proper (() ==> ()) (@coreP M).
  Proof. intros ??. rewrite !equiv_spec=>-[A B]. split; rewrite ?A // ?B //. Qed.

Ralf Jung's avatar
Ralf Jung committed
34
  Lemma coreP_elim P : PersistentP P  coreP P - P.
35
  Proof.
Ralf Jung's avatar
Ralf Jung committed
36
    iIntros (?) "HCP". unshelve iApply ("HCP" $! P). iIntros "P". done.
37
38
39
  Qed.
End core.

40
Global Opaque coreP.