Rules for fancy updates and plain propositions.

This commit is based on code by Amin Timany.

theories/base_logic/lib/fancy_updates.v

@@ -81,6 +81,25 @@ Qed.
 Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ∗ Q ={E1,E2}=∗ P ∗ Q.
 Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.
 
+Lemma fupd_plain' E1 E2 E2' P Q `{!Plain P} :
+  E1 ⊆ E2 →
+  (Q ={E1, E2'}=∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
+Proof.
+  iIntros ((E3&->&HE)%subseteq_disjoint_union_L) "HQP HQ".
+  rewrite fupd_eq /fupd_def ownE_op //. iIntros "H".
+  iMod ("HQ" with "H") as ">(Hws & [HE1 HE3] & HQ)"; iModIntro.
+  iAssert (◇ P)%I as "#HP".
+  { by iMod ("HQP" with "HQ [$]") as "(_ & _ & HP)". }
+  iMod "HP". iFrame. auto.
+Qed.
+
+Lemma later_fupd_plain E P `{!Plain P} : (▷ |={E}=> P) ={E}=∗ ▷ ◇ P.
+Proof.
+  rewrite fupd_eq /fupd_def. iIntros "HP [Hw HE]".
+  iAssert (▷ ◇ P)%I with "[-]" as "#$"; last by iFrame.
+  iNext. by iMod ("HP" with "[$]") as "(_ & _ & HP)".
+Qed.
+
 (** * Derived rules *)
 Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@fupd Σ _ E1 E2).
 Proof. intros P Q; apply fupd_mono. Qed.
@@ -140,6 +159,13 @@ 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.
+
+Lemma fupd_plain E1 E2 P Q `{!Plain P} :
+  E1 ⊆ E2 → (Q -∗ P) -∗ (|={E1, E2}=> Q) ={E1}=∗ (|={E1, E2}=> Q) ∗ P.
+Proof.
+  iIntros (HE) "HQP HQ". iApply (fupd_plain' _ _ E1 with "[HQP] HQ"); first done.
+  iIntros "?". iApply fupd_intro. by iApply "HQP".
+Qed.
 End fupd.
 
 (** Proofmode class instances *)