From 3e4b87c2c9dd67ae774cbe8170a7d0e98556f3d7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 27 Oct 2018 17:54:25 +0200
Subject: [PATCH] Show that bupd entails plausibly.
---
theories/bi/updates.v | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 480faeda6..574b84b39 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -172,6 +172,12 @@ Section bupd_derived_sbi.
- rewrite -bupd_intro. apply forall_intro=> x.
by rewrite (forall_elim x) bupd_plain.
Qed.
+
+ Lemma bupd_plausibly P : (|==> P) ⊢ <plausible> P.
+ Proof.
+ apply forall_intro=> Q. apply wand_intro_l. rewrite bupd_frame_l.
+ by rewrite plainly_elim wand_elim_l bupd_plain.
+ Qed.
End bupd_plainly.
End bupd_derived_sbi.
--
GitLab