From fe43c8dfb797be0c43a1be5e8f44b75de49ffd56 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Jun 2022 16:20:49 -0400
Subject: [PATCH] add a test

---
 tests/atomic.ref |  2 ++
 tests/atomic.v   | 14 ++++++++++++--
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/tests/atomic.ref b/tests/atomic.ref
index de749e7a9..0c7d1674c 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -1,3 +1,5 @@
+The command has indeed failed with message:
+Tactic failure: iAuIntro: spacial context empty, and emp not laterable.
 1 goal
   
   Σ : gFunctors
diff --git a/tests/atomic.v b/tests/atomic.v
index 20b83453a..8fa7ac6fd 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 
 Unset Mangle Names.
 
-Section definition.
+Section general_bi_tests.
   Context `{BiFUpd PROP} {TA TB : tele} (Eo Ei : coPset).
 
   (** We can quantify over telescopes *inside* Iris and use them with atomic
@@ -14,7 +14,17 @@ Section definition.
   Definition AU_tele_quantify_iris : Prop :=
     ⊢ ∀ (TA TB : tele) (α : TA → PROP) (β Φ : TA → TB → PROP),
         atomic_update Eo Ei α β Φ.
-End definition.
+
+  (** iAuIntro works with non-empty laterable spacial context without any further
+  assumptions. *)
+  Lemma au_intro_1 (P : PROP) `{!Laterable P} (α : TA → PROP) (β Φ : TA → TB → PROP) :
+    P -∗ atomic_update Eo Ei α β Φ.
+  Proof. iIntros "HP". iAuIntro. Abort.
+  (** But in an empty context, it fails, since [emp] now needs to be laterable. *)
+  Lemma au_intro_2 (α : TA → PROP) (β Φ : TA → TB → PROP) :
+    ⊢ atomic_update Eo Ei α β Φ.
+  Proof. Fail iAuIntro. Abort.
+End general_bi_tests.
 
 Section tests.
   Context `{!heapGS Σ} {aheap: atomic_heap Σ}.
-- 
GitLab