Derived rules of the plain modality.

theories/base_logic/derived.v

@@ -39,6 +39,11 @@ Arguments persistentP {_} _ {_}.
 Hint Mode PersistentP + ! : typeclass_instances.
 Instance: Params (@PersistentP) 1.
 
+Class PlainP {M} (P : uPred M) := plainP : P ⊢ ☃ P.
+Arguments plainP {_} _ {_}.
+Hint Mode PlainP + ! : typeclass_instances.
+Instance: Params (@PlainP) 1.
+
 Module uPred.
 Section derived.
 Context {M : ucmraT}.
@@ -471,6 +476,104 @@ Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 Lemma sep_forall_r {A} (Φ : A → uPred M) Q : (∀ a, Φ a) ∗ Q ⊢ ∀ a, Φ a ∗ Q.
 Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
 
+(* Plain modality *)
+Global Instance plainly_mono' : Proper ((⊢) ==> (⊢)) (@uPred_plainly M).
+Proof. intros P Q; apply plainly_mono. Qed.
+Global Instance naugth_flip_mono' :
+  Proper (flip (⊢) ==> flip (⊢)) (@uPred_plainly M).
+Proof. intros P Q; apply plainly_mono. Qed.
+
+Lemma plainly_elim P : ☃ P ⊢ P.
+Proof. by rewrite plainly_elim' always_elim. Qed.
+Hint Resolve plainly_mono plainly_elim.
+Lemma plainly_intro' P Q : (☃ P ⊢ Q) → ☃ P ⊢ ☃ Q.
+Proof. intros <-. apply plainly_idemp. Qed.
+Lemma plainly_idemp P : ☃ ☃ P ⊣⊢ ☃ P.
+Proof. apply (anti_symm _); auto using plainly_idemp. Qed.
+
+Lemma always_plainly P : □ ☃ P ⊣⊢ ☃ P.
+Proof.
+  apply (anti_symm _); auto using always_elim.
+  by rewrite -plainly_elim' plainly_idemp.
+Qed.
+Lemma plainly_always P : ☃ □ P ⊣⊢ ☃ P.
+Proof.
+  apply (anti_symm _); auto using plainly_mono, always_elim.
+  by rewrite -plainly_elim' plainly_idemp.
+Qed.
+
+Lemma plainly_pure φ : ☃ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
+Proof.
+  apply (anti_symm _); auto.
+  apply pure_elim'=> Hφ.
+  trans (∀ x : False, ☃ True : uPred M)%I; [by apply forall_intro|].
+  rewrite plainly_forall_2. auto using plainly_mono, pure_intro.
+Qed.
+Lemma plainly_forall {A} (Ψ : A → uPred M) : (☃ ∀ a, Ψ a) ⊣⊢ (∀ a, ☃ Ψ a).
+Proof.
+  apply (anti_symm _); auto using plainly_forall_2.
+  apply forall_intro=> x. by rewrite (forall_elim x).
+Qed.
+Lemma plainly_exist {A} (Ψ : A → uPred M) : (☃ ∃ a, Ψ a) ⊣⊢ (∃ a, ☃ Ψ a).
+Proof.
+  apply (anti_symm _); auto using plainly_exist_1.
+  apply exist_elim=> x. by rewrite (exist_intro x).
+Qed.
+Lemma plainly_and P Q : ☃ (P ∧ Q) ⊣⊢ ☃ P ∧ ☃ Q.
+Proof. rewrite !and_alt plainly_forall. by apply forall_proper=> -[]. Qed.
+Lemma plainly_or P Q : ☃ (P ∨ Q) ⊣⊢ ☃ P ∨ ☃ Q.
+Proof. rewrite !or_alt plainly_exist. by apply exist_proper=> -[]. Qed.
+Lemma plainly_impl P Q : ☃ (P → Q) ⊢ ☃ P → ☃ Q.
+Proof.
+  apply impl_intro_l; rewrite -plainly_and.
+  apply plainly_mono, impl_elim with P; auto.
+Qed.
+Lemma plainly_internal_eq {A:ofeT} (a b : A) : ☃ (a ≡ b) ⊣⊢ a ≡ b.
+Proof.
+  apply (anti_symm (⊢)); auto using always_elim.
+  apply (internal_eq_rewrite a b (λ b, ☃ (a ≡ b))%I); auto.
+  { intros n; solve_proper. }
+  rewrite -(internal_eq_refl a) plainly_pure; auto.
+Qed.
+
+Lemma plainly_and_sep_l_1 P Q : ☃ P ∧ Q ⊢ ☃ P ∗ Q.
+Proof. by rewrite -always_plainly always_and_sep_l_1. Qed.
+Lemma plainly_and_sep_l' P Q : ☃ P ∧ Q ⊣⊢ ☃ P ∗ Q.
+Proof. apply (anti_symm (⊢)); auto using plainly_and_sep_l_1. Qed.
+Lemma plainly_and_sep_r' P Q : P ∧ ☃ Q ⊣⊢ P ∗ ☃ Q.
+Proof. by rewrite !(comm _ P) plainly_and_sep_l'. Qed.
+Lemma plainly_sep_dup' P : ☃ P ⊣⊢ ☃ P ∗ ☃ P.
+Proof. by rewrite -plainly_and_sep_l' idemp. Qed.
+
+Lemma plainly_and_sep P Q : ☃ (P ∧ Q) ⊣⊢ ☃ (P ∗ Q).
+Proof.
+  apply (anti_symm (⊢)); auto.
+  rewrite -{1}plainly_idemp plainly_and plainly_and_sep_l'; auto.
+Qed.
+Lemma plainly_sep P Q : ☃ (P ∗ Q) ⊣⊢ ☃ P ∗ ☃ Q.
+Proof. by rewrite -plainly_and_sep -plainly_and_sep_l' plainly_and. Qed.
+
+Lemma plainly_wand P Q : ☃ (P -∗ Q) ⊢ ☃ P -∗ ☃ Q.
+Proof. by apply wand_intro_r; rewrite -plainly_sep wand_elim_l. Qed.
+Lemma plainly_wand_impl P Q : ☃ (P -∗ Q) ⊣⊢ ☃ (P → Q).
+Proof.
+  apply (anti_symm (⊢)); [|by rewrite -impl_wand].
+  apply plainly_intro', impl_intro_r.
+  by rewrite plainly_and_sep_l' plainly_elim wand_elim_l.
+Qed.
+Lemma wand_impl_plainly P Q : (☃ P -∗ Q) ⊣⊢ (☃ P → Q).
+Proof.
+  apply (anti_symm (⊢)); [|by rewrite -impl_wand].
+  apply impl_intro_l. by rewrite plainly_and_sep_l' wand_elim_r.
+Qed.
+Lemma plainly_entails_l' P Q : (P ⊢ ☃ Q) → P ⊢ ☃ Q ∗ P.
+Proof. intros; rewrite -plainly_and_sep_l'; auto. Qed.
+Lemma plainly_entails_r' P Q : (P ⊢ ☃ Q) → P ⊢ P ∗ ☃ Q.
+Proof. intros; rewrite -plainly_and_sep_r'; auto. Qed.
+
+Lemma plainly_laterN n P : ☃ ▷^n P ⊣⊢ ▷^n ☃ P.
+Proof. induction n as [|n IH]; simpl; auto. by rewrite plainly_later IH. Qed.
+
 (* Always derived *)
 Hint Resolve always_mono always_elim.
 Global Instance always_mono' : Proper ((⊢) ==> (⊢)) (@uPred_always M).
