From 36654e769c49adaa99ef058223b7cb171f8d7808 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 15 Feb 2018 17:05:40 +0100
Subject: [PATCH] Make iPureIntro able to introduce [bi_affinely (bi_pure P)]
 when the context is empty.

---
 theories/proofmode/coq_tactics.v  | 10 ++++++++--
 theories/proofmode/environments.v |  6 ------
 theories/proofmode/tactics.v      |  3 ++-
 3 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index e273f9f45..9e971ae75 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -524,8 +524,14 @@ Proof.
 Qed.
 
 (** * Pure *)
-Lemma tac_pure_intro Δ Q φ : FromPure false Q φ → φ → envs_entails Δ Q.
-Proof. intros ??. rewrite envs_entails_eq -(from_pure _ Q). by apply pure_intro. Qed.
+Lemma tac_pure_intro Δ Q φ af :
+  env_spatial_is_nil Δ = af → FromPure af Q φ → φ → envs_entails Δ Q.
+Proof.
+  intros ???. rewrite envs_entails_eq -(from_pure _ Q). destruct af.
+  - rewrite env_spatial_is_nil_affinely_persistently //=. f_equiv.
+    by apply pure_intro.
+  - by apply pure_intro.
+Qed.
 
 Lemma tac_pure Δ Δ' i p P φ Q :
   envs_lookup_delete i Δ = Some (p, P, Δ') →
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 2e5abfb31..4816f938a 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -69,12 +69,6 @@ Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
      else ''(y,Γ') ← env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
   end.
 
-Definition env_is_singleton {A} (Γ : env A) : bool :=
-  match Γ with
-  | Esnoc (Esnoc Enil _ _) _ _ => true
-  | _ => false
-  end.
-
 Inductive env_Forall2 {A B} (P : A → B → Prop) : env A → env B → Prop :=
   | env_Forall2_nil : env_Forall2 P Enil Enil
   | env_Forall2_snoc Γ1 Γ2 i x y :
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 9e06f66fa..cf98dc70b 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -229,7 +229,8 @@ Tactic Notation "iEmpIntro" :=
 Tactic Notation "iPureIntro" :=
   iStartProof;
   eapply tac_pure_intro;
-    [apply _ ||
+    [env_reflexivity
+    |apply _ ||
      let P := match goal with |- FromPure _ ?P _ => P end in
      fail "iPureIntro:" P "not pure"
     |].
-- 
GitLab