updates.v 22.4 KB
Newer Older
1
From stdpp Require Import coPset.
2
From iris.bi Require Import interface derived_laws_later big_op plainly.
3
From iris Require Import options.
4
Import interface.bi derived_laws.bi derived_laws_later.bi.
5

6 7 8
(* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
Set Default Proof Using "Type*".

Robbert Krebbers's avatar
Robbert Krebbers committed
9 10
(* We first define operational type classes for the notations, and then later
bundle these operational type classes with the laws. *)
11
Class BUpd (PROP : Type) : Type := bupd : PROP  PROP.
12
Instance : Params (@bupd) 2 := {}.
13
Hint Mode BUpd ! : typeclass_instances.
14
Arguments bupd {_}%type_scope {_} _%bi_scope.
15

16 17 18
Notation "|==> Q" := (bupd Q) : bi_scope.
Notation "P ==∗ Q" := (P  |==> Q) (only parsing) : stdpp_scope.
Notation "P ==∗ Q" := (P - |==> Q)%I : bi_scope.
19

20
Class FUpd (PROP : Type) : Type := fupd : coPset  coPset  PROP  PROP.
21
Instance: Params (@fupd) 4 := {}.
22
Hint Mode FUpd ! : typeclass_instances.
23
Arguments fupd {_}%type_scope {_} _ _ _%bi_scope.
24

Ralf Jung's avatar
Ralf Jung committed
25 26 27
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.
28

Ralf Jung's avatar
Ralf Jung committed
29 30 31
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.
32

Ralf Jung's avatar
Ralf Jung committed
33
(** * Step-taking fancy updates. *)
34
(** These have two masks, but they are different than the two masks of a
Ralf Jung's avatar
Ralf Jung committed
35 36 37 38
    mask-changing update: in [|={Eo}[Ei]▷=> Q], the first mask [Eo] ("outer
    mask") holds at the beginning and the end; the second mask [Ei] ("inner
    mask") holds around each ▷. This is also why we use a different notation
    than for the two masks of a mask-changing updates. *)
39 40 41
Notation "|={ Eo } [ Ei ]▷=> Q" := (|={Eo,Ei}=>  |={Ei,Eo}=> Q)%I : bi_scope.
Notation "P ={ Eo } [ Ei ]▷=∗ Q" := (P - |={Eo}[Ei]=> Q)%I : bi_scope.
Notation "P ={ Eo } [ Ei ]▷=∗ Q" := (P - |={Eo}[Ei]=> Q) (only parsing) : stdpp_scope.
42 43 44 45 46

Notation "|={ E }▷=> Q" := (|={E}[E]=> Q)%I : bi_scope.
Notation "P ={ E }▷=∗ Q" := (P ={E}[E]= Q)%I : bi_scope.
Notation "P ={ E }▷=∗ Q" := (P ={E}[E]= Q) : stdpp_scope.

Ralf Jung's avatar
Ralf Jung committed
47 48 49 50 51
(** For the iterated version, in principle there are 4 masks: "outer" and
    "inner" of [|={Eo}[Ei]▷=>], as well as "begin" and "end" masks [E1] and [E2]
    that could potentially differ from [Eo]. The latter can be obtained from
    this notation by adding normal mask-changing update modalities: [
    |={E1,Eo}=> |={Eo}[Ei]▷=>^n |={Eo,E2}=> Q] *)
52 53 54
Notation "|={ Eo } [ Ei ]▷=>^ n Q" := (Nat.iter n (λ P, |={Eo}[Ei]=> P) Q)%I : bi_scope.
Notation "P ={ Eo } [ Ei ]▷=∗^ n Q" := (P - |={Eo}[Ei]=>^n Q)%I : bi_scope.
Notation "P ={ Eo } [ Ei ]▷=∗^ n Q" := (P - |={Eo}[Ei]=>^n Q) (only parsing) : stdpp_scope.
55

56 57 58
Notation "|={ E }▷=>^ n Q" := (|={E}[E]=>^n Q)%I : bi_scope.
Notation "P ={ E }▷=∗^ n Q" := (P ={E}[E]=^n Q)%I : bi_scope.
Notation "P ={ E }▷=∗^ n Q" := (P ={E}[E]=^n Q) (only parsing) : stdpp_scope.
59

Robbert Krebbers's avatar
Robbert Krebbers committed
60
(** Bundled versions  *)
Robbert Krebbers's avatar
Robbert Krebbers committed
61
(* Mixins allow us to create instances easily without having to use Program *)
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
63
  bi_bupd_mixin_bupd_ne : NonExpansive (bupd (PROP:=PROP));
Robbert Krebbers's avatar
Robbert Krebbers committed
64 65 66 67 68 69
  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;
}.

70
Record BiFUpdMixin (PROP : bi) `(FUpd PROP) := {
71
  bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd (PROP:=PROP) E1 E2);
Robbert Krebbers's avatar
Robbert Krebbers committed
72 73 74 75 76 77
  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;
78
  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
79 80 81 82 83 84 85 86 87
}.

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.

88
Class BiFUpd (PROP : bi) := {
Robbert Krebbers's avatar
Robbert Krebbers committed
89 90 91
  bi_fupd_fupd :> FUpd PROP;
  bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
}.
92
Hint Mode BiFUpd ! : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
93 94
Arguments bi_fupd_fupd : simpl never.

95
Class BiBUpdFUpd (PROP : bi) `{BiBUpd PROP, BiFUpd PROP} :=
Robbert Krebbers's avatar
Robbert Krebbers committed
96
  bupd_fupd E (P : PROP) : (|==> P) ={E}= P.
97
Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
98

99
Class BiBUpdPlainly (PROP : bi) `{!BiBUpd PROP, !BiPlainly PROP} :=
Robbert Krebbers's avatar
Robbert Krebbers committed
100
  bupd_plainly (P : PROP) : (|==>  P) - P.
101
Hint Mode BiBUpdPlainly ! - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
102

103 104 105 106
(** 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]. *)
107
Class BiFUpdPlainly (PROP : bi) `{!BiFUpd PROP, !BiPlainly PROP} := {
108 109
  (** When proving a fancy update of a plain proposition, you can also prove it
  while being allowed to open all invariants. *)
110 111
  fupd_plainly_mask_empty E (P : PROP) :
    (|={E,}=>  P)  |={E}=> P;
112 113 114
  (** 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]. *)
115 116
  fupd_plainly_keep_l E (P R : PROP) :
    (R ={E}=  P)  R  |={E}=> P  R;
117 118 119
  (** 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. *)
120 121
  fupd_plainly_later E (P : PROP) :
    ( |={E}=>  P)  |={E}=>   P;
122
  (** Forall quantifiers commute with fancy updates over plain propositions. *)
123 124
  fupd_plainly_forall_2 E {A} (Φ : A  PROP) :
    ( x, |={E}=>  Φ x)  |={E}=>  x, Φ x
Robbert Krebbers's avatar
Robbert Krebbers committed
125
}.
126
Hint Mode BiBUpdFUpd ! - - : typeclass_instances.
Robbert Krebbers's avatar
Robbert Krebbers committed
127

