From 020be80627531d33c86ee8cb85bfedca039e5b38 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 3 Nov 2017 18:01:55 +0100
Subject: [PATCH] Simplify uses of AffineEnv by making it easy to prove when
 the BI is affine.

---
 theories/proofmode/coq_tactics.v | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 7c003f243..67c483d10 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -443,16 +443,15 @@ Global Instance affine_env_snoc Γ i P :
   Affine P → AffineEnv Γ → AffineEnv (Esnoc Γ i P).
 Proof. by constructor. Qed.
 
+(* If the BI is affine, no need to walk on the whole environment. *)
+Global Instance affine_env_bi `(AffineBI PROP) Γ : AffineEnv Γ | 0.
+Proof. induction Γ; apply _. 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_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.
+  AffineEnv (env_spatial Δ) → Affine ([∗] env_spatial Δ).
+Proof. intros H. induction H; simpl; apply _. Qed.
+
+Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → Δ ⊢ emp.
 Proof. intros. by rewrite (affine Δ). Qed.
 
 Lemma tac_assumption Δ Δ' i p P Q :
@@ -571,7 +570,7 @@ Proof. destruct pe; by split. Qed.
 
 Lemma tac_always_intro Δ Δ' a pe pl Q Q' :
   FromAlways a pe pl Q' Q →
-  (if a then TCOr (AffineBI PROP) (AffineEnv (env_spatial Δ')) else TCTrue) →
+  (if a then AffineEnv (env_spatial Δ') else TCTrue) →
   IntoAlwaysEnvs pe pl Δ' Δ →
   (Δ ⊢ Q) → Δ' ⊢ Q'.
 Proof.
-- 
GitLab