updates.v 19 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
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;
57
  bi_fupd_mixin_fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P)  R ={E1,E2}= P  R;
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59 60 61 62 63 64 65 66 67 68 69 70
}.

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 87 88 89 90
  fupd_plainly_mask_empty E (P : PROP) :
    (|={E,}=>  P)  |={E}=> P;
  fupd_plainly_keep_l E (P R : PROP) :
    (R ={E}=  P)  R  |={E}=> P  R;
  fupd_plainly_later E (P : PROP) :
    ( |={E}=>  P)  |={E}=>   P;
  fupd_plainly_forall_2 E {A} (Φ : A  PROP) :
    ( x, |={E}=>  Φ x)  |={E}=>  x, Φ x
Robbert Krebbers's avatar
Robbert Krebbers committed
91
}.
92
Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
93

Robbert Krebbers's avatar
Robbert Krebbers committed
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
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.
109

Robbert Krebbers's avatar
Robbert Krebbers committed
110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
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.
127
  Lemma fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P)  R ={E1,E2}= P  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
128 129
  Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed.
End fupd_laws.
130 131

Section bupd_derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
132 133
  Context `{BiBUpd PROP}.
  Implicit Types P Q R : PROP.
134

135
  (* FIXME: Removing the `PROP:=` diverges. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
136 137
  Global Instance bupd_proper :
    Proper (() ==> ()) (bupd (PROP:=PROP)) := ne_proper _.
138 139

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

  Lemma except_0_bupd P :  (|==> P)  (|==>  P).
  Proof.
161 162
    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
163
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
164

165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
  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
180
End bupd_derived_sbi.
181 182

Section fupd_derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
183 184
  Context `{BiFUpd PROP}.
  Implicit Types P Q R : PROP.
185

Robbert Krebbers's avatar
Robbert Krebbers committed
186 187
  Global Instance fupd_proper E1 E2 :
    Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2) := ne_proper _.
188 189

  (** FUpd derived rules *)
190
  Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2).
191 192
  Proof. intros P Q; apply fupd_mono. Qed.
  Global Instance fupd_flip_mono' E1 E2 :
193
    Proper (flip () ==> flip ()) (fupd (PROP:=PROP) E1 E2).
194 195 196
  Proof. intros P Q; apply fupd_mono. Qed.

  Lemma fupd_intro E P : P ={E}= P.
Robbert Krebbers's avatar
Robbert Krebbers committed
197
  Proof. by rewrite {1}(fupd_intro_mask E E P) // fupd_trans. Qed.
Ralf Jung's avatar
Ralf Jung committed
198
  Lemma fupd_intro_mask' E1 E2 : E2  E1  (|={E1,E2}=> |={E2,E1}=> bi_emp (PROP:=PROP))%I.
199 200 201 202
  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.

203 204
  Lemma fupd_frame_l E1 E2 R Q : (R  |={E1,E2}=> Q) ={E1,E2}= R  Q.
  Proof. rewrite !(comm _ R); apply fupd_frame_r. Qed.
205
  Lemma fupd_wand_l E1 E2 P Q : (P - Q)  (|={E1,E2}=> P) ={E1,E2}= Q.
206
  Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
207
  Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}= Q.
208
  Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
209

210 211 212 213 214 215 216
  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.

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

224 225 226 227
  Lemma fupd_elim E1 E2 E3 P Q :
    (Q - (|={E2,E3}=> P))  (|={E1,E2}=> Q) - (|={E1,E3}=> P).
  Proof. intros ->. rewrite fupd_trans //. Qed.

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

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

  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. *)
301
  Lemma step_fupd_wand E1 E2 E3 P Q : (|={E1,E2,E3}=> P) - (P - Q) - |={E1,E2,E3}=> Q.
302
  Proof.
303 304 305
    apply wand_intro_l.
    by rewrite (later_intro (P - Q)%I) fupd_frame_l -later_sep fupd_frame_l
               wand_elim_l.
306 307
  Qed.

308 309
  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.
310 311 312 313 314 315 316
  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.
317
    intros ??. rewrite -(emp_sep (|={E1,F2}=> P)%I).
318 319 320 321 322
    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.
323
    rewrite [X in (X  _)%I]later_intro -later_sep. f_equiv.
324 325 326 327 328 329 330
    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.
331 332 333 334 335 336 337 338 339 340

  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.

341
  Lemma step_fupd_fupd E E' P : (|={E,E'}=> P)  (|={E,E'}=> |={E}=> P).
342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
  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.

368 369 370
  Section fupd_plainly_derived.
    Context `{BiPlainly PROP, !BiFUpdPlainly PROP}.

371 372 373 374 375 376 377 378
    Lemma fupd_plainly_mask E E' P : (|={E,E'}=>  P)  |={E}=> P.
    Proof.
      rewrite -(fupd_plainly_mask_empty).
      apply fupd_elim, (fupd_mask_weaken _ _ _). set_solver.
    Qed.

    Lemma fupd_plainly_elim E P :  P ={E}= P.
    Proof. by rewrite (fupd_intro E ( P)%I) fupd_plainly_mask. Qed.
379

380 381
    Lemma fupd_plainly_keep_r E P R : R  (R ={E}=  P)  |={E}=> R  P.
    Proof. by rewrite !(comm _ R) fupd_plainly_keep_l. Qed.
382

383 384 385 386
    Lemma fupd_plain_mask_empty E P `{!Plain P} : (|={E,}=> P)  |={E}=> P.
    Proof. by rewrite {1}(plain P) fupd_plainly_mask_empty. Qed.
    Lemma fupd_plain_mask E E' P `{!Plain P} : (|={E,E'}=> P)  |={E}=> P.
    Proof. by rewrite {1}(plain P) fupd_plainly_mask. Qed.