Robbert Krebbers's avatar
Robbert Krebbers committed
128 129 130 131 132 133 134 135 136 137 138 139 140 141 142
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.
143

Robbert Krebbers's avatar
Robbert Krebbers committed
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
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.
161
  Lemma fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P)  R ={E1,E2}= P  R.
Robbert Krebbers's avatar
Robbert Krebbers committed
162 163
  Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed.
End fupd_laws.
164 165

Section bupd_derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
166 167
  Context `{BiBUpd PROP}.
  Implicit Types P Q R : PROP.
168

169
  (* FIXME: Removing the `PROP:=` diverges. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
170 171
  Global Instance bupd_proper :
    Proper (() ==> ()) (bupd (PROP:=PROP)) := ne_proper _.
172 173

  (** BUpd derived rules *)
174
  Global Instance bupd_mono' : Proper (() ==> ()) (bupd (PROP:=PROP)).
175
  Proof. intros P Q; apply bupd_mono. Qed.
176
  Global Instance bupd_flip_mono' : Proper (flip () ==> flip ()) (bupd (PROP:=PROP)).
177 178 179 180 181
  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.
182
  Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
183
  Lemma bupd_wand_r P Q : (|==> P)  (P - Q) == Q.
184
  Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
185 186
  Lemma bupd_sep P Q : (|==> P)  (|==> Q) == P  Q.
  Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.
187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203

  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
204 205 206

  Lemma except_0_bupd P :  (|==> P)  (|==>  P).
  Proof.
207
    rewrite /bi_except_0. apply or_elim; eauto using bupd_mono, or_intro_r.
208
    by rewrite -bupd_intro -or_intro_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
209
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
210

211
  Section bupd_plainly.
212
    Context `{!BiPlainly PROP, !BiBUpdPlainly PROP}.
