(* iris/bi/updates.v *)
From stdpp Require Import coPset
From iris.bi Require Import interface derived_laws_later big_op plainly
From iris.prelude Require Import options

Local SetPrimitive Projections.

Class BUpd(PROP : Type) : Type := bupd : PROP → PROP.

Global Instance: Params (@bupd) 2 := {}.

Global HintMode BUpd ! : typeclass_instances.

Global Argumentsbupd {_}%_type_scope {_} _%_bi_scope.

Global TypeclassesOpaque bupd.

Class FUpd(PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.

Global Instance: Params (@fupd) 4 := {}.

Global HintMode FUpd ! : typeclass_instances.

Global Argumentsfupd {_}%_type_scope {_} _ _ _%_bi_scope.

Global TypeclassesOpaque fupd.

Record BiBUpdMixin(PROP : bi) `(BUpd PROP) := {
  bi_bupd_mixin_bupd_ne : NonExpansive (bupd (PROP:=PROP));
  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 : bi) `(FUpd PROP) := {
  bi_fupd_mixin_fupd_ne E1 E2 :
    NonExpansive (fupd (PROP:=PROP) E1 E2);
  bi_fupd_mixin_fupd_mask_subseteq E1 E2 :
    E2 ⊆ E1 → ⊢@{PROP} |={E1,E2}=> |={E2,E1}=> emp;
  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 R : PROP) :
    (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R;
}.

Class BiBUpd(PROP : bi) := {
  #[global] bi_bupd_bupd :: BUpd PROP;
  bi_bupd_mixin : BiBUpdMixin PROP bi_bupd_bupd;
}.

Global HintMode BiBUpd ! : typeclass_instances.

Global Argumentsbi_bupd_bupd : simpl never.

Class BiFUpd(PROP : bi) := {
  #[global] bi_fupd_fupd :: FUpd PROP;
  bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
}.

Global HintMode BiFUpd ! : typeclass_instances.

Global Argumentsbi_fupd_fupd : simpl never.

Class BiBUpdFUpd(PROP : bi) `{BiBUpd PROP, BiFUpd PROP} :=
  bupd_fupd E (P : PROP) : (|==> P) ⊢ |={E}=> P.

Global HintMode BiBUpdFUpd ! - - : typeclass_instances.

Class BiBUpdSbi(PROP : bi) `{!BiBUpd PROP, !Sbi PROP} :=
  bupd_si_pure Pi : (|==> <si_pure> Pi) ⊢@{PROP} <si_pure> Pi.

Global HintMode BiBUpdSbi ! - - : typeclass_instances.

Class BiFUpdSbi(PROP : bi) `{!BiFUpd PROP, !Sbi PROP} := {

Global HintMode BiBUpdFUpd ! - - : typeclass_instances.

Global Instancebupd_ne : NonExpansive (@bupd PROP _).
  Proof. eapply bi_bupd_mixin_bupd_ne, bi_bupd_mixin. Qed.

Lemma bupd_introP : 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.

Global Instancefupd_ne E1 E2 : NonExpansive (@fupd PROP _ E1 E2).
  Proof. eapply bi_fupd_mixin_fupd_ne, bi_fupd_mixin. Qed.

Lemma fupd_mask_subseteq{E1} E2 : E2 ⊆ E1 → ⊢@{PROP} |={E1,E2}=> |={E2,E1}=> emp.
  Proof. eapply bi_fupd_mixin_fupd_mask_subseteq, bi_fupd_mixin. Qed.

Lemma except_0_fupdE1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ⊢ |={E1,E2}=> P.
  Proof. eapply bi_fupd_mixin_except_0_fupd, bi_fupd_mixin. Qed.

Lemma fupd_monoE1 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_transE1 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_rE1 E2 (P R : PROP) : (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R.
  Proof. eapply bi_fupd_mixin_fupd_frame_r, bi_fupd_mixin. Qed.

Global Instancebupd_proper :
    Proper ((≡) ==> (≡)) (bupd (PROP:=PROP)) := ne_proper _.

Global Instancebupd_mono' : Proper ((⊢) ==> (⊢)) (bupd (PROP:=PROP)).
  Proof. intros P Q; apply bupd_mono. Qed.

Global Instancebupd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (bupd (PROP:=PROP)).
  Proof. intros P Q; apply bupd_mono. Qed.

Lemma bupd_frame_lR Q : (R ∗ |==> Q) ⊢ |==> R ∗ Q.
  Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.

Lemma bupd_wand_lP Q : (P -∗ Q) ∗ (|==> P) ⊢ |==> Q.
  Proof. by rewrite bupd_frame_l wand_elim_l. Qed.

Lemma bupd_wand_rP Q : (|==> P) ∗ (P -∗ Q) ⊢ |==> Q.
  Proof. by rewrite bupd_frame_r wand_elim_r. Qed.

Lemma bupd_sepP Q : (|==> P) ∗ (|==> Q) ⊢ |==> P ∗ Q.
  Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed.

Lemma bupd_idempP : (|==> |==> P) ⊣⊢ |==> P.
  Proof.
    apply: anti_symm.
    - apply bupd_trans.
    - apply bupd_intro.
  Qed.

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

Lemma bupd_orP Q : (|==> P) ∨ (|==> Q) ⊢ |==> (P ∨ Q).
  Proof. apply or_elim; apply bupd_mono; [ apply or_intro_l | apply or_intro_r ]. Qed.

Global Instancebupd_or_homomorphism :
    MonoidHomomorphism bi_or bi_or (flip (⊢)) (bupd (PROP:=PROP)).
  Proof. split; [split|]; try apply _; [apply bupd_or | apply bupd_intro]. Qed.

Lemma bupd_andP Q : (|==> (P ∧ Q)) ⊢ (|==> P) ∧ (|==> Q).
  Proof. apply and_intro; apply bupd_mono; [apply and_elim_l | apply and_elim_r]. Qed.

Lemma bupd_existA (Φ : A → PROP) : (∃ x : A, |==> Φ x) ⊢ |==> ∃ x : A, Φ x.
  Proof. apply exist_elim=> a. by rewrite -(exist_intro a). Qed.

Lemma bupd_forallA (Φ : A → PROP) : (|==> ∀ x : A, Φ x) ⊢ ∀ x : A, |==> Φ x.
  Proof. apply forall_intro=> a. by rewrite -(forall_elim a). Qed.

Lemma big_sepL_bupd{A} (Φ : nat → A → PROP) l :
    ([∗ list] k↦x ∈ l, |==> Φ k x) ⊢ |==> [∗ list] k↦x ∈ l, Φ k x.
  Proof. by rewrite (big_opL_commute _). Qed.

Lemma big_sepM_bupd{A} `{Countable K} (Φ : K → A → PROP) l :
    ([∗ map] k↦x ∈ l, |==> Φ k x) ⊢ |==> [∗ map] k↦x ∈ l, Φ k x.
  Proof. by rewrite (big_opM_commute _). Qed.

Lemma big_sepM2_bupd{A B} `{Countable K} (Φ : K → A → B → PROP) l1 l2 :
    ([∗ map] k↦a;b ∈ l1;l2, |==> Φ k a b) ⊢ |==> [∗ map] k↦a;b ∈ l1;l2, Φ k a b.
  Proof.
    rewrite !big_sepM2_alt big_sepM_bupd.
    rewrite !persistent_and_affinely_sep_l bupd_frame_l //.
  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.

Lemma except_0_bupdP : ◇ (|==> P) ⊢ (|==> ◇ P).
  Proof.
    rewrite /bi_except_0. apply or_elim; eauto using bupd_mono, or_intro_r.
    by rewrite -bupd_intro -or_intro_l.
  Qed.

Global Instancebupd_absorbing P :
    Absorbing P → Absorbing (|==> P).
  Proof. rewrite /Absorbing /bi_absorbingly bupd_frame_l =>-> //. Qed.

Lemma bupd_plainlyP : (|==> ■ P) ⊢ ■ P.
    Proof. apply bupd_si_pure. Qed.

Lemma bupd_plainly_elimP `{!Absorbing P} : (|==> ■ P) ⊢ P.
    Proof. by rewrite bupd_plainly plainly_elim. Qed.

Lemma bupd_elimP `{!Plain P, !Absorbing P} : (|==> P) ⊢ P.
    Proof.
      by rewrite {1}(plain P) /plainly bupd_si_pure si_pure_si_emp_valid_elim.
    Qed.

Lemma bupd_plain_forall{A} (Φ : A → PROP)
        `{!∀ x, Plain (Φ x), !∀ x, Absorbing (Φ x)} :
      (|==> ∀ x, Φ x) ⊣⊢ (∀ x, |==> Φ x).
    Proof.
      apply (anti_symm _).
      - apply bupd_forall.
      - rewrite -bupd_intro. apply forall_intro=> x.
        by rewrite (forall_elim x) bupd_elim.
    Qed.

Global Instancebupd_plain P : Plain P → Plain (|==> P).
    Proof.
      intros. rewrite /Plain. rewrite {1}(plain P) {1}bupd_elim.
      by rewrite -bupd_intro.
    Qed.

Global Instancefupd_proper E1 E2 :
    Proper ((≡) ==> (≡)) (fupd (PROP:=PROP) E1 E2) := ne_proper _.

Global Instancefupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd (PROP:=PROP) E1 E2).
  Proof. intros P Q; apply fupd_mono. Qed.

