updates.v 21.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
Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
42
  bi_bupd_mixin_bupd_ne : NonExpansive (bupd (PROP:=PROP));
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45 46 47 48 49
  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) := {
50
  bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd (PROP:=PROP) E1 E2);
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52 53 54 55 56
  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 83 84 85
(** These rules for the interaction between the [■] and [|={E1,E2=>] modalities
only make sense for affine logics. From the axioms below, one could derive
[■ P ={E}=∗ P] (see the lemma [fupd_plainly_elim]), which in turn gives
[True ={E}=∗ emp]. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
87 88
  (** When proving a fancy update of a plain proposition, you can also prove it
  while being allowed to open all invariants. *)
89 90
  fupd_plainly_mask_empty E (P : PROP) :
    (|={E,}=>  P)  |={E}=> P;
91 92 93
  (** A strong eliminator (a la modus ponens) for the wand-fancy-update with a
  plain conclusion: We eliminate [R ={E}=∗ ■ P] by supplying an [R], but we get
  to keep the [R]. *)
94 95
  fupd_plainly_keep_l E (P R : PROP) :
    (R ={E}=  P)  R  |={E}=> P  R;
96 97 98
  (** Later "almost" commutes with fancy updates over plain propositions. It
  commutes "almost" because of the ◇ modality, which is needed in the definition
  of fancy updates so one can remove laters of timeless propositions. *)
99 100
  fupd_plainly_later E (P : PROP) :
    ( |={E}=>  P)  |={E}=>   P;
101
  (** Forall quantifiers commute with fancy updates over plain propositions. *)
102 103
  fupd_plainly_forall_2 E {A} (Φ : A  PROP) :
    ( x, |={E}=>  Φ x)  |={E}=>  x, Φ x
Robbert Krebbers's avatar
Robbert Krebbers committed
104
}.
105
Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
106

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

Robbert Krebbers's avatar
Robbert Krebbers committed
123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
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.
140
  Lemma fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P)  R ={E1,E2}= P  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
141 142
  Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed.
End fupd_laws.
143 144

Section bupd_derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
145 146
  Context `{BiBUpd PROP}.
  Implicit Types P Q R : PROP.
147

148
  (* FIXME: Removing the `PROP:=` diverges. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
149 150
  Global Instance bupd_proper :
    Proper (() ==> ()) (bupd (PROP:=PROP)) := ne_proper _.
151 152

  (** BUpd derived rules *)
153
  Global Instance bupd_mono' : Proper (() ==> ()) (bupd (PROP:=PROP)).
154
  Proof. intros P Q; apply bupd_mono. Qed.
155
  Global Instance bupd_flip_mono' : Proper (flip () ==> flip ()) (bupd (PROP:=PROP)).
156 157 158 159 160
  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.
161
  Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
162
  Lemma bupd_wand_r P Q : (|==> P)  (P - Q) == Q.
163
  Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
164 165
  Lemma bupd_sep P Q : (|==> P)  (|==> Q) == P  Q.
  Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182

  Global Instance bupd_homomorphism :
    MonoidHomomorphism bi_sep bi_sep (flip ()) (bupd (PROP:=PROP)).
  Proof. split; [split|]; try apply _. apply bupd_sep. apply bupd_intro. Qed.

  Lemma big_sepL_bupd {A} (Φ : nat  A  PROP) l :
    ([ list] kx  l, |==> Φ k x)  |==> [ list] kx  l, Φ k x.
  Proof. by rewrite (big_opL_commute _). Qed.
  Lemma big_sepM_bupd {A} `{Countable K} (Φ : K  A  PROP) l :
    ([ map] kx  l, |==> Φ k x)  |==> [ map] kx  l, Φ k x.
  Proof. by rewrite (big_opM_commute _). Qed.
  Lemma big_sepS_bupd `{Countable A} (Φ : A  PROP) l :
    ([ set]  x  l, |==> Φ x)  |==> [ set] x  l, Φ x.
  Proof. by rewrite (big_opS_commute _). Qed.
  Lemma big_sepMS_bupd `{Countable A} (Φ : A  PROP) l :
    ([ mset] x  l, |==> Φ x)  |==> [ mset] x  l, Φ x.
  Proof. by rewrite (big_opMS_commute _). Qed.
