Make iAssumption work when the whole remaining spatial context is affine.

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 :

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"]

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.