From 625d60c3daba70e065c6393a38b4f5d5b14295a9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 27 Oct 2018 14:40:49 +0200
Subject: [PATCH] Some useful BI derived lemmas.

---
 theories/bi/derived_laws_bi.v | 6 ++++++
 theories/bi/plainly.v         | 3 +++
 2 files changed, 9 insertions(+)

diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 8b7b27536..f9deee67e 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -385,6 +385,9 @@ Proof.
   apply wand_intro_l. rewrite left_absorb. auto.
 Qed.
 
+Lemma wand_trans P Q R : (P -∗ Q) ∗ (Q -∗ R) ⊢ (P -∗ R).
+Proof. apply wand_intro_l. by rewrite assoc !wand_elim_r. Qed.
+
 Lemma wand_curry P Q R : (P -∗ Q -∗ R) ⊣⊢ (P ∗ Q -∗ R).
 Proof.
   apply (anti_symm _).
@@ -429,6 +432,9 @@ Lemma wand_entails P Q : (P -∗ Q)%I → P ⊢ Q.
 Proof. intros. rewrite -[P]emp_sep. by apply wand_elim_l'. Qed.
 Lemma entails_wand P Q : (P ⊢ Q) → (P -∗ Q)%I.
 Proof. intros ->. apply wand_intro_r. by rewrite left_id. Qed.
+(* A version that works with rewrite, in which bi_emp_valid is unfolded. *)
+Lemma entails_wand' P Q : (P ⊢ Q) → emp ⊢ (P -∗ Q).
+Proof. apply entails_wand. Qed.
 
 Lemma equiv_wand_iff P Q : (P ⊣⊢ Q) → (P ∗-∗ Q)%I.
 Proof. intros ->; apply wand_iff_refl. Qed.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index abff5e642..ac919a18f 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -188,6 +188,9 @@ Proof.
   apply plainly_mono, impl_elim with P; auto.
 Qed.
 
+Lemma plainly_emp_2 : emp ⊢@{PROP} ■ emp.
+Proof. apply plainly_emp_intro. Qed.
+
 Lemma plainly_sep_dup P : ■ P ⊣⊢ ■ P ∗ ■ P.
 Proof.
   apply (anti_symm _).
-- 
GitLab