Global Instancefupd_flip_mono' E1 E2 :
    Proper (flip (⊢) ==> flip (⊢)) (fupd (PROP:=PROP) E1 E2).
  Proof. intros P Q; apply fupd_mono. Qed.

Lemma fupd_mask_intro_subseteqE1 E2 P :
    E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
  Proof.
    intros HE.
    apply wand_entails', wand_intro_r.
    rewrite fupd_mask_subseteq; last exact: HE.
    rewrite !fupd_frame_r. rewrite left_id. done.
  Qed.

Lemma fupd_introE P : P ⊢ |={E}=> P.
  Proof. by rewrite {1}(fupd_mask_intro_subseteq E E P) // fupd_trans. Qed.

Lemma fupd_except_0E1 E2 P : (|={E1,E2}=> ◇ P) ⊢ |={E1,E2}=> P.
  Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.

Lemma fupd_idempE P : (|={E}=> |={E}=> P) ⊣⊢ |={E}=> P.
  Proof.
    apply: anti_symm.
    - apply fupd_trans.
    - apply fupd_intro.
  Qed.

Lemma fupd_mask_weaken{E1} E2 {E3 P} :
    E2 ⊆ E1 →
    ((|={E2,E1}=> emp) ={E2,E3}=∗ P) ⊢ |={E1,E3}=> P.
  Proof.
    intros HE.
    apply wand_entails', wand_intro_r.
    rewrite {1}(fupd_mask_subseteq E2) //.
    rewrite fupd_frame_r. by rewrite wand_elim_r fupd_trans.
  Qed.

