Commit 5b084890 authored by Robbert Krebbers's avatar Robbert Krebbers

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.
parent 1f796221
......@@ -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 "'<plausible>' P" (at level 20, right associativity).
Reserved Notation "'<obj>' P" (at level 20, right associativity).
Reserved Notation "'<subj>' P" (at level 20, right associativity).
......
......@@ -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 "<plausible> 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 (<plausible> P).
Proof. rewrite /plausibly. apply _. Qed.
Global Instance plausibly_plain P : Plain (<plausible> P).
Proof. rewrite /plausibly. apply _. Qed.
Global Instance plausibly_persistent P : Persistent (<plausible> P).
Proof. apply plain_persistent, _. Qed.
Lemma plausibly_intro P : P <plausible> 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} : <plausible> 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 : <plausible> <plausible> P <plausible> P.
Proof. apply (plain_plausibly _). Qed.
Lemma plausibly_wand P Q : (P - Q) <plausible> P - <plausible> 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) :
<plausible> ( x, Φ x) ( x, <plausible> Φ x).
Proof.
rewrite plain_plausibly. apply forall_proper=> x. by rewrite plain_plausibly.
Qed.
Definition plausibly_later_plainly P : <plausible> P <plausible> P.
Proof. by rewrite !plain_plausibly. Qed.
End plainly_derived.
(* When declared as an actual instance, [plain_persistent] will cause
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment