Another absorbing instance for wand.

43ee9e86 · Robbert Krebbers · 1c42ec5d · 43ee9e86
Commit 43ee9e86 authored Dec 06, 2017 by Robbert Krebbers
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1623,9 +1623,15 @@ Proof. intros. by rewrite /Absorbing -absorbingly_sep_l absorbing. Qed.
 Global Instance sep_absorbing_r P Q : Absorbing Q → Absorbing (P ∗ Q).
 Proof. intros. by rewrite /Absorbing -absorbingly_sep_r absorbing. Qed.

-Global Instance wand_absorbing P Q : Absorbing Q → Absorbing (P -∗ Q).
+Global Instance wand_absorbing_l P Q : Absorbing P → Absorbing (P -∗ Q).
+Proof.
+  intros. rewrite /Absorbing /bi_absorbingly. apply wand_intro_l.
+  by rewrite assoc (sep_elim_l P) wand_elim_r.
+Qed.
+Global Instance wand_absorbing_r P Q : Absorbing Q → Absorbing (P -∗ Q).
 Proof. intros. by rewrite /Absorbing absorbingly_wand !absorbing -absorbingly_intro. Qed.

+
 Global Instance absorbingly_absorbing P : Absorbing (bi_absorbingly P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
 Global Instance plainly_absorbing P : Absorbing (bi_plainly P).