Lemma fupd_mask_introE1 E2 P :
    E2 ⊆ E1 →
    ((|={E2,E1}=> emp) -∗ P) ⊢ |={E1,E2}=> P.
  Proof.
    intros. etrans; [|by apply fupd_mask_weaken]. by rewrite -fupd_intro.
  Qed.

Lemma fupd_mask_intro_discardE1 E2 P `{!Absorbing P} :
    E2 ⊆ E1 → P ⊢ |={E1,E2}=> P.
  Proof.
    intros. etrans; [|by apply fupd_mask_intro].
    apply wand_intro_r. rewrite sep_elim_l. done.
  Qed.

Lemma fupd_frame_lE1 E2 R Q : (R ∗ |={E1,E2}=> Q) ⊢ |={E1,E2}=> R ∗ Q.
  Proof. rewrite !(comm _ R); apply fupd_frame_r. Qed.

Lemma fupd_wand_lE1 E2 P Q : (P -∗ Q) ∗ (|={E1,E2}=> P) ⊢ |={E1,E2}=> Q.
  Proof. by rewrite fupd_frame_l wand_elim_l. Qed.

Lemma fupd_wand_rE1 E2 P Q : (|={E1,E2}=> P) ∗ (P -∗ Q) ⊢ |={E1,E2}=> Q.
  Proof. by rewrite fupd_frame_r wand_elim_r. Qed.

Global Instancefupd_absorbing E1 E2 P :
    Absorbing P → Absorbing (|={E1,E2}=> P).
  Proof. rewrite /Absorbing /bi_absorbingly fupd_frame_l =>-> //. Qed.

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

Lemma fupd_elimE1 E2 E3 P Q :
    (Q ⊢ (|={E2,E3}=> P)) → (|={E1,E2}=> Q) ⊢ (|={E1,E3}=> P).
  Proof. intros ->. rewrite fupd_trans //. Qed.

Lemma fupd_mask_frame_rE1 E2 Ef P :
    E1 ## Ef → (|={E1,E2}=> P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P.
  Proof.
    intros ?. rewrite -fupd_mask_frame_r' //. f_equiv.
    apply impl_intro_l, and_elim_r.
  Qed.

Lemma fupd_mask_monoE1 E2 P : E1 ⊆ E2 → (|={E1}=> P) ⊢ |={E2}=> P.
  Proof.
    intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
  Qed.

Lemma fupd_mask_frameE E' E1 E2 P :
    E1 ⊆ E →
    (|={E1,E2}=> |={E2 ∪ (E ∖ E1),E'}=> P) ⊢ (|={E,E'}=> P).
  Proof.
    intros ?. rewrite (fupd_mask_frame_r _ _ (E ∖ E1)); last set_solver.
    rewrite fupd_trans.
    by replace (E1 ∪ E ∖ E1) with E by (by apply union_difference_L).
  Qed.

Lemma fupd_mask_frame_accE E' E1 E2 P Q :
    E1 ⊆ E →
    (|={E1,E1∖E2}=> Q) -∗
    (Q -∗ |={E∖E2,E'}=> (∀ R, (|={E1∖E2,E1}=> R) -∗ |={E∖E2,E}=> R) -∗  P) -∗
    (|={E,E'}=> P).
  Proof.
    intros HE. apply entails_wand, wand_intro_r. rewrite fupd_frame_r.
    rewrite wand_elim_r. clear Q.
    rewrite -(fupd_mask_frame E E'); first apply fupd_mono; last done.

Lemma fupd_mask_subseteq_emptyset_differenceE1 E2 :
    E2 ⊆ E1 →
    ⊢@{PROP} |={E1, E2}=> |={∅, E1∖E2}=> emp.
  Proof.
    intros ?. rewrite [in fupd E1](union_difference_L E2 E1); [|done].
    rewrite (comm_L (∪))
      -[X in fupd _ X](left_id_L ∅ (∪) E2) -fupd_mask_frame_r; [|set_solver+].
    apply fupd_mask_intro_subseteq; set_solver.
  Qed.

Lemma fupd_orE1 E2 P Q :
    (|={E1,E2}=> P) ∨ (|={E1,E2}=> Q) ⊢@{PROP}
    (|={E1,E2}=> (P ∨ Q)).
  Proof. apply or_elim; apply fupd_mono; [ apply or_intro_l | apply or_intro_r ]. Qed.

Global Instancefupd_or_homomorphism E :
    MonoidHomomorphism bi_or bi_or (flip (⊢)) (fupd (PROP:=PROP) E E).
  Proof. split; [split|]; try apply _; [apply fupd_or | apply fupd_intro]. Qed.

Lemma fupd_andE1 E2 P Q :
    (|={E1,E2}=> (P ∧ Q)) ⊢@{PROP} (|={E1,E2}=> P) ∧ (|={E1,E2}=> Q).
  Proof. apply and_intro; apply fupd_mono; [apply and_elim_l | apply and_elim_r]. Qed.

Lemma fupd_existE1 E2 A (Φ : A → PROP) :
    (∃ x : A, |={E1, E2}=> Φ x) ⊢ |={E1, E2}=> ∃ x : A, Φ x.
  Proof. apply exist_elim=> a. by rewrite -(exist_intro a). Qed.

Lemma fupd_forallE1 E2 A (Φ : A → PROP) :
    (|={E1, E2}=> ∀ x : A, Φ x) ⊢ ∀ x : A, |={E1, E2}=> Φ x.
  Proof. apply forall_intro=> a. by rewrite -(forall_elim a). Qed.

Lemma fupd_sepE P Q : (|={E}=> P) ∗ (|={E}=> Q) ⊢ |={E}=> P ∗ Q.
  Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.

Global Instancefupd_sep_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 :
    ([∗ list] k↦x ∈ l, |={E}=> Φ k x) ⊢ |={E}=> [∗ list] k↦x ∈ l, Φ k x.
  Proof. by rewrite (big_opL_commute _). Qed.

Lemma big_sepL2_fupd{A B} E (Φ : nat → A → B → PROP) l1 l2 :
    ([∗ list] k↦x;y ∈ l1;l2, |={E}=> Φ k x y) ⊢ |={E}=> [∗ list] k↦x;y ∈ l1;l2, Φ k x y.
  Proof.
    rewrite !big_sepL2_alt !persistent_and_affinely_sep_l.
    etrans; [| by apply fupd_frame_l]. apply sep_mono_r. apply big_sepL_fupd.
  Qed.

Lemma big_sepM_fupd`{Countable K} {A} E (Φ : K → A → PROP) m :
    ([∗ map] k↦x ∈ m, |={E}=> Φ k x) ⊢ |={E}=> [∗ map] k↦x ∈ m, Φ k x.
  Proof. by rewrite (big_opM_commute _). Qed.