213 214 215 216 217 218 219 220 221 222 223 224 225

    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.
226
End bupd_derived.
227 228

Section fupd_derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
229 230
  Context `{BiFUpd PROP}.
  Implicit Types P Q R : PROP.
231

Robbert Krebbers's avatar
Robbert Krebbers committed
232 233
  Global Instance fupd_proper E1 E2 :
    Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2) := ne_proper _.
234 235

  (** FUpd derived rules *)
236
  Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (fupd (PROP:=PROP) E1 E2).
237 238
  Proof. intros P Q; apply fupd_mono. Qed.
  Global Instance fupd_flip_mono' E1 E2 :
239
    Proper (flip () ==> flip ()) (fupd (PROP:=PROP) E1 E2).
240 241 242
  Proof. intros P Q; apply fupd_mono. Qed.

  Lemma fupd_intro E P : P ={E}= P.
Robbert Krebbers's avatar
Robbert Krebbers committed
243
  Proof. by rewrite {1}(fupd_intro_mask E E P) // fupd_trans. Qed.
Gregory Malecha's avatar
Gregory Malecha committed
244
  Lemma fupd_intro_mask' E1 E2 : E2  E1  @{PROP} |={E1,E2}=> |={E2,E1}=> emp.
245 246 247 248
  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.

249 250
  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.
251
  Lemma fupd_wand_l E1 E2 P Q : (P - Q)  (|={E1,E2}=> P) ={E1,E2}= Q.
252
  Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
253
  Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}= Q.
254
  Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
255

256 257 258 259 260 261 262
  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.

263 264 265
  Lemma fupd_trans_frame E1 E2 E3 P Q :
    ((Q ={E2,E3}= emp)  |={E1,E2}=> (Q  P)) ={E1,E3}= P.
  Proof.
266
    rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
267 268 269
    by rewrite fupd_frame_r left_id fupd_trans.
  Qed.

270 271 272 273
  Lemma fupd_elim E1 E2 E3 P Q :
    (Q - (|={E2,E3}=> P))  (|={E1,E2}=> Q) - (|={E1,E3}=> P).
  Proof. intros ->. rewrite fupd_trans //. Qed.

274 275 276 277
  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.
278
    apply impl_intro_l, and_elim_r.
279 280 281 282 283
  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.
284 285
  (** How to apply an arbitrary mask-changing view shift when having
      an arbitrary mask. *)
286
  Lemma fupd_mask_frame E E' E1 E2 P :
287 288
    E1  E 
    (|={E1,E2}=> |={E2  (E  E1),E'}=> P) - (|={E,E'}=> P).
289
  Proof.
290 291
    intros ?. rewrite (fupd_mask_frame_r _ _ (E  E1)); last set_solver.
    rewrite fupd_trans.
292
    by replace (E1  E  E1) with E by (by apply union_difference_L).
293
  Qed.
294 295 296 297 298 299 300 301 302
  (* 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).
303
  Proof.
304 305
    intros HE. apply wand_intro_r. rewrite fupd_frame_r.
    rewrite wand_elim_r. clear Q.
306 307 308 309 310 311 312
    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.
313 314 315
    eapply wand_apply;
      last (apply sep_mono; first reflexivity); first reflexivity.
    apply forall_intro=>R. apply wand_intro_r.
316 317 318
    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.
319 320 321 322 323
  Qed.

  Lemma fupd_mask_same E E1 P :
    E = E1  (|={E}=> P) - (|={E,E1}=> P).
  Proof. intros <-. done. Qed.
324 325 326

  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.
327 328 329 330 331 332

  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 :
333
    ([ list] kx  l, |={E}=> Φ k x) ={E}= [ list] kx  l, Φ k x.
334 335
  Proof. by rewrite (big_opL_commute _). Qed.
  Lemma big_sepM_fupd `{Countable K} {A} E (Φ : K  A  PROP) m :
