From be7ca8aa2c8485de2912241298a97bedb2a53724 Mon Sep 17 00:00:00 2001
From: Joseph Tassarotti <jtassaro@andrew.cmu.edu>
Date: Wed, 21 Feb 2018 09:50:01 -0500
Subject: [PATCH] More tests of iInv.

---
 theories/tests/proofmode_iris.v | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/theories/tests/proofmode_iris.v b/theories/tests/proofmode_iris.v
index 01b80bb6a..b702dd745 100644
--- a/theories/tests/proofmode_iris.v
+++ b/theories/tests/proofmode_iris.v
@@ -60,7 +60,7 @@ Section iris_tests.
     by iApply inv_alloc.
   Qed.
 
-  Lemma test_iInv_1 N P: inv N (bi_persistently P) ={⊤}=∗ ▷ P.
+  Lemma test_iInv_0 N P: inv N (bi_persistently P) ={⊤}=∗ ▷ P.
   Proof.
     iIntros "#H".
     iInv N as "#H2" "Hclose".
@@ -68,6 +68,16 @@ Section iris_tests.
     iModIntro. by iNext.
   Qed.
 
+  Lemma test_iInv_1 N E P:
+    ↑N ⊆ E →
+    inv N (bi_persistently P) ={E}=∗ ▷ P.
+  Proof.
+    iIntros (?) "#H".
+    iInv N as "#H2" "Hclose".
+    iMod ("Hclose" with "H2").
+    iModIntro. by iNext.
+  Qed.
+
   Lemma test_iInv_2 γ p N P:
     cinv N γ (bi_persistently P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
   Proof.
@@ -187,4 +197,14 @@ Section iris_tests.
     Fail iInv "H2" as "#H2" "Hclose".
     done.
   Qed.
+
+  (* test destruction of existentials when opening an invariant *)
+  Lemma test_iInv_13 N:
+    inv N (∃ (v1 v2 v3 : nat), emp ∗ emp ∗ emp) ={⊤}=∗ ▷ emp.
+  Proof.
+    iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)" "Hclose".
+    iMod ("Hclose" with "[]").
+    { iNext; iExists O; done. }
+    iModIntro. by iNext.
+  Qed.
 End iris_tests.
-- 
GitLab