Lemma big_sepM2_fupd`{Countable K} {A B} E (Φ : K → A → B → PROP) m m' :
    ([∗ map] k↦x;y ∈ m;m', |={E}=> Φ k x y) ⊢ |={E}=> [∗ map] k↦x;y ∈ m;m', Φ k x y.
  Proof.
    rewrite !big_sepM2_alt big_sepM_fupd.
    rewrite !persistent_and_affinely_sep_l fupd_frame_l //.
  Qed.

Lemma big_sepS_fupd`{Countable A} E (Φ : A → PROP) X :
    ([∗ set] x ∈ X, |={E}=> Φ x) ⊢ |={E}=> [∗ set] x ∈ X, Φ x.
  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.

Lemma step_fupd_wandEo Ei P Q : (|={Eo}[Ei]▷=> P) -∗ (P -∗ Q) -∗ |={Eo}[Ei]▷=> Q.
  Proof.
    apply entails_wand, wand_intro_l.
    by rewrite (later_intro (P -∗ Q)) fupd_frame_l -later_sep fupd_frame_l
               wand_elim_l.
  Qed.

Lemma step_fupd_mask_frame_rEo Ei Ef P :
    Eo ## Ef → Ei ## Ef → (|={Eo}[Ei]▷=> P) ⊢ |={Eo ∪ Ef}[Ei ∪ Ef]▷=> P.
  Proof.
    intros. rewrite -fupd_mask_frame_r //. do 2 f_equiv. by apply fupd_mask_frame_r.
  Qed.

