updates.v 17.1 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
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.
31
Notation "P ={ E1 , E2 }▷=∗ Q" := (P  |={ E1 , E2, E1 }=> Q) (only parsing) : stdpp_scope.
32
Notation "P ={ E1 , E2 }▷=∗ Q" := (P - |={ E1 , E2, E1 }=> Q)%I : bi_scope.
Ralf Jung's avatar
Ralf Jung committed
33
34
Notation "|={ E }▷=> Q" := (|={E,E}=> Q)%I : bi_scope.
Notation "P ={ E }▷=∗ Q" := (P ={E,E}= Q)%I : bi_scope.
35
Notation "|={ E1 , E2 }▷=>^ n Q" := (Nat.iter n (λ P, |={E1,E2}=> P) Q)%I : bi_scope.
36
37
Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P  |={E1,E2}=>^n Q)%I (only parsing) : stdpp_scope.
Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P - |={E1,E2}=>^n Q)%I : bi_scope.
38

Robbert Krebbers's avatar
Robbert Krebbers committed
39
(** Bundled versions  *)
Robbert Krebbers's avatar
Robbert Krebbers committed
40
(* Mixins allow us to create instances easily without having to use Program *)
Robbert Krebbers's avatar
Robbert Krebbers committed
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
67
68
69
70
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;
}.
71
Hint Mode BiFUpd ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
73
74
75
Arguments bi_fupd_fupd : simpl never.

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

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

Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
83
84
85
86
  fupd_plainly_weak E (P Q : PROP) :
    (Q ={E}=  P) - Q ={E}= Q  P;
  later_fupd_plainly p E1 E2 (P : PROP) :
    (?p |={E1, E2}=>  P) ={E1}= ?p  P;
Robbert Krebbers's avatar
Robbert Krebbers committed
87
}.
88
Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
89

Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
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.
105

Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
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.
126
127

Section bupd_derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
  Context `{BiBUpd PROP}.
  Implicit Types P Q R : PROP.
130

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

  (** BUpd derived rules *)
136
  Global Instance bupd_mono' : Proper (() ==> ()) (bupd (PROP:=PROP)).
137
  Proof. intros P Q; apply bupd_mono. Qed.
138
  Global Instance bupd_flip_mono' : Proper (flip () ==> flip ()) (bupd (PROP:=PROP)).
139
140
141
142
143
  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.
144
  Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
145
  Lemma bupd_wand_r P Q : (|==> P)  (P - Q) == Q.
146
  Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
147
148
149
150
  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
151
152
153
154
155
156
Section bupd_derived_sbi.
  Context {PROP : sbi} `{BiBUpd PROP}.
  Implicit Types P Q R : PROP.

  Lemma except_0_bupd P :  (|==> P)  (|==>  P).
  Proof.
157
158
    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
159
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
160

161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
  Section bupd_plainly.
    Context `{BiBUpdPlainly PROP}.

    Lemma bupd_plain P `{!Plain P} : (|==> P)  P.
    Proof. by rewrite {1}(plain P) bupd_plainly. Qed.

    Lemma bupd_forall {A} (Φ : A  PROP) `{ x, Plain (Φ x)} :
      (|==>  x, Φ x)  ( x, |==> Φ x).
    Proof.
      apply (anti_symm _).
      - apply forall_intro=> x. by rewrite (forall_elim x).
      - rewrite -bupd_intro. apply forall_intro=> x.
        by rewrite (forall_elim x) bupd_plain.
    Qed.
  End bupd_plainly.
Robbert Krebbers's avatar
Robbert Krebbers committed
176
End bupd_derived_sbi.
177
178

Section fupd_derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
179
180
  Context `{BiFUpd PROP}.
  Implicit Types P Q R : PROP.
181

Robbert Krebbers's avatar
Robbert Krebbers committed
182
183
  Global Instance fupd_proper E1 E2 :
    Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2) := ne_proper _.