387

388 389 390 391 392 393 394 395 396
    Lemma fupd_plain_keep_l E P R `{!Plain P} : (R ={E}= P)  R  |={E}=> P  R.
    Proof. by rewrite {1}(plain P) fupd_plainly_keep_l. Qed.
    Lemma fupd_plain_keep_r E P R `{!Plain P} : R  (R ={E}= P)  |={E}=> R  P.
    Proof. by rewrite {1}(plain P) fupd_plainly_keep_r. Qed.

    Lemma fupd_plain_later E P `{!Plain P} : ( |={E}=> P)  |={E}=>   P.
    Proof. by rewrite {1}(plain P) fupd_plainly_later. Qed.
    Lemma fupd_plain_forall_2 E {A} (Φ : A  PROP) `{! x, Plain (Φ x)} :
      ( x, |={E}=> Φ x)  |={E}=>  x, Φ x.
397
    Proof.
398 399
      rewrite -fupd_plainly_forall_2. apply forall_mono=> x.
      by rewrite {1}(plain (Φ _)).
400 401
    Qed.

402 403
    Lemma fupd_plainly_laterN E n P `{HP : !Plain P} :
      (^n |={E}=> P)  |={E}=> ^n  P.
404
    Proof.
405 406 407 408
      revert P HP. induction n as [|n IH]=> P ? /=.
      - by rewrite -except_0_intro.
      - rewrite -!later_laterN !laterN_later.
        rewrite fupd_plain_later. by rewrite IH except_0_later.
409 410
    Qed.

411 412 413
    Lemma fupd_plain_forall E1 E2 {A} (Φ : A  PROP) `{! x, Plain (Φ x)} :
      E2  E1 
      (|={E1,E2}=>  x, Φ x)  ( x, |={E1,E2}=> Φ x).
414
    Proof.
415 416 417 418 419 420 421
      intros. apply (anti_symm _).
      { apply forall_intro=> x. by rewrite (forall_elim x). }
      trans ( x, |={E1}=> Φ x)%I.
      { apply forall_mono=> x. by rewrite fupd_plain_mask. }
      rewrite fupd_plain_forall_2. apply fupd_elim.
      rewrite {1}(plain ( x, Φ x)) (fupd_mask_weaken E1 E2 ( _)%I) //.
      apply fupd_elim. by rewrite fupd_plainly_elim.
422
    Qed.
423 424 425
    Lemma fupd_plain_forall' E {A} (Φ : A  PROP) `{! x, Plain (Φ x)} :
      (|={E}=>  x, Φ x)  ( x, |={E}=> Φ x).
    Proof. by apply fupd_plain_forall. Qed.
426

427 428 429 430 431 432 433
    Lemma step_fupd_plain E E' P `{!Plain P} : (|={E,E'}=> P) ={E}=   P.
    Proof.
      rewrite -(fupd_plain_mask _ E' (  P)%I).
      apply fupd_elim. by rewrite fupd_plain_mask -fupd_plain_later.
    Qed.

    Lemma step_fupdN_plain E E' n P `{!Plain P} : (|={E,E'}=>^n P) ={E}= ^n  P.
434 435
    Proof.
      induction n as [|n IH].
436 437 438
      - by rewrite -fupd_intro -except_0_intro.
      - rewrite Nat_iter_S step_fupd_fupd IH !fupd_trans step_fupd_plain.
        apply fupd_mono. destruct n as [|n]; simpl.
439 440 441
        * by rewrite except_0_idemp.
        * by rewrite except_0_later.
    Qed.
442

443 444 445 446 447 448 449 450 451 452 453 454 455
    Lemma step_fupd_plain_forall E1 E2 {A} (Φ : A  PROP) `{! x, Plain (Φ x)} :
      E2  E1 
      (|={E1,E2}=>  x, Φ x)  ( x, |={E1,E2}=> Φ x).
    Proof.
      intros. apply (anti_symm _).
      { apply forall_intro=> x. by rewrite (forall_elim x). }
      trans ( x, |={E1}=>   Φ x)%I.
      { apply forall_mono=> x. by rewrite step_fupd_plain. }
      rewrite -fupd_plain_forall'. apply fupd_elim.
      rewrite -(fupd_except_0 E2 E1) -step_fupd_intro //.
      by rewrite -later_forall -except_0_forall.
    Qed.
  End fupd_plainly_derived.
456
End fupd_derived.