Lemma step_fupd_mask_monoEo1 Eo2 Ei1 Ei2 P :
    Ei2 ⊆ Ei1 → Eo1 ⊆ Eo2 → (|={Eo1}[Ei1]▷=> P) ⊢ |={Eo2}[Ei2]▷=> P.
  Proof.
    intros ??. rewrite -(emp_sep (|={Eo1}[Ei1]▷=> P)%I).
    rewrite (fupd_mask_intro_subseteq Eo2 Eo1 emp) //.
    rewrite fupd_frame_r -(fupd_trans Eo2 Eo1 Ei2). f_equiv.
    rewrite fupd_frame_l -(fupd_trans Eo1 Ei1 Ei2). f_equiv.
    rewrite (fupd_mask_intro_subseteq Ei1 Ei2 (|={_,_}=> emp)) //.
    rewrite fupd_frame_r. f_equiv.
    rewrite [X in (X ∗ _)%I]later_intro -later_sep. f_equiv.
    rewrite fupd_frame_r -(fupd_trans Ei2 Ei1 Eo2). f_equiv.
    rewrite fupd_frame_l -(fupd_trans Ei1 Eo1 Eo2). f_equiv.
    by rewrite fupd_frame_r left_id.
  Qed.

Lemma step_fupd_introEi Eo P : Ei ⊆ Eo → ▷ P ⊢ |={Eo}[Ei]▷=> P.
  Proof. intros. by rewrite -(step_fupd_mask_mono Ei _ Ei _) // -!fupd_intro. Qed.