184
185

  (** FUpd derived rules *)
186
  Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2).
187
188
  Proof. intros P Q; apply fupd_mono. Qed.
  Global Instance fupd_flip_mono' E1 E2 :
189
    Proper (flip () ==> flip ()) (fupd (PROP:=PROP) E1 E2).
190
191
192
  Proof. intros P Q; apply fupd_mono. Qed.

  Lemma fupd_intro E P : P ={E}= P.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
  Proof. by rewrite {1}(fupd_intro_mask E E P) // fupd_trans. Qed.
Ralf Jung's avatar
Ralf Jung committed
194
  Lemma fupd_intro_mask' E1 E2 : E2  E1  (|={E1,E2}=> |={E2,E1}=> bi_emp (PROP:=PROP))%I.
195
196
197
198
199
200
201
  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.
202
  Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
203
  Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}= Q.
204
  Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
205

206
207
208
209
210
211
212
  Lemma fupd_mask_weaken E1 E2 P `{!Absorbing P} : E2  E1  P ={E1,E2}= P.
  Proof.
    intros ?. rewrite -{1}(right_id emp%I bi_sep P%I).
    rewrite (fupd_intro_mask E1 E2 emp%I) //.
    by rewrite fupd_frame_l sep_elim_l.
  Qed.

213
214
215
  Lemma fupd_trans_frame E1 E2 E3 P Q :
    ((Q ={E2,E3}= emp)  |={E1,E2}=> (Q  P)) ={E1,E3}= P.
  Proof.
216
    rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
217
218
219
    by rewrite fupd_frame_r left_id fupd_trans.
  Qed.

220
221
222
223
  Lemma fupd_elim E1 E2 E3 P Q :
    (Q - (|={E2,E3}=> P))  (|={E1,E2}=> Q) - (|={E1,E3}=> P).
  Proof. intros ->. rewrite fupd_trans //. Qed.

224
225
226
227
  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.
228
    apply impl_intro_l, and_elim_r.
229
230
231
232
233
  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.
234
235
  (** How to apply an arbitrary mask-changing view shift when having
      an arbitrary mask. *)
236
  Lemma fupd_mask_frame E E' E1 E2 P :
237
238
    E1  E 
    (|={E1,E2}=> |={E2  (E  E1),E'}=> P) - (|={E,E'}=> P).
239
  Proof.
240
241
    intros ?. rewrite (fupd_mask_frame_r _ _ (E  E1)); last set_solver.
    rewrite fupd_trans.
242
243
244
    assert (E = E1  E  E1) as <-; last done.
    apply union_difference_L. done.
  Qed.
245
246
247
248
249
250
251
252
253
  (* 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).
254
  Proof.
255
256
    intros HE. apply wand_intro_r. rewrite fupd_frame_r.
    rewrite wand_elim_r. clear Q.
257
258
259
260
261
262
263
    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.
264
265
266
    eapply wand_apply;
      last (apply sep_mono; first reflexivity); first reflexivity.
    apply forall_intro=>R. apply wand_intro_r.
267
268
269
    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.
270
271
272
273
274
  Qed.

  Lemma fupd_mask_same E E1 P :
    E = E1  (|={E}=> P) - (|={E,E1}=> P).
  Proof. intros <-. done. Qed.
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297

  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.

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

305
306
  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.
307
308
309
310
311
312
313
  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.
314
    intros ??. rewrite -(emp_sep (|={E1,F2}=> P)%I).
315
316
317
318
319
    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.
320
    rewrite [X in (X  _)%I]later_intro -later_sep. f_equiv.
321
322
323
324
325
326
327
    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.
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365

  Lemma step_fupd_frame_l E1 E2 R Q :
    (R  |={E1, E2}=> Q) - |={E1, E2}=> (R  Q).
  Proof.
    rewrite fupd_frame_l.
    apply fupd_mono.
    rewrite [P in P  _  _](later_intro R) -later_sep fupd_frame_l.
    by apply later_mono, fupd_mono.
  Qed.

  Lemma step_fupd_fupd E P:
    (|={E, }=> P)  (|={E, }=> |={E}=> P).
  Proof.
    apply (anti_symm ()).
    - by rewrite -fupd_intro.
    - by rewrite fupd_trans.
  Qed.

  Lemma step_fupdN_mono E1 E2 n P Q :
    (P  Q)  (|={E1, E2}=>^n P)  (|={E1, E2}=>^n Q).
  Proof.
    intros HPQ. induction n as [|n IH]=> //=. rewrite IH //.
  Qed.

  Lemma step_fupdN_S_fupd n E P:
    (|={E, }=>^(S n) P)  (|={E, }=>^(S n) |={E}=> P).
  Proof.
    apply (anti_symm ()); rewrite !Nat_iter_S_r; apply step_fupdN_mono;
      rewrite -step_fupd_fupd //.
  Qed.

  Lemma step_fupdN_frame_l E1 E2 n R Q :
    (R  |={E1, E2}=>^n Q) - |={E1, E2}=>^n (R  Q).
  Proof.
    induction n as [|n IH]; simpl; [done|].
    rewrite step_fupd_frame_l IH //=.
  Qed.

366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
  Section fupd_plainly_derived.
    Context `{BiPlainly PROP, !BiFUpdPlainly PROP}.

    Lemma fupd_plain_weak E P Q `{!Plain P}:
      (Q ={E}= P) - Q ={E}= Q  P.
    Proof. by rewrite {1}(plain P) fupd_plainly_weak. Qed.

    Lemma later_fupd_plain p E1 E2 P `{!Plain P} :
      (?p |={E1, E2}=> P) ={E1}= ?p  P.
    Proof. by rewrite {1}(plain P) later_fupd_plainly. Qed.

    Lemma fupd_plain_strong E1 E2 P `{!Plain P} :
      (|={E1, E2}=> P) ={E1}=  P.
    Proof. by apply (later_fupd_plain false). Qed.

    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.
      intros (E3&->&HE)%subseteq_disjoint_union_L.
      apply wand_intro_l. rewrite fupd_frame_r.
      rewrite fupd_plain_strong fupd_except_0 fupd_plain_weak wand_elim_r.
      rewrite (fupd_mask_mono E1 (E1  E3)); last by set_solver+.
      rewrite fupd_trans -(fupd_trans E1 (E1  E3) E1).
      apply fupd_mono. rewrite -fupd_frame_r.
      apply sep_mono; auto. apply fupd_intro_mask; set_solver+.
    Qed.

    Lemma fupd_plain E1 E2 P Q `{!Plain P} :
      E1  E2  (Q - P) - (|={E1, E2}=> Q) ={E1}= (|={E1, E2}=> Q)  P.
    Proof.
      intros HE. rewrite -(fupd_plain' _ _ E1) //. apply wand_intro_l.
        by rewrite wand_elim_r -fupd_intro.
    Qed.

    Lemma step_fupd_plain E P `{!Plain P} :
      (|={E, }=> P) ={E}=   P.
    Proof.
      specialize (later_fupd_plain true  E P) => //= ->.
      rewrite fupd_trans fupd_plain_strong. apply fupd_mono, except_0_later.
    Qed.

    Lemma step_fupdN_plain E n P `{!Plain P}:
      (|={E, }=>^n P) ={E}= ^n  P.
    Proof.
      induction n as [|n IH].
      - rewrite -fupd_intro. apply except_0_intro.
      - rewrite Nat_iter_S step_fupd_fupd IH ?fupd_trans step_fupd_plain.
        apply fupd_mono. destruct n; simpl.
        * by rewrite except_0_idemp.
        * by rewrite except_0_later.
    Qed.
  End fupd_plainly_derived.
419

420
End fupd_derived.