From 5b084890f4ae430db912b6e5c565facde11fbddd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Sat, 27 Oct 2018 14:41:13 +0200
Subject: [PATCH] The plausibly modality.
Much of this is based on https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/184#note_31510
by Amin Timany, but made to work for non-affine BIs and changed in
a way that it follows the Iris naming conventions.
---
theories/bi/notation.v | 2 ++
theories/bi/plainly.v | 59 ++++++++++++++++++++++++++++++++++++++++++
2 files changed, 61 insertions(+)
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index d522114b..1a96d9e5 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 ac919a18..9507319c 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
--
GitLab