From f7956eda384df6a2ce523cf5baadca023f9d9cdb Mon Sep 17 00:00:00 2001
From: Janno <janno@mpi-sws.org>
Date: Mon, 24 Jan 2022 14:55:57 +0000
Subject: [PATCH] Stop `iAssumption` from unifying evar premises with `False`

---
 CHANGELOG.md                  |  9 +++++++++
 iris/proofmode/ltac_tactics.v |  3 ++-
 tests/proofmode.ref           |  4 ++++
 tests/proofmode.v             | 22 ++++++++++++++--------
 4 files changed, 29 insertions(+), 9 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 783b24183..162142ed4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,15 @@ way the logic is used on paper.  We also document changes in the Coq
 development; every API-breaking change should be listed, but not every new
 lemma.
 
+## Iris master
+
+**Changes in `proofmode`:**
+
+* `iAssumption` no longer instantiates evar premises with `False`. This used
+   to occur when the conclusion contains variables that are not in scope of the
+   evar, thus blocking the default behavior of instantiating the premise with
+   the conclusion. The old behavior can be emulated with`iExFalso. iExact "H".`
+
 ## Iris 3.6.0 (2022-01-22)
 
 The highlights and most notable changes of this release are:
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 6f605be73..8bed13969 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -306,7 +306,8 @@ Tactic Notation "iAssumption" :=
           |exact Hass
           |pm_reduce; iSolveTC ||
            fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"]
-       |assert (P = False%I) as Hass by reflexivity;
+       |assert_fails (is_evar P); 
+        assert (P = False%I) as Hass by reflexivity;
         apply (tac_false_destruct _ j p P);
           [pm_reflexivity
           |exact Hass]
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index cd1337a5d..cf81d3910 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -254,6 +254,10 @@ Tactic failure: iEval: %: unsupported selection pattern.
   â–· emp
 The command has indeed failed with message:
 Tactic failure: iFrame: cannot frame Q.
+The command has indeed failed with message:
+No applicable tactic.
+The command has indeed failed with message:
+No applicable tactic.
 "test_and_sep_affine_bi"
      : string
 1 goal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index aa055dc3b..7d9fecc09 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -326,11 +326,6 @@ Definition tc_opaque_test : PROP := tc_opaque (∀ x : nat, ⌜ x = x ⌝)%I.
 Lemma test_iIntros_tc_opaque : ⊢ tc_opaque_test.
 Proof. by iIntros (x). Qed.
 
-(** Prior to 0b84351c this used to loop, now [iAssumption] instantiates [R] with
-[False] and performs false elimination. *)
-Lemma test_iAssumption_evar_ex_false : ∃ R, R ⊢ ∀ P, P.
-Proof. eexists. iIntros "?" (P). iAssumption. Qed.
-
 Lemma test_iApply_evar P Q R : (∀ Q, Q -∗ P) -∗ R -∗ P.
 Proof. iIntros "H1 H2". iApply "H1". iExact "H2". Qed.
 
@@ -978,12 +973,23 @@ Lemma test_iAssumption_evar P : ∃ R, (R ⊢ P) ∧ R = P.
 Proof.
   eexists. split.
   - iIntros "H". iAssumption.
-  (* Now verify that the evar was chosen as desired (i.e., it should not pick False). *)
-  - reflexivity.
+  - (* Verify that [iAssumption] instantiates the evar for the existential [R]
+    to become [P], and in particular, that it does not make it [False]. *)
+    reflexivity.
 Qed.
 
+(** Prior to 0b84351c this used to loop, now [iAssumption] fails. *)
 Lemma test_iAssumption_False_no_loop : ∃ R, R ⊢ ∀ P, P.
-Proof. eexists. iIntros "?" (P). done. Qed.
+Proof.
+  eexists. iIntros "H" (P).
+  (* Make sure that [iAssumption] does not perform False elimination on
+  hypotheses that are evars. *)
+  Fail iAssumption.
+  (* And neither does [done]. *)
+  Fail done.
+  (* But we can of course achieve that using an explicit proof. *)
+  iExFalso. iExact "H".
+Qed.
 
 Lemma test_apply_affine_impl `{!BiPlainly PROP} (P : PROP) :
   P -∗ (∀ Q : PROP, ■ (Q -∗ <pers> Q) → ■ (P -∗ Q) → Q).
-- 
GitLab