336
    ([ map] kx  m, |={E}=> Φ k x) ={E}= [ map] kx  m, Φ k x.
337 338
  Proof. by rewrite (big_opM_commute _). Qed.
  Lemma big_sepS_fupd `{Countable A} E (Φ : A  PROP) X :
339
    ([ set] x  X, |={E}=> Φ x) ={E}= [ set] x  X, Φ x.
340 341 342 343
  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.
344 345

  (** Fancy updates that take a step derived rules. *)
346
  Lemma step_fupd_wand Eo Ei P Q : (|={Eo}[Ei]=> P) - (P - Q) - |={Eo}[Ei]=> Q.
347
  Proof.
348 349 350
    apply wand_intro_l.
    by rewrite (later_intro (P - Q)%I) fupd_frame_l -later_sep fupd_frame_l
               wand_elim_l.
351 352
  Qed.

353 354
  Lemma step_fupd_mask_frame_r Eo Ei Ef P :
    Eo ## Ef  Ei ## Ef  (|={Eo}[Ei]=> P)  |={Eo  Ef}[Ei  Ef]=> P.
355 356 357 358
  Proof.
    intros. rewrite -fupd_mask_frame_r //. do 2 f_equiv. by apply fupd_mask_frame_r.
  Qed.

359 360
  Lemma step_fupd_mask_mono Eo1 Eo2 Ei1 Ei2 P :
    Ei2  Ei1  Eo1  Eo2  (|={Eo1}[Ei1]=> P)  |={Eo2}[Ei2]=> P.
361
  Proof.
362 363 364 365 366
    intros ??. rewrite -(emp_sep (|={Eo1}[Ei1]=> P)%I).
    rewrite (fupd_intro_mask Eo2 Eo1 emp%I) //.
    rewrite fupd_frame_r -(fupd_trans Eo2 Eo1 Ei2). f_equiv.
    rewrite fupd_frame_l -(fupd_trans Eo1 Ei1 Ei2). f_equiv.
    rewrite (fupd_intro_mask Ei1 Ei2 (|={_,_}=> emp)%I) //.
367
    rewrite fupd_frame_r. f_equiv.
368
    rewrite [X in (X  _)%I]later_intro -later_sep. f_equiv.
369 370
    rewrite fupd_frame_r -(fupd_trans Ei2 Ei1 Eo2). f_equiv.
    rewrite fupd_frame_l -(fupd_trans Ei1 Eo1 Eo2). f_equiv.
371 372 373
    by rewrite fupd_frame_r left_id.
  Qed.

374 375
  Lemma step_fupd_intro Ei Eo P : Ei  Eo   P - |={Eo}[Ei]=> P.
  Proof. intros. by rewrite -(step_fupd_mask_mono Ei _ Ei _) // -!fupd_intro. Qed.
376

377 378
  Lemma step_fupd_frame_l Eo Ei R Q :
    (R  |={Eo}[Ei]=> Q) - |={Eo}[Ei]=> (R  Q).
379 380 381 382 383 384 385
  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.

386
  Lemma step_fupd_fupd Eo Ei P : (|={Eo}[Ei]=> P)  (|={Eo}[Ei]=> |={Eo}=> P).
387 388 389 390 391 392
  Proof.
    apply (anti_symm ()).
    - by rewrite -fupd_intro.
    - by rewrite fupd_trans.
  Qed.

393 394
  Lemma step_fupdN_mono Eo Ei n P Q :
    (P  Q)  (|={Eo}[Ei]=>^n P)  (|={Eo}[Ei]=>^n Q).
395 396 397 398
  Proof.
    intros HPQ. induction n as [|n IH]=> //=. rewrite IH //.
  Qed.

399 400
  Lemma step_fupdN_wand Eo Ei n P Q :
    (|={Eo}[Ei]=>^n P) - (P - Q) - (|={Eo}[Ei]=>^n Q).
401 402 403 404 405 406 407
  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.

408
  Lemma step_fupdN_S_fupd n E P:
409
    (|={E}[]=>^(S n) P)  (|={E}[]=>^(S n) |={E}=> P).
410 411 412 413 414
  Proof.
    apply (anti_symm ()); rewrite !Nat_iter_S_r; apply step_fupdN_mono;
      rewrite -step_fupd_fupd //.
  Qed.

415 416
  Lemma step_fupdN_frame_l Eo Ei n R Q :
    (R  |={Eo}[Ei]=>^n Q) - |={Eo}[Ei]=>^n (R  Q).
417 418 419 420 421
  Proof.
    induction n as [|n IH]; simpl; [done|].
    rewrite step_fupd_frame_l IH //=.
  Qed.

422
  Section fupd_plainly_derived.
423
    Context `{!BiPlainly PROP, !BiFUpdPlainly PROP}.
