fix iPureIntro when the goal is an absorbing modality

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.

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.