From d840f8cb3a076f05a3eb07b3fbafdcd27886eb50 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 29 Mar 2019 15:32:41 +0100
Subject: [PATCH] add derived soundness_bupd matching soundness_later

---
 theories/base_logic/bi.v      | 2 ++
 theories/base_logic/derived.v | 6 ++++++
 2 files changed, 8 insertions(+)

diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index b6d065037..5a6ef337e 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -213,6 +213,8 @@ Lemma soundness_later P : bi_emp_valid (▷ P) → bi_emp_valid P.
 Proof. apply soundness_later. Qed.
 End restate.
 
+(** See [derived.v] for the version for basic updates. *)
+
 (** New unseal tactic that also unfolds the BI layer.
     This is used by [base_logic.double_negation].
     TODO: Can we get rid of this? *)
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index e5b4462bd..721431164 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -92,6 +92,12 @@ Global Instance uPred_ownM_sep_homomorphism :
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 
 (** Consistency/soundness statement *)
+Lemma soundness_bupd_plain P `{!Plain P} : bi_emp_valid (|==> P) → bi_emp_valid P.
+Proof.
+  eapply bi_emp_valid_mono. etrans; last exact: bupd_plainly. apply bupd_mono'.
+  apply: plain.
+Qed.
+
 Corollary soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
 Proof.
   induction n as [|n IH]=> /=.
-- 
GitLab