183 184
End bupd_derived.

Robbert Krebbers's avatar
Robbert Krebbers committed
185 186 187 188 189 190
Section bupd_derived_sbi.
  Context {PROP : sbi} `{BiBUpd PROP}.
  Implicit Types P Q R : PROP.

  Lemma except_0_bupd P :  (|==> P)  (|==>  P).
  Proof.
191 192
    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
193
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
194

195 196 197 198 199 200 201 202 203 204 205 206 207 208 209
  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
210
End bupd_derived_sbi.
211 212

Section fupd_derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
213 214
  Context `{BiFUpd PROP}.
  Implicit Types P Q R : PROP.
215

Robbert Krebbers's avatar
Robbert Krebbers committed
216 217
  Global Instance fupd_proper E1 E2 :
    Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2) := ne_proper _.
218 219

  (** FUpd derived rules *)
220
  Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2).
221 222
  Proof. intros P Q; apply fupd_mono. Qed.
  Global Instance fupd_flip_mono' E1 E2 :
223
    Proper (flip () ==> flip ()) (fupd (PROP:=PROP) E1 E2).
224 225 226
  Proof. intros P Q; apply fupd_mono. Qed.

  Lemma fupd_intro E P : P ={E}= P.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
  Proof. by rewrite {1}(fupd_intro_mask E E P) // fupd_trans. Qed.
Ralf Jung's avatar
Ralf Jung committed
228
  Lemma fupd_intro_mask' E1 E2 : E2  E1  (|={E1,E2}=> |={E2,E1}=> bi_emp (PROP:=PROP))%I.
229 230 231 232
  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.

233 234
  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.
235
  Lemma fupd_wand_l E1 E2 P Q : (P - Q)  (|={E1,E2}=> P) ={E1,E2}= Q.
236
  Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
237
  Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}= Q.
238
  Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
239

240 241 242 243 244 245 246
  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.

247 248 249
  Lemma fupd_trans_frame E1 E2 E3 P Q :
    ((Q ={E2,E3}= emp)  |={E1,E2}=> (Q  P)) ={E1,E3}= P.
  Proof.
250
    rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
251 252 253
    by rewrite fupd_frame_r left_id fupd_trans.
  Qed.

254 255 256 257
  Lemma fupd_elim E1 E2 E3 P Q :
    (Q - (|={E2,E3}=> P))  (|={E1,E2}=> Q) - (|={E1,E3}=> P).
  Proof. intros ->. rewrite fupd_trans //. Qed.

258 259 260 261
  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.
262
    apply impl_intro_l, and_elim_r.
263 264 265 266 267
  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.
268 269
  (** How to apply an arbitrary mask-changing view shift when having
      an arbitrary mask. *)
270
  Lemma fupd_mask_frame E E' E1 E2 P :
271 272
    E1  E 
    (|={E1,E2}=> |={E2  (E  E1),E'}=> P) - (|={E,E'}=> P).
273
  Proof.
274 275
    intros ?. rewrite (fupd_mask_frame_r _ _ (E  E1)); last set_solver.
    rewrite fupd_trans.
276
    by replace (E1  E  E1) with E by (by apply union_difference_L).
277
  Qed.
278 279 280 281 282 283 284 285 286
  (* 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).
287
  Proof.
288 289
    intros HE. apply wand_intro_r. rewrite fupd_frame_r.
    rewrite wand_elim_r. clear Q.
290 291 292 293 294 295 296
    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.
297 298 299
    eapply wand_apply;
      last (apply sep_mono; first reflexivity); first reflexivity.
    apply forall_intro=>R. apply wand_intro_r.
300 301 302
    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.
303 304 305 306 307
  Qed.

  Lemma fupd_mask_same E E1 P :
    E = E1  (|={E}=> P) - (|={E,E1}=> P).
  Proof. intros <-. done. Qed.
308 309 310

  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.
311 312 313 314 315 316

  Global Instance fupd_homomorphism E :
    MonoidHomomorphism bi_sep bi_sep (flip ()) (fupd (PROP:=PROP) E E).
  Proof. split; [split|]; try apply _. apply fupd_sep. apply fupd_intro. Qed.

  Lemma big_sepL_fupd {A} E (Φ : nat  A  PROP) l :