@@ -485,12 +588,7 @@ Lemma always_idemp P : □ □ P ⊣⊢ □ P.
 Proof. apply (anti_symm _); auto using always_idemp_2. Qed.
 
 Lemma always_pure φ : □ ⌜φ⌝ ⊣⊢ ⌜φ⌝.
-Proof.
-  apply (anti_symm _); auto.
-  apply pure_elim'=> Hφ.
-  trans (∀ x : False, □ True : uPred M)%I; [by apply forall_intro|].
-  rewrite always_forall_2. auto using always_mono, pure_intro.
-Qed.
+Proof. by rewrite -plainly_pure always_plainly. Qed.
 Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
 Proof.
   apply (anti_symm _); auto using always_forall_2.
@@ -511,12 +609,7 @@ Proof.
   apply always_mono, impl_elim with P; auto.
 Qed.
 Lemma always_internal_eq {A:ofeT} (a b : A) : □ (a ≡ b) ⊣⊢ a ≡ b.
-Proof.
-  apply (anti_symm (⊢)); auto using always_elim.
-  apply (internal_eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
-  { intros n; solve_proper. }
-  rewrite -(internal_eq_refl a) always_pure; auto.
-Qed.
+Proof. by rewrite -plainly_internal_eq always_plainly. Qed.
 
 Lemma always_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ∗ Q.
 Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed.
@@ -616,7 +709,6 @@ Proof. apply wand_intro_r; rewrite -later_sep; eauto using wand_elim_l. Qed.
 Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 
-
 (* Iterated later modality *)
 Global Instance laterN_ne m : NonExpansive (@uPred_laterN M m).
 Proof. induction m; simpl. by intros ???. solve_proper. Qed.
@@ -745,6 +837,8 @@ Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /uPred_except_0 -later_or False_or. Qed.
 Lemma except_0_always P : ◇ □ P ⊣⊢ □ ◇ P.
 Proof. by rewrite /uPred_except_0 always_or always_later always_pure. Qed.
+Lemma except_0_plainly P : ◇ ☃ P ⊣⊢ ☃ ◇ P.
+Proof. by rewrite /uPred_except_0 plainly_or plainly_later plainly_pure. Qed.
 Lemma except_0_always_if p P : ◇ □?p P ⊣⊢ □?p ◇ P.
 Proof. destruct p; simpl; auto using except_0_always. Qed.
 Lemma except_0_frame_l P Q : P ∗ ◇ Q ⊢ ◇ (P ∗ Q).
@@ -764,11 +858,10 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
 Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
 Proof. apply (anti_symm _); first by auto. apply ownM_unit. Qed.
+Lemma plainly_cmra_valid {A : cmraT} (a : A) : ☃ ✓ a ⊣⊢ ✓ a.
+Proof. apply (anti_symm _); auto using plainly_elim, plainly_cmra_valid_1. Qed.
 Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
-Proof.
-  intros; apply (anti_symm _); first by apply:always_elim.
-  apply:always_cmra_valid_1.
-Qed.
+Proof. by rewrite -plainly_cmra_valid always_plainly. Qed.
 
 (** * Derived rules *)
 Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M).