Lemma step_fupd_frame_lEo Ei R Q :
    (R ∗ |={Eo}[Ei]▷=> Q) ⊢ |={Eo}[Ei]▷=> (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_fupdEo Ei P : (|={Eo}[Ei]▷=> P) ⊣⊢ (|={Eo}[Ei]▷=> |={Eo}=> P).
  Proof.
    apply (anti_symm (⊢)).
    - by rewrite -fupd_intro.
    - by rewrite fupd_trans.
  Qed.

Lemma step_fupdN_monoEo Ei n P Q :
    (P ⊢ Q) → (|={Eo}[Ei]▷=>^n P) ⊢ (|={Eo}[Ei]▷=>^n Q).
  Proof.
    intros HPQ. induction n as [|n IH]=> //=. rewrite IH //.
  Qed.

Lemma step_fupdN_wandEo Ei n P Q :
    (|={Eo}[Ei]▷=>^n P) -∗ (P -∗ Q) -∗ (|={Eo}[Ei]▷=>^n Q).
  Proof.
    apply entails_wand, 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.

Lemma step_fupdN_introEi Eo n P : Ei ⊆ Eo → ▷^n P ⊢ |={Eo}[Ei]▷=>^n P.
  Proof.
    induction n as [|n IH]=> ?; [done|].
    rewrite /= -step_fupd_intro; [|done]. by rewrite IH.
  Qed.

Lemma step_fupdN_S_fupdn E P :
    (|={E}[∅]▷=>^(S n) P) ⊣⊢ (|={E}[∅]▷=>^(S n) |={E}=> P).
  Proof.
    apply (anti_symm (⊢)); rewrite !Nat.iter_succ_r; apply step_fupdN_mono;
      rewrite -step_fupd_fupd //.
  Qed.

Lemma step_fupdN_frame_lEo Ei n R Q :
    (R ∗ |={Eo}[Ei]▷=>^n Q) ⊢ |={Eo}[Ei]▷=>^n (R ∗ Q).
  Proof.
    induction n as [|n IH]; simpl; [done|].
    rewrite step_fupd_frame_l IH //=.
  Qed.

Lemma step_fupdN_addn m Eo Ei P :
    (|={Eo}[Ei]▷=>^(n+m) P) ⊣⊢ (|={Eo}[Ei]▷=>^n |={Eo}[Ei]▷=>^m P).
  Proof.
    induction n as [ | n IH]; simpl; [done | by rewrite IH].
  Qed.

Lemma step_fupdN_len m Eo Ei P :
    n ≤ m → Ei ⊆ Eo → (|={Eo}[Ei]▷=>^n P) ⊢ (|={Eo}[Ei]▷=>^m P).
  Proof.
    intros ??. replace m with ((m - n) + n) by lia.
    rewrite step_fupdN_add.
    rewrite -(step_fupdN_intro _ _ (m - n)); last done.
    by rewrite -laterN_intro.
  Qed.

Lemma fupd_plainly_keep_lE E' (P R : PROP) :
      (R ={E,E'}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R.
    Proof. by rewrite /plainly fupd_si_pure_keep_l si_pure_si_emp_valid_elim. Qed.

Lemma fupd_plainly_laterE P : (▷ |={E}=> ■ P) ⊢ |={E}=> ▷ ◇ P.
    Proof.
      by rewrite /plainly fupd_si_pure_later si_pure_si_emp_valid_elim.
    Qed.

Lemma fupd_plainly_forall_2E {A} (Φ : A → PROP) :
      (∀ x, |={E}=> ■ Φ x) ⊢ |={E}=> ∀ x, Φ x.
    Proof.
      rewrite /plainly fupd_si_pure_forall_2.
      by setoid_rewrite si_pure_si_emp_valid_elim; last apply _.
    Qed.

Lemma fupd_plainly_maskE E' P : (|={E,E'}=> ■ P) ⊢ |={E}=> P.
    Proof.
      trans (|={E}=> P ∗ emp)%I; last by rewrite right_id.
      rewrite -fupd_plainly_keep_l.
      rewrite right_id left_id. done.
    Qed.

Lemma fupd_plainly_elimE P : ■ P ⊢ |={E}=> P.
    Proof. by rewrite (fupd_intro E (■ P)) fupd_plainly_mask. Qed.

Lemma fupd_plainly_keep_rE E' P R : R ∗ (R ={E,E'}=∗ ■ P) ⊢ |={E}=> R ∗ P.
    Proof. by rewrite !(comm _ R) fupd_plainly_keep_l. Qed.

Lemma fupd_plainly_laterNE n P : (▷^n |={E}=> ■ P) ⊢ |={E}=> ▷^n ◇ P.
    Proof.
      revert P. induction n as [|n IH]=> P /=.
      { by rewrite -except_0_intro (fupd_plainly_elim E) fupd_trans. }
      rewrite -!later_laterN !laterN_later.
      rewrite -plainly_idemp fupd_plainly_later.
      by rewrite except_0_plainly_1 later_plainly_1 IH except_0_later.
    Qed.

