From 8022419a8d8656d71e365c95af43cee270f25879 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 24 Aug 2017 10:48:53 +0200
Subject: [PATCH] Make iAssumption work when the whole remaining spatial
 context is affine.

---
 theories/proofmode/coq_tactics.v | 18 +++++++++++++++---
 theories/proofmode/tactics.v     |  6 +++---
 theories/tests/proofmode.v       |  3 +++
 3 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index fa8acee90..32bddfd10 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -408,16 +408,28 @@ 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.
+Global Instance affine_env_snoc Γ i P :
+  Affine P → AffineEnv Γ → AffineEnv (Esnoc Γ i P).
+Proof. by constructor. Qed.
+
+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_assumption Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') →
   FromAssumption p P Q →
-  (if env_spatial_is_nil Δ' then TCTrue else Absorbing Q) →
+  (if env_spatial_is_nil Δ' then TCTrue
+   else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) →
   Δ ⊢ Q.
 Proof.
-  intros. rewrite envs_lookup_delete_sound //.
+  intros ?? H. rewrite envs_lookup_delete_sound //.
   destruct (env_spatial_is_nil Δ') eqn:?.
   - by rewrite (env_spatial_is_nil_bare_persistently Δ') // sep_elim_l.
-  - by rewrite from_assumption.
+  - rewrite from_assumption. destruct H as [?|?]=>//. by rewrite sep_elim_l.
 Qed.
 
 Lemma tac_rename Δ Δ' i j p P Q :
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 311944a27..03f23388f 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -136,7 +136,7 @@ Tactic Notation "iExact" constr(H) :=
 
 Tactic Notation "iAssumptionCore" :=
   let rec find Γ i P :=
-    match Γ with
+    lazymatch Γ with
     | Esnoc ?Γ ?j ?Q => first [unify P Q; unify i j|find Γ i P]
     end in
   match goal with
@@ -153,7 +153,7 @@ Tactic Notation "iAssumptionCore" :=
 Tactic Notation "iAssumption" :=
   let Hass := fresh in
   let rec find p Γ Q :=
-    match Γ with
+    lazymatch Γ with
     | Esnoc ?Γ ?j ?P => first
        [pose proof (_ : FromAssumption p P Q) as Hass;
         eapply (tac_assumption _ _ j p P);
@@ -167,7 +167,7 @@ Tactic Notation "iAssumption" :=
           |exact Hass]
        |find p Γ Q]
     end in
-  match goal with
+  lazymatch goal with
   | |- of_envs (Envs ?Γp ?Γs) ⊢ ?Q =>
      first [find true Γp Q | find false Γs Q
            |fail "iAssumption:" Q "not found"]
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 7d36c33c5..d2b31fd4c 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -71,6 +71,9 @@ Lemma test_very_fast_iIntros P :
   ∀ x y : nat, (⌜ x = y ⌝ → P -∗ P)%I.
 Proof. by iIntros. Qed.
 
+Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P -∗ Q -∗ R -∗ Q.
+Proof. iIntros "H1 H2 H3". iAssumption. Qed.
+
 Lemma test_iDestruct_spatial_and P Q1 Q2 : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1.
 Proof. iIntros "[H1 [H2 _]]". iFrame. Qed.
 
-- 
GitLab