updates.v 13.4 KB
Newer Older
1
From stdpp Require Import coPset.
2
From iris.bi Require Import interface derived_laws_sbi big_op plainly.
3
Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
4

Robbert Krebbers's avatar
Robbert Krebbers committed
5 6
(* We first define operational type classes for the notations, and then later
bundle these operational type classes with the laws. *)
7
Class BUpd (PROP : Type) : Type := bupd : PROP  PROP.
8
Instance : Params (@bupd) 2.
9
Hint Mode BUpd ! : typeclass_instances.
10

11 12 13
Notation "|==> Q" := (bupd Q) : bi_scope.
Notation "P ==∗ Q" := (P  |==> Q) (only parsing) : stdpp_scope.
Notation "P ==∗ Q" := (P - |==> Q)%I : bi_scope.
14

15
Class FUpd (PROP : Type) : Type := fupd : coPset  coPset  PROP  PROP.
16
Instance: Params (@fupd) 4.
17
Hint Mode FUpd ! : typeclass_instances.
18

Ralf Jung's avatar
Ralf Jung committed
19 20 21
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q)%I : bi_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P - |={E1,E2}=> Q) : stdpp_scope.
22

Ralf Jung's avatar
Ralf Jung committed
23 24 25
Notation "|={ E }=> Q" := (fupd E E Q) : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)%I : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q) : stdpp_scope.
26 27

(** Fancy updates that take a step. *)
28 29 30 31
Notation "|={ E1 , E2 , E3 }▷=> Q" := (|={E1,E2}=> ( |={E2,E3}=> Q))%I : bi_scope.
Notation "P ={ E1 , E2 , E3 }▷=∗ Q" := (P - |={ E1,E2,E3 }=> Q)%I : bi_scope.
Notation "|={ E1 , E2 }▷=> Q" := (|={E1,E2,E1}=> Q)%I : bi_scope.
Notation "P ={ E1 , E2 }▷=∗ Q" := (P - |={ E1 , E2, E1 }=> Q)%I : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
32 33
Notation "|={ E }▷=> Q" := (|={E,E}=> Q)%I : bi_scope.
Notation "P ={ E }▷=∗ Q" := (P ={E,E}= Q)%I : bi_scope.
34

Robbert Krebbers's avatar
Robbert Krebbers committed
35
(** Bundled versions  *)
Robbert Krebbers's avatar
Robbert Krebbers committed
36
(* Mixins allow us to create instances easily without having to use Program *)
Robbert Krebbers's avatar
Robbert Krebbers committed
37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66
Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
  bi_bupd_mixin_bupd_ne : NonExpansive bupd;
  bi_bupd_mixin_bupd_intro (P : PROP) : P == P;
  bi_bupd_mixin_bupd_mono (P Q : PROP) : (P  Q)  (|==> P) == Q;
  bi_bupd_mixin_bupd_trans (P : PROP) : (|==> |==> P) == P;
  bi_bupd_mixin_bupd_frame_r (P R : PROP) : (|==> P)  R == P  R;
}.

Record BiFUpdMixin (PROP : sbi) `(FUpd PROP) := {
  bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd E1 E2);
  bi_fupd_mixin_fupd_intro_mask E1 E2 (P : PROP) : E2  E1  P  |={E1,E2}=> |={E2,E1}=> P;
  bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) :  (|={E1,E2}=> P) ={E1,E2}= P;
  bi_fupd_mixin_fupd_mono E1 E2 (P Q : PROP) : (P  Q)  (|={E1,E2}=> P)  |={E1,E2}=> Q;
  bi_fupd_mixin_fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P)  |={E1,E3}=> P;
  bi_fupd_mixin_fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
    E1 ## Ef  (|={E1,E2}=> E2 ## Ef  P) ={E1  Ef,E2  Ef}= P;
  bi_fupd_mixin_fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P)  Q ={E1,E2}= P  Q;
}.

Class BiBUpd (PROP : bi) := {
  bi_bupd_bupd :> BUpd PROP;
  bi_bupd_mixin : BiBUpdMixin PROP bi_bupd_bupd;
}.
Hint Mode BiBUpd ! : typeclass_instances.
Arguments bi_bupd_bupd : simpl never.

Class BiFUpd (PROP : sbi) := {
  bi_fupd_fupd :> FUpd PROP;
  bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
}.
67
Hint Mode BiFUpd ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
68 69 70 71
Arguments bi_fupd_fupd : simpl never.

Class BiBUpdFUpd (PROP : sbi) `{BiBUpd PROP, BiFUpd PROP} :=
  bupd_fupd E (P : PROP) : (|==> P) ={E}= P.
72
Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
73

