From 35769f677eb91cae46dc292f51a34d48005494f7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 3 Dec 2017 21:45:37 +0100
Subject: [PATCH] =?UTF-8?q?Instance=20for=20`Absorbing=20(P=20=E2=86=92=20?=
 =?UTF-8?q?Q)`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Note sure whether these premises are the weakest possible.
---
 theories/bi/derived.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index e19e4d577..0b1a61b92 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -1689,6 +1689,13 @@ Global Instance exist_absorbing {A} (Φ : A → PROP) :
   (∀ x, Absorbing (Φ x)) → Absorbing (∃ x, Φ x).
 Proof. rewrite /Absorbing=> ?. rewrite absorbingly_exist. auto using exist_mono. Qed.
 
+Global Instance impl_absorbing P Q :
+  Persistent P → Absorbing P → Absorbing Q → Absorbing (P → Q).
+Proof.
+  intros. rewrite /Absorbing. apply impl_intro_l.
+  rewrite persistent_and_affinely_sep_l_1 absorbingly_sep_r.
+  by rewrite -persistent_and_affinely_sep_l impl_elim_r.
+Qed.
 Global Instance internal_eq_absorbing {A : ofeT} (x y : A) :
   Absorbing (x ≡ y : PROP)%I.
 Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
-- 
GitLab