317
    ([ list] kx  l, |={E}=> Φ k x) ={E}= [ list] kx  l, Φ k x.
318 319
  Proof. by rewrite (big_opL_commute _). Qed.
  Lemma big_sepM_fupd `{Countable K} {A} E (Φ : K  A  PROP) m :
320
    ([ map] kx  m, |={E}=> Φ k x) ={E}= [ map] kx  m, Φ k x.
321 322
  Proof. by rewrite (big_opM_commute _). Qed.
  Lemma big_sepS_fupd `{Countable A} E (Φ : A  PROP) X :
323
    ([ set] x  X, |={E}=> Φ x) ={E}= [ set] x  X, Φ x.
324 325 326 327
  Proof. by rewrite (big_opS_commute _). Qed.
  Lemma big_sepMS_fupd `{Countable A} E (Φ : A  PROP) l :
    ([ mset] x  l, |={E}=> Φ x)  |={E}=> [ mset] x  l, Φ x.
  Proof. by rewrite (big_opMS_commute _). Qed.
328 329

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

337 338
  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.
339 340 341 342 343 344 345
  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.
346
    intros ??. rewrite -(emp_sep (|={E1,F2}=> P)%I).
347 348 349 350 351
    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.
352
    rewrite [X in (X  _)%I]later_intro -later_sep. f_equiv.
353 354 355 356 357 358 359
    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.
360 361 362 363 364 365 366 367 368 369

  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.

370
  Lemma step_fupd_fupd E E' P : (|={E,E'}=> P)  (|={E,E'}=> |={E}=> P).
371 372 373 374 375 376 377
  Proof.
    apply (anti_symm ()).
    - by rewrite -fupd_intro.
    - by rewrite fupd_trans.
  Qed.

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

383 384 385 386 387 388 389 390 391
  Lemma step_fupdN_wand E1 E2 n P Q :
    (|={E1,E2}=>^n P) - (P - Q) - (|={E1,E2}=>^n Q).
  Proof.
    apply wand_intro_l. induction n as [|n IH]=> /=.
    { by rewrite wand_elim_l. }
    rewrite -IH -fupd_frame_l later_sep -fupd_frame_l.
    by apply sep_mono; first apply later_intro.
  Qed.

392 393 394 395 396 397 398 399 400 401 402 403 404 405
  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.

406 407 408
  Section fupd_plainly_derived.
    Context `{BiPlainly PROP, !BiFUpdPlainly PROP}.

409 410 411 412 413 414 415 416
    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.
417

418 419
    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.
420

421 422 423 424
    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.
425

426 427 428 429 430 431 432 433 434
    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.
435
    Proof.
436 437
      rewrite -fupd_plainly_forall_2. apply forall_mono=> x.
      by rewrite {1}(plain (Φ _)).
438 439
    Qed.

440 441
    Lemma fupd_plainly_laterN E n P `{HP : !Plain P} :
      (^n |={E}=> P)  |={E}=> ^n  P.
442
    Proof.
443 444 445 446
      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.
447 448
    Qed.

449 450 451
    Lemma fupd_plain_forall E1 E2 {A} (Φ : A  PROP) `{! x, Plain (Φ x)} :
      E2  E1 
      (|={E1,E2}=>  x, Φ x)  ( x, |={E1,E2}=> Φ x).
452
    Proof.
453 454 455 456 457 458 459
      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.
460
    Qed.
461 462 463
    Lemma fupd_plain_forall' E {A} (Φ : A  PROP) `{! x, Plain (Φ x)} :
      (|={E}=>  x, Φ x)  ( x, |={E}=> Φ x).
    Proof. by apply fupd_plain_forall. Qed.
464

465 466 467 468 469 470 471
    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.
472 473
    Proof.
      induction n as [|n IH].
474 475 476
      - 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.
477 478 479
        * by rewrite except_0_idemp.
        * by rewrite except_0_later.
    Qed.
480

481 482 483 484 485 486 487 488 489 490 491 492 493
    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.
494
End fupd_derived.