424

425 426 427 428 429 430 431 432
    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.
433

434 435
    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.
436

437 438 439 440
    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.
441

442 443 444 445 446 447 448
    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.
449 450 451 452 453 454
    Lemma fupd_plain_laterN E n P `{!Plain P} : (^n |={E}=> P)  |={E}=> ^n  P.
    Proof.
      induction n as [|n IH]; simpl; [by rewrite -except_0_intro|].
      by rewrite IH fupd_plain_later except_0_laterN except_0_idemp.
    Qed.

455 456
    Lemma fupd_plain_forall_2 E {A} (Φ : A  PROP) `{! x, Plain (Φ x)} :
      ( x, |={E}=> Φ x)  |={E}=>  x, Φ x.
457
    Proof.
458 459
      rewrite -fupd_plainly_forall_2. apply forall_mono=> x.
      by rewrite {1}(plain (Φ _)).
460 461
    Qed.

462 463
    Lemma fupd_plainly_laterN E n P `{HP : !Plain P} :
      (^n |={E}=> P)  |={E}=> ^n  P.
464
    Proof.
465 466 467 468
      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.
469 470
    Qed.

471 472 473
    Lemma fupd_plain_forall E1 E2 {A} (Φ : A  PROP) `{! x, Plain (Φ x)} :
      E2  E1 
      (|={E1,E2}=>  x, Φ x)  ( x, |={E1,E2}=> Φ x).
474
    Proof.
475 476 477 478 479 480 481
      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.
482
    Qed.
483 484 485
    Lemma fupd_plain_forall' E {A} (Φ : A  PROP) `{! x, Plain (Φ x)} :
      (|={E}=>  x, Φ x)  ( x, |={E}=> Φ x).
    Proof. by apply fupd_plain_forall. Qed.
486

487
    Lemma step_fupd_plain Eo Ei P `{!Plain P} : (|={Eo}[Ei]=> P) ={Eo}=   P.
488
    Proof.
489
      rewrite -(fupd_plain_mask _ Ei (  P)%I).
490 491 492
      apply fupd_elim. by rewrite fupd_plain_mask -fupd_plain_later.
    Qed.

493
    Lemma step_fupdN_plain Eo Ei n P `{!Plain P} : (|={Eo}[Ei]=>^n P) ={Eo}= ^n  P.
494 495
    Proof.
      induction n as [|n IH].
496 497 498
      - 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.
499 500 501
        * by rewrite except_0_idemp.
        * by rewrite except_0_later.
    Qed.
502

503 504 505
    Lemma step_fupd_plain_forall Eo Ei {A} (Φ : A  PROP) `{! x, Plain (Φ x)} :
      Ei  Eo 
      (|={Eo}[Ei]=>  x, Φ x)  ( x, |={Eo}[Ei]=> Φ x).
506 507 508
    Proof.
      intros. apply (anti_symm _).
      { apply forall_intro=> x. by rewrite (forall_elim x). }
509
      trans ( x, |={Eo}=>   Φ x)%I.
510 511
      { apply forall_mono=> x. by rewrite step_fupd_plain. }
      rewrite -fupd_plain_forall'. apply fupd_elim.
512
      rewrite -(fupd_except_0 Ei Eo) -step_fupd_intro //.
513 514 515
      by rewrite -later_forall -except_0_forall.
    Qed.
  End fupd_plainly_derived.
516
End fupd_derived.