@@ -861,6 +954,24 @@ Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A)
   (∀ x, TimelessP (Ψ x)) → TimelessP P → TimelessP (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
+(* Derived lemmas for plainness *)
+Global Instance PlainP_proper : Proper ((≡) ==> iff) (@PlainP M).
+Proof. solve_proper. Qed.
+Global Instance limit_preserving_PlainP {A:ofeT} `{Cofe A} (Φ : A → uPred M) :
+  NonExpansive Φ → LimitPreserving (λ x, PlainP (Φ x)).
+Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
+
+Global Instance Plain_Persistent P : PlainP P → PersistentP P.
+Proof. rewrite /PlainP /PersistentP => HP. by rewrite {1}HP plainly_elim'. Qed.
+
+Lemma plainly_plainly P `{!PlainP P} : ☃ P ⊣⊢ P.
+Proof. apply (anti_symm (⊢)); eauto. Qed.
+Lemma plainly_intro P Q `{!PlainP P} : (P ⊢ Q) → P ⊢ ☃ Q.
+Proof. rewrite -(plainly_plainly P); apply plainly_intro'. Qed.
+
+Lemma bupd_plain P `{!PlainP P} : (|==> P) ⊢ P.
+Proof. by rewrite -{1}(plainly_plainly P) bupd_plainly. Qed.
+
 (* Derived lemmas for persistence *)
 Global Instance PersistentP_proper : Proper ((≡) ==> iff) (@PersistentP M).
 Proof. solve_proper. Qed.
@@ -890,6 +1001,53 @@ Proof.
   apply impl_intro_l. by rewrite always_and_sep_l wand_elim_r.
 Qed.
 
+(* Plain *)
+Global Instance pure_plain φ : PlainP (⌜φ⌝ : uPred M)%I.
+Proof. by rewrite /PlainP plainly_pure. Qed.
+Global Instance pure_impl_plain φ Q : PlainP Q → PlainP (⌜φ⌝ → Q)%I.
+Proof.
+  rewrite /PlainP pure_impl_forall plainly_forall. auto using forall_mono.
+Qed.
+Global Instance pure_wand_plain φ Q : PlainP Q → PlainP (⌜φ⌝ -∗ Q)%I.
+Proof.
+  rewrite /PlainP -always_impl_wand pure_impl_forall plainly_forall.
+  auto using forall_mono.
+Qed.
+Global Instance plainly_plain P : PlainP (☃ P).
+Proof. by intros; apply plainly_intro'. Qed.
+Global Instance always_plain P : PlainP P → PlainP (□ P).
+Proof. rewrite /PlainP=> HP. by rewrite {1}HP always_plainly plainly_always. Qed.
+Global Instance and_plain P Q :
+  PlainP P → PlainP Q → PlainP (P ∧ Q).
+Proof. by intros; rewrite /PlainP plainly_and; apply and_mono. Qed.
+Global Instance or_plain P Q :
+  PlainP P → PlainP Q → PlainP (P ∨ Q).
+Proof. by intros; rewrite /PlainP plainly_or; apply or_mono. Qed.
+Global Instance sep_plain P Q :
+  PlainP P → PlainP Q → PlainP (P ∗ Q).
+Proof. by intros; rewrite /PlainP plainly_sep; apply sep_mono. Qed.
+Global Instance forall_plain {A} (Ψ : A → uPred M) :
+  (∀ x, PlainP (Ψ x)) → PlainP (∀ x, Ψ x).
+Proof. by intros; rewrite /PlainP plainly_forall; apply forall_mono. Qed.
+Global Instance exist_palin {A} (Ψ : A → uPred M) :
+  (∀ x, PlainP (Ψ x)) → PlainP (∃ x, Ψ x).
+Proof. by intros; rewrite /PlainP plainly_exist; apply exist_mono. Qed.
+Global Instance internal_eq_plain {A : ofeT} (a b : A) :
+  PlainP (a ≡ b : uPred M)%I.
+Proof. by intros; rewrite /PlainP plainly_internal_eq. Qed.
+Global Instance cmra_valid_plain {A : cmraT} (a : A) :
+  PlainP (✓ a : uPred M)%I.
+Proof. by intros; rewrite /PlainP; apply plainly_cmra_valid_1. Qed.
+Global Instance later_plain P : PlainP P → PlainP (▷ P).
+Proof. by intros; rewrite /PlainP plainly_later; apply later_mono. Qed.
+Global Instance except_0_plain P : PlainP P → PlainP (◇ P).
+Proof. by intros; rewrite /PlainP -except_0_plainly; apply except_0_mono. Qed.
+Global Instance laterN_plain n P : PlainP P → PlainP (▷^n P).
+Proof. induction n; apply _. Qed.
+Global Instance from_option_palin {A} P (Ψ : A → uPred M) (mx : option A) :
+  (∀ x, PlainP (Ψ x)) → PlainP P → PlainP (from_option Ψ P mx).
+Proof. destruct mx; apply _. Qed.
+
 (* Persistence *)
 Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I.
 Proof. by rewrite /PersistentP always_pure. Qed.
@@ -929,6 +1087,8 @@ Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
 Proof. by intros; rewrite /PersistentP always_cmra_valid. Qed.
 Global Instance later_persistent P : PersistentP P → PersistentP (▷ P).
 Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
+Global Instance except_0_persistent P : PersistentP P → PersistentP (◇ P).
+Proof. by intros; rewrite /PersistentP -except_0_always; apply except_0_mono. Qed.
 Global Instance laterN_persistent n P : PersistentP P → PersistentP (▷^n P).
 Proof. induction n; apply _. Qed.
 Global Instance ownM_persistent : Persistent a → PersistentP (@uPred_ownM M a).
@@ -948,6 +1108,9 @@ Global Instance uPred_sep_monoid : Monoid (@uPred_sep M) :=
 Global Instance uPred_always_and_homomorphism :
   MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always M).
 Proof. split; [split; try apply _|]. apply always_and. apply always_pure. Qed.
