From e896ce1a58f42df81d90b5212e8850847ab44cfc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 30 Aug 2017 11:57:35 +0200
Subject: [PATCH] Make iEmpIntro succeed in a non-empty, but affine, spatial
 context.

---
 theories/proofmode/coq_tactics.v | 15 ++++++++-------
 theories/proofmode/tactics.v     |  3 ++-
 theories/tests/proofmode.v       |  4 ++++
 3 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 817edd512..9557c72f6 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -435,13 +435,6 @@ Proof.
 Qed.
 
 (** * Basic rules *)
-Lemma tac_emp_intro Δ :
-  env_spatial_is_nil Δ = true →
-  Δ ⊢ emp.
-Proof.
-  intros. by rewrite (env_spatial_is_nil_bare_persistently Δ) // (affine (⬕ Δ)).
-Qed.
-
 Class AffineEnv (Γ : env PROP) := affine_env : Forall Affine Γ.
 Global Instance affine_env_nil : AffineEnv Enil.
 Proof. constructor. Qed.
@@ -453,6 +446,14 @@ Instance affine_env_spatial Δ :
   TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ)) → Affine ([∗] env_spatial Δ).
 Proof. destruct 1 as [?|H]. apply _. induction H; simpl; apply _. Qed.
 
+Lemma tac_emp_intro Δ :
+  (* Establishing [AffineEnv (env_spatial Δ)] is rather expensive (linear in the
+  size of the context), so first check whether the whole BI is affine (which
+  takes constant time). *)
+  TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ)) →
+  Δ ⊢ emp.
+Proof. intros [?|?]; by rewrite (affine Δ). Qed.
+
 Lemma tac_assumption Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') →
   FromAssumption p P Q →
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 51eb5eabd..b9b48ab08 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -202,7 +202,8 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
 Tactic Notation "iEmpIntro" :=
   iStartProof;
   eapply tac_emp_intro;
-    [env_reflexivity || fail "iEmpIntro: spatial context is non-empty"].
+    [env_cbv; apply _ ||
+     fail "iEmpIntro: spatial context contains non-affine hypotheses"].
 
 Tactic Notation "iPureIntro" :=
   iStartProof;
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 7aaec057b..8c6ce8060 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -91,6 +91,10 @@ Lemma test_iSpecialize_auto_frame P Q R :
   (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
 Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
 
+Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
+  P -∗ Q → R -∗ emp.
+Proof. iIntros "HP #HQ HR". iEmpIntro. Qed.
+
 (* Check coercions *)
 Lemma test_iExist_coercion (P : Z → PROP) : (∀ x, P x) -∗ ∃ x, P x.
 Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
-- 
GitLab