From cce5a9ee86d8d5c8fb9ca794f380571c16678bdc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 May 2023 18:25:57 +0200
Subject: [PATCH] Generalize `persistent_entails_{l,r}`.

---
 iris/base_logic/lib/own.v |  2 +-
 iris/bi/derived_laws.v    | 14 +++++++-------
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/iris/base_logic/lib/own.v b/iris/base_logic/lib/own.v
index 593835c21..520afde78 100644
--- a/iris/base_logic/lib/own.v
+++ b/iris/base_logic/lib/own.v
@@ -185,7 +185,7 @@ Proof. apply entails_wand, wand_intro_r. by rewrite -own_op own_valid. Qed.
 Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
 Proof. apply entails_wand. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
 Lemma own_valid_r γ a : own γ a ⊢ own γ a ∗ ✓ a.
-Proof. apply: bi.persistent_entails_r. apply own_valid. Qed.
+Proof. apply: bi.entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a.
 Proof. by rewrite comm -own_valid_r. Qed.
 
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index bddb71c55..f175de300 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -915,6 +915,11 @@ Proof.
   by rewrite affinely_elim wand_elim_r.
 Qed.
 
+Lemma entails_l P Q `{!Separable Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
+Proof. intros. rewrite -and_sep_1; auto. Qed.
+Lemma entails_r P Q `{!Separable Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
+Proof. intros. rewrite -and_sep_1; auto. Qed.
+
 Section separable_affine_bi.
   Context `{!BiAffine PROP}.
 
@@ -1229,9 +1234,9 @@ Lemma persistently_wand P Q : <pers> (P -∗ Q) ⊢ <pers> P -∗ <pers> Q.
 Proof. apply wand_intro_r. by rewrite persistently_sep_2 wand_elim_l. Qed.
 
 Lemma persistently_entails_l P Q : (P ⊢ <pers> Q) → P ⊢ <pers> Q ∗ P.
-Proof. intros; rewrite -and_sep_l_1; auto. Qed.
+Proof. apply: entails_l. Qed.
 Lemma persistently_entails_r P Q : (P ⊢ <pers> Q) → P ⊢ P ∗ <pers> Q.
-Proof. intros; rewrite -and_sep_r_1; auto. Qed.
+Proof. apply: entails_r. Qed.
 
 Lemma persistently_impl_wand_2 P Q : <pers> (P -∗ Q) ⊢ <pers> (P → Q).
 Proof.
@@ -1668,11 +1673,6 @@ Qed.
 Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ <pers> Q.
 Proof. intros HP. by rewrite (persistent P) HP. Qed.
 
-Lemma persistent_entails_l P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ Q ∗ P.
-Proof. intros. rewrite -and_sep_1; auto. Qed.
-Lemma persistent_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
-Proof. intros. rewrite -and_sep_1; auto. Qed.
-
 Lemma absorbingly_intuitionistically_into_persistently P :
   <absorb> □ P ⊣⊢ <pers> P.
 Proof. apply: absorbingly_affinely. Qed.
-- 
GitLab