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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
18
19
20
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.
21

Ralf Jung's avatar
Ralf Jung committed
22
23
24
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.
25
26

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

Robbert Krebbers's avatar
Robbert Krebbers committed
32
(** Bundled versions  *)
Robbert Krebbers's avatar
Robbert Krebbers committed
33
(* Mixins allow us to create instances easily without having to use Program *)
Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
36
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
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;
}.
64
Hint Mode BiFUpd ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
67
68
Arguments bi_fupd_fupd : simpl never.

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

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

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;
}.
82
Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
83

Robbert Krebbers's avatar
Robbert Krebbers committed
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
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.
99

Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
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.
120
121

Section bupd_derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
123
  Context `{BiBUpd PROP}.
  Implicit Types P Q R : PROP.
124

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

  (** BUpd derived rules *)
130
  Global Instance bupd_mono' : Proper (() ==> ()) (bupd (PROP:=PROP)).
131
  Proof. intros P Q; apply bupd_mono. Qed.
132
  Global Instance bupd_flip_mono' : Proper (flip () ==> flip ()) (bupd (PROP:=PROP)).
133
134
135
136
137
138
139
140
141
142
143
144
  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.
  Proof. by rewrite bupd_frame_l bi.wand_elim_l. Qed.
  Lemma bupd_wand_r P Q : (|==> P)  (P - Q) == Q.
  Proof. by rewrite bupd_frame_r bi.wand_elim_r. Qed.
  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
145
146
147
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.
    rewrite /sbi_except_0. apply bi.or_elim; eauto using bupd_mono, bi.or_intro_r.
    by rewrite -bupd_intro -bi.or_intro_l.
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
155
156

  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
157
End bupd_derived_sbi.
158
159

Section fupd_derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
161
  Context `{BiFUpd PROP}.
  Implicit Types P Q R : PROP.
162

Robbert Krebbers's avatar
Robbert Krebbers committed
163
164
  Global Instance fupd_proper E1 E2 :
    Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2) := ne_proper _.
165
166

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

  Lemma fupd_intro E P : P ={E}= P.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
  Proof. by rewrite {1}(fupd_intro_mask E E P) // fupd_trans. Qed.
Ralf Jung's avatar
Ralf Jung committed
175
  Lemma fupd_intro_mask' E1 E2 : E2  E1  (|={E1,E2}=> |={E2,E1}=> bi_emp (PROP:=PROP))%I.
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
  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.
  Proof. by rewrite fupd_frame_l bi.wand_elim_l. Qed.
  Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}= Q.
  Proof. by rewrite fupd_frame_r bi.wand_elim_r. Qed.

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

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

198
199
200
201
202
203
204
205
206
207
  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.
    apply bi.impl_intro_l, bi.and_elim_r.
  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.
208
209
  (** How to apply an arbitrary mask-changing view shift when having
      an arbitrary mask. *)
210
  Lemma fupd_mask_frame E E' E1 E2 P :
211
212
    E1  E 
    (|={E1,E2}=> |={E2  (E  E1),E'}=> P) - (|={E,E'}=> P).
213
  Proof.
214
215
    intros ?. rewrite (fupd_mask_frame_r _ _ (E  E1)); last set_solver.
    rewrite fupd_trans.
216
217
218
    assert (E = E1  E  E1) as <-; last done.
    apply union_difference_L. done.
  Qed.
219
220
221
222
223
224
225
226
227
  (* 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).
228
  Proof.
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
    intros HE. apply bi.wand_intro_r. rewrite fupd_frame_r.
    rewrite bi.wand_elim_r. clear Q.
    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.
    eapply bi.wand_apply;
      last (apply bi.sep_mono; first reflexivity); first reflexivity.
    apply bi.forall_intro=>R. apply bi.wand_intro_r.
    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.
244
245
246
247
248
  Qed.

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

  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
271
  Lemma fupd_plain `{BiPlainly PROP, !BiFUpdPlainly PROP} E1 E2 P Q `{!Plain P} :
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
    E1  E2  (Q - P) - (|={E1, E2}=> Q) ={E1}= (|={E1, E2}=> Q)  P.
  Proof.
    intros HE. rewrite -(fupd_plain' _ _ E1) //. apply bi.wand_intro_l.
    by rewrite bi.wand_elim_r -fupd_intro.
  Qed.

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

  Lemma step_fupd_mask_frame_r E1 E2 Ef P :
    E1 ## Ef  E2 ## Ef  (|={E1,E2}=> P)  |={E1  Ef,E2  Ef}=> P.
  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.
    intros ??. rewrite -(left_id emp%I _ (|={E1,F2}=> P)%I).
    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.
    rewrite [X in (X  _)%I]bi.later_intro -bi.later_sep. f_equiv.
    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.