diff --git a/iris/bi/updates.v b/iris/bi/updates.v index a26a1835272c7f060faf08242a689bf04ae47dc9..99b613eaab1709a7034508a906c7924c31fe7813 100644 --- a/iris/bi/updates.v +++ b/iris/bi/updates.v @@ -240,6 +240,10 @@ Section bupd_derived. by rewrite -bupd_intro -or_intro_l. Qed. + Global Instance bupd_absorbing P : + Absorbing P → Absorbing (|==> P). + Proof. rewrite /Absorbing /bi_absorbingly bupd_frame_l =>-> //. Qed. + Section bupd_plainly. Context `{!BiPlainly PROP, !BiBUpdPlainly PROP}. @@ -326,6 +330,10 @@ Section fupd_derived. Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ∗ (P -∗ Q) ={E1,E2}=∗ Q. Proof. by rewrite fupd_frame_r wand_elim_r. Qed. + Global Instance fupd_absorbing E1 E2 P : + Absorbing P → Absorbing (|={E1,E2}=> P). + Proof. rewrite /Absorbing /bi_absorbingly fupd_frame_l =>-> //. Qed. + Lemma fupd_trans_frame E1 E2 E3 P Q : ((Q ={E2,E3}=∗ emp) ∗ |={E1,E2}=> (Q ∗ P)) ={E1,E3}=∗ P. Proof.