From 31a0912cfea582d6bb7af4f564734b71a3de9cd7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 6 May 2019 16:33:57 +0200
Subject: [PATCH] Some additional results about `<affine>?p`.

---
 theories/bi/derived_laws_bi.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index e6aeeaf16..215778047 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -1144,6 +1144,13 @@ Proof. destruct p; simpl; auto using affinely_sep. Qed.
 Lemma affinely_if_idemp p P : <affine>?p <affine>?p P ⊣⊢ <affine>?p P.
 Proof. destruct p; simpl; auto using affinely_idemp. Qed.
 
+Lemma affinely_if_and_l p P Q : <affine>?p P ∧ Q ⊣⊢ <affine>?p (P ∧ Q).
+Proof. destruct p; simpl; auto using affinely_and_l. Qed.
+Lemma affinely_if_and_r p P Q : P ∧ <affine>?p Q ⊣⊢ <affine>?p (P ∧ Q).
+Proof. destruct p; simpl; auto using affinely_and_r. Qed.
+Lemma affinely_if_and_lr p P Q : <affine>?p P ∧ Q ⊣⊢ P ∧ <affine>?p Q.
+Proof. destruct p; simpl; auto using affinely_and_lr. Qed.
+
 (* Conditional absorbingly modality *)
 Global Instance absorbingly_if_ne p : NonExpansive (@bi_absorbingly_if PROP p).
 Proof. solve_proper. Qed.
@@ -1468,10 +1475,14 @@ Global Instance persistently_persistent P : Persistent (<pers> P).
 Proof. by rewrite /Persistent persistently_idemp. Qed.
 Global Instance affinely_persistent P : Persistent P → Persistent (<affine> P).
 Proof. rewrite /bi_affinely. apply _. Qed.
+Global Instance affinely_if_persistent p P : Persistent P → Persistent (<affine>?p P).
+Proof. destruct p; simpl; apply _. Qed.
 Global Instance intuitionistically_persistent P : Persistent (â–¡ P).
 Proof. rewrite /bi_intuitionistically. apply _. Qed.
 Global Instance absorbingly_persistent P : Persistent P → Persistent (<absorb> P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
+Global Instance absorbingly_if_persistent p P : Persistent P → Persistent (<absorb>?p P).
+Proof. destruct p; simpl; apply _. Qed.
 Global Instance from_option_persistent {A} P (Ψ : A → PROP) (mx : option A) :
   (∀ x, Persistent (Ψ x)) → Persistent P → Persistent (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
-- 
GitLab