Lemma fupd_plain_maskE E' P `{!Plain P} : (|={E,E'}=> P) ⊢ |={E}=> P.
    Proof. by rewrite {1}(plain P) fupd_plainly_mask. Qed.

Lemma fupd_plain_keep_lE E' P R `{!Plain P} : (R ={E,E'}=∗ P) ∗ R ⊢ |={E}=> P ∗ R.
    Proof. rewrite {1}(plain P) fupd_plainly_keep_l //. Qed.

Lemma fupd_plain_keep_rE E' P R `{!Plain P} : R ∗ (R ={E,E'}=∗ P) ⊢ |={E}=> R ∗ P.
    Proof. by rewrite !(comm _ R) fupd_plain_keep_l. Qed.

Lemma fupd_plain_keepE E' P R `{!Plain P} : (R ={E,E'}=∗ P) -∗ R -∗ |={E}=> P ∗ R.
    Proof. apply entails_wand, wand_intro_r, fupd_plain_keep_l. done. Qed.

Lemma fupd_plain_laterE P `{!Plain P} : (▷ |={E}=> P) ⊢ |={E}=> ▷ ◇ P.
    Proof. by rewrite {1}(plain P) fupd_plainly_later. Qed.

Lemma fupd_plain_laterNE n P `{!Plain P} : (▷^n |={E}=> P) ⊢ |={E}=> ▷^n ◇ P.
    Proof. by rewrite {1}(plain P) fupd_plainly_laterN. Qed.

Lemma fupd_plain_forall_2E {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
      (∀ x, |={E}=> Φ x) ⊢ |={E}=> ∀ x, Φ x.
    Proof.
      rewrite -fupd_plainly_forall_2. apply forall_mono=> x.
      by rewrite {1}(plain (Φ _)).
    Qed.

Lemma fupd_plain_forallE1 E2 {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
      E2 ⊆ E1 →
      (|={E1,E2}=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E1,E2}=> Φ x).
    Proof.
      intros. apply (anti_symm _); first apply fupd_forall.
      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_intro_discard E1 E2 (■ _)) //.
      apply fupd_elim. by rewrite fupd_plainly_elim.
    Qed.

Lemma fupd_plain_forall'E {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
      (|={E}=> ∀ x, Φ x) ⊣⊢ (∀ x, |={E}=> Φ x).
    Proof. by apply fupd_plain_forall. Qed.

Lemma step_fupd_plainEo Ei P `{!Plain P} : (|={Eo}[Ei]▷=> P) ⊢ |={Eo}=> ▷ ◇ P.
    Proof.
      rewrite -(fupd_plain_mask _ Ei (▷ ◇ P)).
      apply fupd_elim. by rewrite fupd_plain_mask -fupd_plain_later.
    Qed.

Lemma step_fupdN_plainEo Ei n P `{!Plain P} : (|={Eo}[Ei]▷=>^n P) ⊢ |={Eo}=> ▷^n ◇ P.
    Proof.
      induction n as [|n IH].
      - by rewrite -fupd_intro -except_0_intro.
      - rewrite Nat.iter_succ step_fupd_fupd IH !fupd_trans step_fupd_plain.
        apply fupd_mono. destruct n as [|n]; simpl.
        * by rewrite except_0_idemp.
        * by rewrite except_0_later.
    Qed.

Lemma step_fupd_plain_forallEo Ei {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
      Ei ⊆ Eo →
      (|={Eo}[Ei]▷=> ∀ x, Φ x) ⊣⊢ (∀ x, |={Eo}[Ei]▷=> Φ x).
    Proof.
      intros. apply (anti_symm _).
      { apply forall_intro=> x. by rewrite (forall_elim x). }
      trans (∀ x, |={Eo}=> ▷ ◇ Φ x)%I.
      { apply forall_mono=> x. by rewrite step_fupd_plain. }
      rewrite -fupd_plain_forall'. apply fupd_elim.
      rewrite -(fupd_except_0 Ei Eo) -step_fupd_intro //.
      by rewrite -later_forall -except_0_forall.
    Qed.