Stop `iAssumption` from unifying evar premises with `False`

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:

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]

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

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).