fancy_updates.v 9.63 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
Section fupd.
17
Context `{invG Σ}.
18 19
Implicit Types P Q : iProp Σ.

20 21 22
Global Instance fupd_ne E1 E2 : NonExpansive (fupd E1 E2).
Proof. rewrite uPred_fupd_eq. solve_proper. Qed.
Global Instance fupd_proper E1 E2 : Proper (() ==> ()) (fupd E1 E2).
23 24 25 26 27
Proof. apply ne_proper, _. Qed.

Lemma fupd_intro_mask E1 E2 P : E2  E1  P  |={E1,E2}=> |={E2,E1}=> P.
Proof.
  intros (E1''&->&?)%subseteq_disjoint_union_L.
28
  rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
29
  by iIntros "$ ($ & $ & HE) !> !> [$ $] !> !>" .
30 31
Qed.

32
Lemma except_0_fupd E1 E2 P :  (|={E1,E2}=> P) ={E1,E2}= P.
33
Proof. rewrite uPred_fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
34

35
Lemma bupd_fupd E P : (|==> P) ={E}= P.
36
Proof. rewrite uPred_fupd_eq. by iIntros ">? [$ $] !> !>". Qed.
37

38
Lemma fupd_mono E1 E2 P Q : (P  Q)  (|={E1,E2}=> P)  |={E1,E2}=> Q.
39
Proof.
40
  rewrite uPred_fupd_eq. iIntros (HPQ) "HP HwE". rewrite -HPQ. by iApply "HP".
41 42
Qed.

43
Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P)  |={E1,E3}=> P.
44
Proof.
45
  rewrite uPred_fupd_eq. iIntros "HP HwE".
46
  iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
47 48 49
Qed.

Lemma fupd_mask_frame_r' E1 E2 Ef P :
50
  E1 ## Ef  (|={E1,E2}=> E2 ## Ef  P) ={E1  Ef,E2  Ef}= P.
51
Proof.
52 53
  intros. rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //.
  iIntros "Hvs (Hw & HE1 &HEf)".
54
  iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
55
  iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
56
  iIntros "!> !>". by iApply "HP".
57 58
Qed.

59
Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P)  Q ={E1,E2}= P  Q.
60
Proof. rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros "[HwP $]". Qed.
61

62 63 64 65 66
Lemma fupd_plain' E1 E2 E2' P Q `{!Plain P} :
  E1  E2 
  (Q ={E1, E2'}= P) - (|={E1, E2}=> Q) ={E1}= (|={E1, E2}=> Q)  P.
Proof.
  iIntros ((E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
67
  rewrite uPred_fupd_eq /uPred_fupd_def ownE_op //. iIntros "H".
68 69 70 71 72 73 74 75
  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.
Qed.

Lemma later_fupd_plain E P `{!Plain P} : ( |={E}=> P) ={E}=   P.
Proof.
76
  rewrite uPred_fupd_eq /uPred_fupd_def. iIntros "HP [Hw HE]".
77 78 79 80
  iAssert (  P)%I with "[-]" as "#$"; last by iFrame.
  iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
Qed.

81
(** * Derived rules *)
82
Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (fupd E1 E2).
83 84
Proof. intros P Q; apply fupd_mono. Qed.
Global Instance fupd_flip_mono' E1 E2 :
85
  Proper (flip () ==> flip ()) (fupd E1 E2).
86 87
Proof. intros P Q; apply fupd_mono. Qed.

88
Lemma fupd_intro E P : P ={E}= P.
89
Proof. iIntros "HP". by iApply bupd_fupd. Qed.
90
Lemma fupd_intro_mask' E1 E2 : E2  E1  (|={E1,E2}=> |={E2,E1}=> True)%I.
91
Proof. exact: fupd_intro_mask. Qed.
92
Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=>  P) ={E1,E2}= P.
93
Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
94

95
Lemma fupd_frame_l E1 E2 P Q : (P  |={E1,E2}=> Q) ={E1,E2}= P  Q.
96
Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
97
Lemma fupd_wand_l E1 E2 P Q : (P - Q)  (|={E1,E2}=> P) ={E1,E2}= Q.
98
Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
99
Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}= Q.
100 101 102
Proof. by rewrite fupd_frame_r wand_elim_r. Qed.

Lemma fupd_trans_frame E1 E2 E3 P Q :
103
  ((Q ={E2,E3}= True)  |={E1,E2}=> (Q  P)) ={E1,E3}= P.
104 105 106 107 108 109
Proof.
  rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
  by rewrite fupd_frame_r left_id fupd_trans.
Qed.

Lemma fupd_mask_frame_r E1 E2 Ef P :
110
  E1 ## Ef  (|={E1,E2}=> P) ={E1  Ef,E2  Ef}= P.
111 112 113 114
Proof.
  iIntros (?) "H". iApply fupd_mask_frame_r'; auto.
  iApply fupd_wand_r; iFrame "H"; eauto.
Qed.
115
Lemma fupd_mask_mono E1 E2 P : E1  E2  (|={E1}=> P) ={E2}= P.
116 117 118 119
Proof.
  intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
Qed.

120
Lemma fupd_sep E P Q : (|={E}=> P)  (|={E}=> Q) ={E}= P  Q.
121
Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
122 123 124 125 126 127
Lemma fupd_big_sepL {A} E (Φ : nat  A  iProp Σ) (l : list A) :
  ([ list] kx  l, |={E}=> Φ k x) ={E}= [ list] kx  l, Φ k x.
Proof.
  apply (big_opL_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
128
Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K  A  iProp Σ) (m : gmap K A) :
129
  ([ map] kx  m, |={E}=> Φ k x) ={E}= [ map] kx  m, Φ k x.
130
Proof.
131
  apply (big_opM_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
132 133 134
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
Lemma fupd_big_sepS `{Countable A} E (Φ : A  iProp Σ) X :
135
  ([ set] x  X, |={E}=> Φ x) ={E}= [ set] x  X, Φ x.
136
Proof.
137
  apply (big_opS_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
138 139
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
140 141 142 143 144 145 146

Lemma fupd_plain E1 E2 P Q `{!Plain P} :
  E1  E2  (Q - P) - (|={E1, E2}=> Q) ={E1}= (|={E1, E2}=> Q)  P.
Proof.
  iIntros (HE) "HQP HQ". iApply (fupd_plain' _ _ E1 with "[HQP] HQ"); first done.
  iIntros "?". iApply fupd_intro. by iApply "HQP".
Qed.
147 148 149 150
End fupd.

(** Proofmode class instances *)
Section proofmode_classes.
151
  Context `{invG Σ}.
152 153 154 155 156 157
  Implicit Types P Q : iProp Σ.

  Global Instance from_pure_fupd E P φ : FromPure P φ  FromPure (|={E}=> P) φ.
  Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.

  Global Instance from_assumption_fupd E p P Q :
158
    FromAssumption p P (|==> Q)  FromAssumption p P (|={E}=> Q)%I.
159 160
  Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
161 162 163
  Global Instance into_wand_fupd E p q R P Q :
    IntoWand false false R P Q 
    IntoWand p q (|={E}=> R) (|={E}=> P) (|={E}=> Q).
164
  Proof.
165
    rewrite /IntoWand /= => HR. rewrite !affinely_persistently_if_elim HR.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
    apply wand_intro_l. by rewrite fupd_sep wand_elim_r.
167
  Qed.
168

Robbert Krebbers's avatar
Robbert Krebbers committed
169 170 171
  Global Instance into_wand_fupd_persistent E1 E2 p q R P Q :
    IntoWand false q R P Q  IntoWand p q (|={E1,E2}=> R) P (|={E1,E2}=> Q).
  Proof.
172
    rewrite /IntoWand /= => HR. rewrite affinely_persistently_if_elim HR.
Robbert Krebbers's avatar
Robbert Krebbers committed
173 174 175 176 177 178 179
    apply wand_intro_l. by rewrite fupd_frame_l wand_elim_r.
  Qed.

  Global Instance into_wand_fupd_args E1 E2 p q R P Q :
    IntoWand p false R P Q  IntoWand' p q R (|={E1,E2}=> P) (|={E1,E2}=> Q).
  Proof.
    rewrite /IntoWand' /IntoWand /= => ->.
180
    apply wand_intro_l. by rewrite affinely_persistently_if_elim fupd_wand_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
181 182 183 184 185
  Qed.

  Global Instance from_sep_fupd E P Q1 Q2 :
    FromSep P Q1 Q2  FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
  Proof. rewrite /FromSep =><-. apply fupd_sep. Qed.
186

Robbert Krebbers's avatar
Robbert Krebbers committed
187
  Global Instance from_or_fupd E1 E2 P Q1 Q2 :
188 189 190
    FromOr P Q1 Q2  FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
  Proof. rewrite /FromOr=><-. apply or_elim; apply fupd_mono; auto with I. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
191
  Global Instance from_exist_fupd {A} E1 E2 P (Φ : A  iProp Σ) :
192 193 194 195 196
    FromExist P Φ  FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
  Proof.
    rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
  Qed.

197 198
  Global Instance frame_fupd p E1 E2 R P Q :
    Frame p R P Q  Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
199 200
  Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.

201 202
  Global Instance is_except_0_fupd E1 E2 P : IsExcept0 (|={E1,E2}=> P).
  Proof. by rewrite /IsExcept0 except_0_fupd. Qed.
203

204 205
  Global Instance from_modal_fupd E P : FromModal (|={E}=> P) P.
  Proof. rewrite /FromModal. apply fupd_intro. Qed.
206

207
  Global Instance elim_modal_bupd_fupd E1 E2 P Q :
208
    ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
209 210
  Proof.
    by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
211
  Qed.
212
  Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
213
    ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
214
  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
215 216 217 218

  Global Instance add_modal_fupd E1 E2 P Q :
    AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
  Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
219 220
End proofmode_classes.

221
Hint Extern 2 (coq_tactics.envs_entails _ (|={_}=> _)) => iModIntro.
222 223 224 225 226 227

(** Fancy updates that take a step. *)

Section step_fupd.
Context `{invG Σ}.

228 229 230
Lemma step_fupd_wand E1 E2 P Q : (|={E1,E2}=> P) - (P - Q) - |={E1,E2}=> Q.
Proof. iIntros "HP HPQ". by iApply "HPQ". Qed.

231
Lemma step_fupd_mask_frame_r E1 E2 Ef P :
232
  E1 ## Ef  E2 ## Ef  (|={E1,E2}=> P)  |={E1  Ef,E2  Ef}=> P.
233 234 235 236 237 238 239 240 241
Proof.
  iIntros (??) "HP". iApply fupd_mask_frame_r. done. iMod "HP". iModIntro.
  iNext. by iApply fupd_mask_frame_r.
Qed.

Lemma step_fupd_mask_mono E1 E2 F1 F2 P :
  F1  F2  E1  E2  (|={E1,F2}=> P)  |={E2,F1}=> P.
Proof.
  iIntros (??) "HP".
242 243
  iMod (fupd_intro_mask') as "HM1"; first done. iMod "HP".
  iMod (fupd_intro_mask') as "HM2"; first done. iModIntro.
244
  iNext. iMod "HM2". iMod "HP". iMod "HM1". done.
245
Qed.
246 247 248

Lemma step_fupd_intro E1 E2 P : E2  E1   P - |={E1,E2}=> P.
Proof. iIntros (?) "HP". iApply (step_fupd_mask_mono E2 _ _ E2); auto. Qed.
249
End step_fupd.