Make iPureIntro able to introduce [bi_affinely (bi_pure P)] when the context is empty.

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, Δ') →

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 :

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