fancy_updates.v 2.16 KB
Newer Older
1
From iris.base_logic.lib Require Export own.
Ralf Jung's avatar
Ralf Jung committed
2
From stdpp Require Export coPset.
3
From iris.base_logic.lib Require Import wsat.
4
From iris.algebra Require Import gmap.
5
From iris.proofmode Require Import tactics classes.
6
Set Default Proof Using "Type".
7
Export invG.
8 9
Import uPred.

10 11 12 13 14 15
Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
  (wsat  ownE E1 ==  (wsat  ownE E2  P))%I.
Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed.
Instance uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux.
Definition uPred_fupd_eq `{invG Σ} : fupd = uPred_fupd_def := seal_eq uPred_fupd_aux.

16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43
Instance fupd_facts `{invG Σ} : FUpdFacts (uPredSI (iResUR Σ)).
Proof.
  split.
  - apply _.
  - rewrite uPred_fupd_eq. solve_proper.
  - intros E1 E2 P (E1''&->&?)%subseteq_disjoint_union_L.
    rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
      by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
  - rewrite uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>".
  - rewrite uPred_fupd_eq. iIntros (E1 E2 P) ">H [Hw HE]". iApply "H"; by iFrame.
  - rewrite uPred_fupd_eq. iIntros (E1 E2 P Q HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
  - rewrite uPred_fupd_eq. iIntros (E1 E2 E3 P) "HP HwE".
    iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
  - intros E1 E2 Ef P HE1Ef. rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
    iIntros "Hvs (Hw & HE1 &HEf)".
    iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
    iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
    iIntros "!> !>". by iApply "HP".
  - rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
  - iIntros (E1 E2 E2' P Q ? (E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
    rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
    iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
    iAssert ( P)%I as "#HP".
    { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
    iMod "HP". iFrame. auto.
  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P ?) "HP [Hw HE]".
    iAssert (  P)%I with "[-]" as "#$"; last by iFrame.
    iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
44
Qed.