From 5bdf0c213a7840e917db3a4f3a31494d34b41160 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 May 2018 11:59:07 +0200
Subject: [PATCH] =?UTF-8?q?Better=20`IntoWand`=20instances=20for=20`<affin?=
 =?UTF-8?q?e>=20=E2=8E=A1=20...=20=E2=8E=A4`=20as=20an=20alternative=20for?=
 =?UTF-8?q?=20ec4ac846.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/proofmode/class_instances_bi.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 45e72fee4..8e7d610ff 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -427,10 +427,34 @@ Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
 Global Instance into_wand_persistently_false q R P Q :
   Absorbing R → IntoWand false q R P Q → IntoWand false q (<pers> R) P Q.
 Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.
+
 Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q R P Q :
   IntoWand p q R P Q → IntoWand p q ⎡R⎤ ⎡P⎤ ⎡Q⎤.
 Proof. by rewrite /IntoWand !embed_intuitionistically_if_2 -embed_wand=> ->. Qed.
 
+(* There are two versions for [IntoWand ⎡RR⎤ ...] with the argument being
+[<affine> ⎡PP⎤]. When the wand [⎡RR⎤] resides in the intuitionistic context
+the result of wand elimination will have the affine modality. Otherwise, it
+won't. Note that when the wand [⎡RR⎤] is under an affine modality, the instance
+[into_wand_affine] would already have been used. *)
+Global Instance into_wand_affine_embed_true `{BiEmbed PROP PROP'} q (PP QQ RR : PROP) :
+  IntoWand true q RR PP QQ → IntoWand true q ⎡RR⎤ (<affine> ⎡PP⎤) (<affine> ⎡QQ⎤) | 100.
+Proof.
+  rewrite /IntoWand /=.
+  rewrite -(intuitionistically_idemp ⎡ _ ⎤%I) embed_intuitionistically_2=> ->.
+  apply bi.wand_intro_l. destruct q; simpl.
+  - rewrite affinely_elim  -(intuitionistically_idemp ⎡ _ ⎤%I).
+    rewrite embed_intuitionistically_2 intuitionistically_sep_2 -embed_sep.
+    by rewrite wand_elim_r intuitionistically_affinely.
+  - by rewrite intuitionistically_affinely affinely_sep_2 -embed_sep wand_elim_r.
+Qed.
+Global Instance into_wand_affine_embed_false `{BiEmbed PROP PROP'} q (PP QQ RR : PROP) :
+  IntoWand false q RR (<affine> PP) QQ → IntoWand false q ⎡RR⎤ (<affine> ⎡PP⎤) ⎡QQ⎤ | 100.
+Proof.
+  rewrite /IntoWand /= => ->.
+  by rewrite embed_affinely_2 embed_intuitionistically_if_2 embed_wand.
+Qed.
+
 (* FromWand *)
 Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
 Proof. by rewrite /FromWand. Qed.
-- 
GitLab