diff --git a/theories/bi/notation.v b/theories/bi/notation.v index d522114bde58578c7a603f55f7b5d02fa86fe3e1..1a96d9e523c7d50fa21c89b9e6f03631f7aa99cd 100644 --- a/theories/bi/notation.v +++ b/theories/bi/notation.v @@ -47,6 +47,8 @@ Reserved Notation "■ P" (at level 20, right associativity). Reserved Notation "■? p P" (at level 20, p at level 9, P at level 20, right associativity, format "■? p P"). +Reserved Notation "'' P" (at level 20, right associativity). + Reserved Notation "'' P" (at level 20, right associativity). Reserved Notation "'' P" (at level 20, right associativity). diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v index ac919a18f08a36178f1b7db20761c2b497c82498..9507319c6501c36df509651328d2ab2576e180cb 100644 --- a/theories/bi/plainly.v +++ b/theories/bi/plainly.v @@ -97,6 +97,14 @@ Typeclasses Opaque plainly_if. Notation "■? p P" := (plainly_if p P) : bi_scope. +Definition plausibly `{!BiPlainly PROP} (P : PROP) : PROP := + (∀ Q, ■ (P -∗ ■ Q) -∗ ■ Q)%I. +Arguments plausibly {_ _} _%I. +Instance: Params (@plausibly) 2. +Typeclasses Opaque plausibly. + +Notation " P" := (plausibly P) : bi_scope. + (* Derived laws *) Section plainly_derived. Context `{BiPlainly PROP}. @@ -527,6 +535,57 @@ Proof. intros. rewrite /Timeless /sbi_except_0 later_plainly_1. by rewrite (timeless P) /sbi_except_0 plainly_or {1}plainly_elim. Qed. + +(* The plausible modality *) +Global Instance plausibly_ne : NonExpansive (@plausibly PROP _). +Proof. solve_proper. Qed. +Global Instance plausibly_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@plausibly PROP _). +Proof. solve_proper. Qed. +Global Instance plausibly_mono' : Proper ((⊢) ==> (⊢)) (@plausibly PROP _). +Proof. solve_proper. Qed. +Global Instance plausibly_flip_mono' : + Proper (flip (⊢) ==> flip (⊢)) (@plausibly PROP _). +Proof. solve_proper. Qed. + +Global Instance plausibly_absorbing P : Absorbing ( P). +Proof. rewrite /plausibly. apply _. Qed. +Global Instance plausibly_plain P : Plain ( P). +Proof. rewrite /plausibly. apply _. Qed. +Global Instance plausibly_persistent P : Persistent ( P). +Proof. apply plain_persistent, _. Qed. + +Lemma plausibly_intro P : P ⊢ P. +Proof. + rewrite /plausibly. apply forall_intro=> Q. apply wand_intro_l. + by rewrite plainly_elim wand_elim_l. +Qed. + +Lemma plain_plausibly P `{!Plain P, !Absorbing P} : P ⊣⊢ P. +Proof. + apply (anti_symm _); last by apply plausibly_intro. + rewrite /plausibly (forall_elim P). + rewrite -(entails_wand' P (■ P)%I) // -plainly_emp_2 emp_wand. + by apply plainly_elim. +Qed. + +Lemma plausibly_trans P : P ⊣⊢ P. +Proof. apply (plain_plausibly _). Qed. + +Lemma plausibly_wand P Q : ■ (P -∗ Q) ⊢ P -∗ Q. +Proof. + rewrite /plausibly. apply wand_intro_l, forall_intro=> R. + rewrite (forall_elim R). apply wand_intro_r. rewrite -assoc plainly_sep_2. + by rewrite wand_trans wand_elim_l. +Qed. + +Definition plausibly_forall_plainly {A} (Φ : A → PROP) : + (∀ x, ■ Φ x) ⊣⊢ (∀ x, ■ Φ x). +Proof. + rewrite plain_plausibly. apply forall_proper=> x. by rewrite plain_plausibly. +Qed. + +Definition plausibly_later_plainly P : ▷ ■ P ⊣⊢ ▷ ■ P. +Proof. by rewrite !plain_plausibly. Qed. End plainly_derived. (* When declared as an actual instance, [plain_persistent] will cause