Robbert Krebbers's avatar
Robbert Krebbers committed
74 75
Class BiBUpdPlainly (PROP : sbi) `{!BiBUpd PROP, !BiPlainly PROP} :=
  bupd_plainly (P : PROP) : (|==>  P) - P.
76
Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78 79 80 81 82 83 84

Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
  fupd_plain' E1 E2 E2' (P Q : PROP) `{!Plain P} :
    E1  E2 
    (Q ={E1, E2'}= P) - (|={E1, E2}=> Q) ={E1}= (|={E1, E2}=> Q)  P;
  later_fupd_plain E (P : PROP) `{!Plain P} :
    ( |={E}=> P) ={E}=   P;
}.
85
Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
86

Robbert Krebbers's avatar
Robbert Krebbers committed
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
Section bupd_laws.
  Context `{BiBUpd PROP}.
  Implicit Types P : PROP.

  Global Instance bupd_ne : NonExpansive (@bupd PROP _).
  Proof. eapply bi_bupd_mixin_bupd_ne, bi_bupd_mixin. Qed.
  Lemma bupd_intro P : P == P.
  Proof. eapply bi_bupd_mixin_bupd_intro, bi_bupd_mixin. Qed.
  Lemma bupd_mono (P Q : PROP) : (P  Q)  (|==> P) == Q.
  Proof. eapply bi_bupd_mixin_bupd_mono, bi_bupd_mixin. Qed.
  Lemma bupd_trans (P : PROP) : (|==> |==> P) == P.
  Proof. eapply bi_bupd_mixin_bupd_trans, bi_bupd_mixin. Qed.
  Lemma bupd_frame_r (P R : PROP) : (|==> P)  R == P  R.
  Proof. eapply bi_bupd_mixin_bupd_frame_r, bi_bupd_mixin. Qed.
End bupd_laws.
102

Robbert Krebbers's avatar
Robbert Krebbers committed
103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122
Section fupd_laws.
  Context `{BiFUpd PROP}.
  Implicit Types P : PROP.

  Global Instance fupd_ne E1 E2 : NonExpansive (@fupd PROP _ E1 E2).
  Proof. eapply bi_fupd_mixin_fupd_ne, bi_fupd_mixin. Qed.
  Lemma fupd_intro_mask E1 E2 (P : PROP) : E2  E1  P  |={E1,E2}=> |={E2,E1}=> P.
  Proof. eapply bi_fupd_mixin_fupd_intro_mask, bi_fupd_mixin. Qed.
  Lemma except_0_fupd E1 E2 (P : PROP) :  (|={E1,E2}=> P) ={E1,E2}= P.
  Proof. eapply bi_fupd_mixin_except_0_fupd, bi_fupd_mixin. Qed.
  Lemma fupd_mono E1 E2 (P Q : PROP) : (P  Q)  (|={E1,E2}=> P)  |={E1,E2}=> Q.
  Proof. eapply bi_fupd_mixin_fupd_mono, bi_fupd_mixin. Qed.
  Lemma fupd_trans E1 E2 E3 (P : PROP) : (|={E1,E2}=> |={E2,E3}=> P)  |={E1,E3}=> P.
  Proof. eapply bi_fupd_mixin_fupd_trans, bi_fupd_mixin. Qed.
  Lemma fupd_mask_frame_r' E1 E2 Ef (P : PROP) :
    E1 ## Ef  (|={E1,E2}=> E2 ## Ef  P) ={E1  Ef,E2  Ef}= P.
  Proof. eapply bi_fupd_mixin_fupd_mask_frame_r', bi_fupd_mixin. Qed.
  Lemma fupd_frame_r E1 E2 (P Q : PROP) : (|={E1,E2}=> P)  Q ={E1,E2}= P  Q.
  Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed.
End fupd_laws.
123 124

Section bupd_derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
125 126
  Context `{BiBUpd PROP}.
  Implicit Types P Q R : PROP.
127

128
  (* FIXME: Removing the `PROP:=` diverges. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
129 130
  Global Instance bupd_proper :
    Proper (() ==> ()) (bupd (PROP:=PROP)) := ne_proper _.
131 132

  (** BUpd derived rules *)
133
  Global Instance bupd_mono' : Proper (() ==> ()) (bupd (PROP:=PROP)).
134
  Proof. intros P Q; apply bupd_mono. Qed.
135
  Global Instance bupd_flip_mono' : Proper (flip () ==> flip ()) (bupd (PROP:=PROP)).
136 137 138 139 140
  Proof. intros P Q; apply bupd_mono. Qed.

  Lemma bupd_frame_l R Q : (R  |==> Q) == R  Q.
  Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
  Lemma bupd_wand_l P Q : (P - Q)  (|==> P) == Q.
141
  Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
142
  Lemma bupd_wand_r P Q : (|==> P)  (P - Q) == Q.
143
  Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
144 145 146 147
  Lemma bupd_sep P Q : (|==> P)  (|==> Q) == P  Q.
  Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
End bupd_derived.

Robbert Krebbers's avatar
Robbert Krebbers committed
148 149 150 151 152 153
Section bupd_derived_sbi.
  Context {PROP : sbi} `{BiBUpd PROP}.
  Implicit Types P Q R : PROP.

  Lemma except_0_bupd P :  (|==> P)  (|==>  P).
  Proof.
154 155
    rewrite /sbi_except_0. apply or_elim; eauto using bupd_mono, or_intro_r.
    by rewrite -bupd_intro -or_intro_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
157 158 159

  Lemma bupd_plain P `{BiBUpdPlainly PROP, !Plain P} : (|==> P)  P.
  Proof. by rewrite {1}(plain P) bupd_plainly. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
End bupd_derived_sbi.
161 162

Section fupd_derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
163 164
  Context `{BiFUpd PROP}.
  Implicit Types P Q R : PROP.
165

Robbert Krebbers's avatar
Robbert Krebbers committed
166 167
  Global Instance fupd_proper E1 E2 :
    Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2) := ne_proper _.
168 169

  (** FUpd derived rules *)
170
  Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2).
171 172
  Proof. intros P Q; apply fupd_mono. Qed.
  Global Instance fupd_flip_mono' E1 E2 :
173
    Proper (flip () ==> flip ()) (fupd (PROP:=PROP) E1 E2).
174 175 176
  Proof. intros P Q; apply fupd_mono. Qed.

  Lemma fupd_intro E P : P ={E}= P.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
  Proof. by rewrite {1}(fupd_intro_mask E E P) // fupd_trans. Qed.
Ralf Jung's avatar
Ralf Jung committed
178
  Lemma fupd_intro_mask' E1 E2 : E2  E1  (|={E1,E2}=> |={E2,E1}=> bi_emp (PROP:=PROP))%I.
179 180 181 182 183 184 185
  Proof. exact: fupd_intro_mask. Qed.
  Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=>  P) ={E1,E2}= P.
  Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.

  Lemma fupd_frame_l E1 E2 P Q : (P  |={E1,E2}=> Q) ={E1,E2}= P  Q.
  Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
  Lemma fupd_wand_l E1 E2 P Q : (P - Q)  (|={E1,E2}=> P) ={E1,E2}= Q.
186
  Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
187
  Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}= Q.
188
  Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
189 190 191 192

  Lemma fupd_trans_frame E1 E2 E3 P Q :
    ((Q ={E2,E3}= emp)  |={E1,E2}=> (Q  P)) ={E1,E3}= P.
  Proof.
193
    rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
194 195 196
    by rewrite fupd_frame_r left_id fupd_trans.
  Qed.

197 198 199 200
  Lemma fupd_elim E1 E2 E3 P Q :
    (Q - (|={E2,E3}=> P))  (|={E1,E2}=> Q) - (|={E1,E3}=> P).
  Proof. intros ->. rewrite fupd_trans //. Qed.

201 202 203 204
  Lemma fupd_mask_frame_r E1 E2 Ef P :
    E1 ## Ef  (|={E1,E2}=> P) ={E1  Ef,E2  Ef}= P.
  Proof.
    intros ?. rewrite -fupd_mask_frame_r' //. f_equiv.
205
    apply impl_intro_l, and_elim_r.
206 207 208 209 210
  Qed.
  Lemma fupd_mask_mono E1 E2 P : E1  E2  (|={E1}=> P) ={E2}= P.
  Proof.
    intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
  Qed.
211 212
  (** How to apply an arbitrary mask-changing view shift when having
      an arbitrary mask. *)
213
  Lemma fupd_mask_frame E E' E1 E2 P :
214 215
    E1  E 
    (|={E1,E2}=> |={E2  (E  E1),E'}=> P) - (|={E,E'}=> P).
216
  Proof.
217 218
    intros ?. rewrite (fupd_mask_frame_r _ _ (E  E1)); last set_solver.
    rewrite fupd_trans.
219 220 221
    assert (E = E1  E  E1) as <-; last done.
    apply union_difference_L. done.
  Qed.
222 223 224 225 226 227 228 229 230
  (* A variant of [fupd_mask_frame] that works well for accessors: Tailored to
     elliminate updates of the form [|={E1,E1∖E2}=> Q] and provides a way to
     transform the closing view shift instead of letting you prove the same
     side-conditions twice. *)
  Lemma fupd_mask_frame_acc E E' E1(*Eo*) E2(*Em*) P Q :
    E1  E 
    (|={E1,E1E2}=> Q) -
    (Q - |={EE2,E'}=> ( R, (|={E1E2,E1}=> R) - |={EE2,E}=> R) -  P) -
    (|={E,E'}=> P).
231
  Proof.
232 233
    intros HE. apply wand_intro_r. rewrite fupd_frame_r.
    rewrite wand_elim_r. clear Q.
234 235 236 237 238 239 240
    rewrite -(fupd_mask_frame E E'); first apply fupd_mono; last done.
    (* The most horrible way to apply fupd_intro_mask *)
    rewrite -[X in (X - _)](right_id emp%I).
    rewrite (fupd_intro_mask (E1  E2  E  E1) (E  E2) emp%I); last first.
    { rewrite {1}(union_difference_L _ _ HE). set_solver. }
    rewrite fupd_frame_l fupd_frame_r. apply fupd_elim.
    apply fupd_mono.
241 242 243
    eapply wand_apply;
      last (apply sep_mono; first reflexivity); first reflexivity.
    apply forall_intro=>R. apply wand_intro_r.
244 245 246
    rewrite fupd_frame_r. apply fupd_elim. rewrite left_id.
    rewrite (fupd_mask_frame_r _ _ (E  E1)); last set_solver+.
    rewrite {4}(union_difference_L _ _ HE). done.
247 248 249 250 251
  Qed.

  Lemma fupd_mask_same E E1 P :
    E = E1  (|={E}=> P) - (|={E,E1}=> P).
  Proof. intros <-. done. Qed.
252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273

  Lemma fupd_sep E P Q : (|={E}=> P)  (|={E}=> Q) ={E}= P  Q.
  Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
  Lemma fupd_big_sepL {A} E (Φ : nat  A  PROP) (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.
  Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K  A  PROP) (m : gmap K A) :
    ([ map] kx  m, |={E}=> Φ k x) ={E}= [ map] kx  m, Φ k x.
  Proof.
    apply (big_opM_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
    intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
  Qed.
  Lemma fupd_big_sepS `{Countable A} E (Φ : A  PROP) X :
    ([ set] x  X, |={E}=> Φ x) ={E}= [ set] x  X, Φ x.
  Proof.
    apply (big_opS_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
    intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
274
  Lemma fupd_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 P Q `{!Plain P} :
275 276
    E1  E2  (Q - P) - (|={E1, E2}=> Q) ={E1}= (|={E1, E2}=> Q)  P.
  Proof.
277 278
    intros HE. rewrite -(fupd_plain' _ _ E1) //. apply wand_intro_l.
    by rewrite wand_elim_r -fupd_intro.
279 280 281
  Qed.

  (** Fancy updates that take a step derived rules. *)
282
  Lemma step_fupd_wand E1 E2 E3 P Q : (|={E1,E2,E3}=> P) - (P - Q) - |={E1,E2,E3}=> Q.
283
  Proof.
284 285 286
    apply wand_intro_l.
    by rewrite (later_intro (P - Q)%I) fupd_frame_l -later_sep fupd_frame_l
               wand_elim_l.
287 288
  Qed.

289 290
  Lemma step_fupd_mask_frame_r E1 E2 E3 Ef P :
    E1 ## Ef  E2 ## Ef  (|={E1,E2,E3}=> P)  |={E1  Ef,E2  Ef,E3  Ef}=> P.
291 292 293 294 295 296 297
  Proof.
    intros. rewrite -fupd_mask_frame_r //. do 2 f_equiv. by apply 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.
298
    intros ??. rewrite -(emp_sep (|={E1,F2}=> P)%I).
299 300 301 302 303
    rewrite (fupd_intro_mask E2 E1 emp%I) //.
    rewrite fupd_frame_r -(fupd_trans E2 E1 F1). f_equiv.
    rewrite fupd_frame_l -(fupd_trans E1 F2 F1). f_equiv.
    rewrite (fupd_intro_mask F2 F1 (|={_,_}=> emp)%I) //.
    rewrite fupd_frame_r. f_equiv.
304
    rewrite [X in (X  _)%I]later_intro -later_sep. f_equiv.
305 306 307 308 309 310 311 312
    rewrite fupd_frame_r -(fupd_trans F1 F2 E2). f_equiv.
    rewrite fupd_frame_l -(fupd_trans F2 E1 E2). f_equiv.
    by rewrite fupd_frame_r left_id.
  Qed.

  Lemma step_fupd_intro E1 E2 P : E2  E1   P - |={E1,E2}=> P.
  Proof. intros. by rewrite -(step_fupd_mask_mono E2 _ _ E2) // -!fupd_intro. Qed.
End fupd_derived.