From c2b96095eeb595276ec7a5a140a3e1f6b3fe3125 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 9 May 2018 13:53:28 +0200
Subject: [PATCH] fix iPureIntro when the goal is an absorbing modality

---
 theories/proofmode/class_instances_bi.v | 9 ++++++---
 theories/tests/proofmode.v              | 4 ++++
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 1e6b32313..ff23506f5 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -215,9 +215,12 @@ Proof.
   rewrite {1}(persistent ⌜φ⌝%I) //.
 Qed.
 
-Global Instance from_pure_absorbingly P φ :
-  FromPure true P φ → FromPure false (<absorb> P) φ.
-Proof. rewrite /FromPure=> <- /=. by rewrite persistent_absorbingly_affinely. Qed.
+Global Instance from_pure_absorbingly P φ p :
+  FromPure true P φ → FromPure p (<absorb> P) φ.
+Proof.
+  rewrite /FromPure=> <- /=.
+  rewrite persistent_absorbingly_affinely affinely_if_elim //.
+Qed.
 Global Instance from_pure_embed `{BiEmbed PROP PROP'} a P φ :
   FromPure a P φ → FromPure a ⎡P⎤ φ.
 Proof. rewrite /FromPure=> <-. by rewrite -embed_pure embed_affinely_if_2. Qed.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 19c61a492..bd5c516be 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -389,6 +389,10 @@ Qed.
 Lemma test_iIntros_pure_neg : (⌜ ¬False ⌝ : PROP)%I.
 Proof. by iIntros (?). Qed.
 
+Lemma test_iPureIntro_absorbing (φ : Prop) :
+  φ → sbi_emp_valid (PROP:=PROP) (<absorb> ⌜φ⌝)%I.
+Proof. intros ?. iPureIntro. done. Qed.
+
 Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
 Proof. iIntros "H". iFrame "H". auto. Qed.
 
-- 
GitLab