fancy_updates.v 3.8 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 auth agree gset coPset.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
From iris.proofmode Require Import tactics.
6
Set Default Proof Using "Type".
7
Export invG.
8 9
Import uPred.

10 11 12
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.
13
Definition uPred_fupd `{invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
Robbert Krebbers's avatar
Robbert Krebbers committed
14
Definition uPred_fupd_eq `{invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
15
  uPred_fupd_aux.(seal_eq).
16

Robbert Krebbers's avatar
Robbert Krebbers committed
17
Lemma uPred_fupd_mixin `{invG Σ} : BiFUpdMixin (uPredSI (iResUR Σ)) uPred_fupd.
18 19 20 21 22
Proof.
  split.
  - rewrite uPred_fupd_eq. solve_proper.
  - intros E1 E2 P (E1''&->&?)%subseteq_disjoint_union_L.
    rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
    by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
24 25 26 27 28 29 30 31 32 33
  - 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 $]".
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35 36 37 38 39 40 41 42 43
Qed.
Instance uPred_bi_fupd `{invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
  {| bi_fupd_mixin := uPred_fupd_mixin |}.

Instance uPred_bi_bupd_fupd `{invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.

Instance uPred_bi_fupd_plainly `{invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
Proof.
  split.
44 45
  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P Q) "HQP HQ [Hw HE]".
    iAssert (  P)%I as "#>HP'".
46
    { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
47
    by iFrame.
48 49
  - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (p E1 E2 P) "HP [Hw HE]".
    iAssert (?p   P)%I with "[-]" as "#HP'"; last by (rewrite plainly_elim; iFrame).
50
    iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
51 52
Qed.

53
Lemma fupd_plain_soundness `{invPreG Σ} E (P: iProp Σ) `{!Plain P}:
54 55 56 57 58 59 60 61 62 63 64 65
  ( `{Hinv: invG Σ}, (|={, E}=> P)%I)  ( P)%I.
Proof.
  iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]".
  iPoseProof (Hfupd Hinv) as "H".
  rewrite uPred_fupd_eq /uPred_fupd_def.
  iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
Qed.

Lemma step_fupdN_soundness `{invPreG Σ} φ n :
  ( `{Hinv: invG Σ}, (|={, }=>^n |={, }=>  φ  : iProp Σ)%I) 
  φ.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
66 67 68 69
  intros Hiter.
  apply (soundness (M:=iResUR Σ) _  (S (S n))); simpl.
  apply (fupd_plain_soundness  _).
  intros Hinv. iPoseProof (Hiter Hinv) as "H".
70
  destruct n as [|n].
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
  - rewrite //=. iPoseProof (fupd_plain_strong with "H") as "H'".
    do 2 iMod "H'"; iModIntro; auto.
  - iPoseProof (step_fupdN_mono _ _ _ _ (|={}=>  ⌜φ⌝)%I with "H") as "H'".
    { iIntros "H". iMod (fupd_plain_strong with "H"); auto. }
    rewrite -step_fupdN_S_fupd.
    iMod (step_fupdN_plain with "H'") as "Hφ". iModIntro. iNext.
    rewrite -later_laterN laterN_later.
    iNext. by do 2 iMod "Hφ".
Qed.

Lemma step_fupdN_soundness' `{invPreG Σ} φ n :
  ( `{Hinv: invG Σ}, (|={, }=>^n  φ  : iProp Σ)%I)  
  φ.
Proof.
  iIntros (Hiter). eapply (step_fupdN_soundness _ n).
  iIntros (Hinv). iPoseProof (Hiter Hinv) as "Hiter".
  iApply (step_fupdN_mono with "Hiter").
  iIntros (?). iMod (fupd_intro_mask' _ ) as "_"; auto.
Qed.