+Global Instance uPred_plainly_and_homomorphism :
+  MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_plainly M).
+Proof. split; [split; try apply _|]. apply plainly_and. apply plainly_pure. Qed.
 Global Instance uPred_always_if_and_homomorphism b :
   MonoidHomomorphism uPred_and uPred_and (≡) (@uPred_always_if M b).
 Proof. split; [split; try apply _|]. apply always_if_and. apply always_if_pure. Qed.
@@ -964,6 +1127,9 @@ Proof. split; [split; try apply _|]. apply except_0_and. apply except_0_True. Qe
 Global Instance uPred_always_or_homomorphism :
   MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always M).
 Proof. split; [split; try apply _|]. apply always_or. apply always_pure. Qed.
+Global Instance uPred_plainly_or_homomorphism :
+  MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_plainly M).
+Proof. split; [split; try apply _|]. apply plainly_or. apply plainly_pure. Qed.
 Global Instance uPred_always_if_or_homomorphism b :
   MonoidHomomorphism uPred_or uPred_or (≡) (@uPred_always_if M b).
 Proof. split; [split; try apply _|]. apply always_if_or. apply always_if_pure. Qed.
@@ -975,11 +1141,14 @@ Global Instance uPred_laterN_or_homomorphism n :
 Proof. split; try apply _. apply laterN_or. Qed.
 Global Instance uPred_except_0_or_homomorphism :
   WeakMonoidHomomorphism uPred_or uPred_or (≡) (@uPred_except_0 M).
