From 8e14fcf891048d1457e53bf4835f2e97d234da08 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 13 Aug 2022 16:58:52 -0400
Subject: [PATCH] avoid MakeIntuitionistically turning a True into emp for
 affine BI

---
 iris/proofmode/class_instances_make.v | 11 ++++++++++-
 tests/proofmode.ref                   | 15 +++++++++++++--
 tests/proofmode.v                     |  9 ++++++++-
 3 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/iris/proofmode/class_instances_make.v b/iris/proofmode/class_instances_make.v
index 336873be2..df86ed206 100644
--- a/iris/proofmode/class_instances_make.v
+++ b/iris/proofmode/class_instances_make.v
@@ -138,8 +138,17 @@ Proof.
   by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
     intuitionistically_emp.
 Qed.
+(** For affine BIs, we would prefer [â–¡ True] to become [True] rather than [emp],
+so we have this instance with lower cost than the next. *)
+Global Instance make_intuitionistically_True_affine :
+  BiAffine PROP →
+  @KnownMakeIntuitionistically PROP True True | 0.
+Proof.
+  intros. rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
+    intuitionistically_True_emp True_emp //.
+Qed.
 Global Instance make_intuitionistically_True :
-  @KnownMakeIntuitionistically PROP True emp | 0.
+  @KnownMakeIntuitionistically PROP True emp | 1.
 Proof.
   by rewrite /KnownMakeIntuitionistically /MakeIntuitionistically
     intuitionistically_True_emp.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 749eb5b97..57992ccc9 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -503,9 +503,9 @@ No applicable tactic.
 1 goal
   
   PROP : bi
-  H : BiAffine PROP
+  BiAffine0 : BiAffine PROP
   P, Q : PROP
-  H0 : Laterable Q
+  H : Laterable Q
   ============================
   "HP" : â–· P
   "HQ" : Q
@@ -534,6 +534,17 @@ No applicable tactic.
   "H" : ⌜φ⌝ -∗ P
   --------------------------------------∗
   ⌜φ⌝ -∗ P
+"test_iFrame_not_add_emp_for_intuitionistically"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  P : PROP
+  ============================
+  "H" : P
+  --------------------------------------â–¡
+  ∃ _ : nat, True
 "elim_mod_accessor"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 3fe9aed5f..2d08f83fe 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1261,7 +1261,7 @@ Proof.
   iIntros "[P _]". done.
 Qed.
 
-Lemma test_iModIntro_make_laterable `{BiAffine PROP} (P Q : PROP) :
+Lemma test_iModIntro_make_laterable `{!BiAffine PROP} (P Q : PROP) :
   Laterable Q →
   P -∗ Q -∗ make_laterable (▷ P ∗ Q).
 Proof.
@@ -1284,6 +1284,13 @@ Proof.
   iIntros (Hφ) "H". iRevert (Hφ). Show. done.
 Qed.
 
+(* Check that when framing things under the â–¡ modality, we do not add [emp] in
+affine BIs. *)
+Check "test_iFrame_not_add_emp_for_intuitionistically".
+Lemma test_iFrame_not_add_emp_for_intuitionistically `{!BiAffine PROP} (P : PROP) :
+  □ P -∗ ∃ _ : nat, □ P.
+Proof. iIntros "#H". iFrame "H". Show. by iExists 0. Qed.
+
 End tests.
 
 Section parsing_tests.
-- 
GitLab