-Proof. split; try apply _. apply except_0_or. Qed. 
+Proof. split; try apply _. apply except_0_or. Qed.
 
 Global Instance uPred_always_sep_homomorphism :
   MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always M).
 Proof. split; [split; try apply _|]. apply always_sep. apply always_pure. Qed.
+Global Instance uPred_plainly_sep_homomorphism :
+  MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_plainly M).
+Proof. split; [split; try apply _|]. apply plainly_sep. apply plainly_pure. Qed.
 Global Instance uPred_always_if_sep_homomorphism b :
   MonoidHomomorphism uPred_sep uPred_sep (≡) (@uPred_always_if M b).
 Proof. split; [split; try apply _|]. apply always_if_sep. apply always_if_pure. Qed.

theories/base_logic/lib/fancy_updates.v

@@ -140,6 +140,45 @@ 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 E2'} P Q `{!PlainP P} :
+  E1 ⊆ E2 →
+  (Q ={E1, E2'}=∗ P) → (|={E1, E2}=> Q) ⊢ |={E1}=> ((|={E1, E2}=> Q) ∗ P).
+Proof.
+  iIntros (HE HQP) "HQ".
+  iPoseProof (HQP) as "HQP".
+  apply subseteq_disjoint_union_L in HE; destruct HE as [E3 [? HE]]; subst.
+  rewrite fupd_eq /fupd_def.
+  iIntros "H". iMod ("HQ" with "H") as "H".
+  iMod "H" as "(Hws & HE2 & HQ)".
+  rewrite ownE_op; trivial; iDestruct "HE2" as "[HE1 HE3]".
+  iAssert (◇ P)%I with "[HQ Hws HE1]" as "#HP".
+  { iApply bupd_plain; eauto.
+    by iMod ("HQP" with "HQ [$]") as "[_ [_ HP]]". }
+  iModIntro. iMod "HP".
+  iModIntro; iFrame; auto.
+Qed.
+
+Lemma fupd_plain {E1 E2} P Q `{!PlainP P} :
+  E1 ⊆ E2 → (Q ⊢ P) → (|={E1, E2}=> Q) ⊢ |={E1}=> ((|={E1, E2}=> Q) ∗ P).
+Proof.
+  iIntros (HE HQP) "HQ".
+  iApply (fupd_plain' with "HQ"); auto.
+  by iIntros "?"; iApply fupd_intro; iApply HQP.
+Qed.
+
+Lemma later_fupd_plain {E} P `{Hpl: !PlainP P} :
+  (▷ |={E}=> P) ⊢ |={E}=> ▷ ◇ P.
+Proof.
+  iIntros "HP". rewrite fupd_eq /fupd_def.
+  iIntros "[Hs He]".
+  iAssert (▷ ◇ P)%I with "[-]" as "#HP'".
+  { iNext. iApply bupd_plain; eauto.
+    iMod ("HP" with "[$]") as "HP".
+    iModIntro. iMod "HP" as "(_&_&HP)". by iModIntro. }
+  by iFrame.
+Qed.
+
 End fupd.
 
 (** Proofmode class instances *)