From 0fe0a881b6a7e7912e362eb742e064b9db8caab3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 5 Mar 2023 10:29:05 +0100
Subject: [PATCH] Add test for `unseal` of `siProp`.

---
 tests/siprop.ref | 17 +++++++++++++++++
 tests/siprop.v   | 10 ++++++++++
 2 files changed, 27 insertions(+)

diff --git a/tests/siprop.ref b/tests/siprop.ref
index e69de29bb..c7ab6a8bf 100644
--- a/tests/siprop.ref
+++ b/tests/siprop.ref
@@ -0,0 +1,17 @@
+"unseal_test"
+     : string
+1 goal
+  
+  P, Q : siProp
+  Φ : nat → siProp
+  ============================
+  siprop.siProp_and_def P
+    (siprop.siProp_and_def (siprop.siProp_later_def Q)
+       (siprop.siProp_exist_def (λ x : nat, Φ x)))
+  ⊣⊢ siprop.siProp_exist_def
+       (λ x : nat,
+          siprop.siProp_or_def
+            (siprop.siProp_and_def P
+               (siprop.siProp_and_def (siprop.siProp_later_def Q)
+                  (siprop.siProp_pure_def True))) 
+            (Φ x))
diff --git a/tests/siprop.v b/tests/siprop.v
index fc72d0ccc..9e6c6b7d5 100644
--- a/tests/siprop.v
+++ b/tests/siprop.v
@@ -1,4 +1,14 @@
+From stdpp Require Import strings.
 From iris.si_logic Require Import bi.
+Unset Mangle Names.
+
+Check "unseal_test".
+Lemma unseal_test (P Q : siProp) (Φ : nat → siProp) :
+  P ∧ ▷ Q ∧ (∃ x, Φ x) ⊣⊢ ∃ x, P ∗ ▷ Q ∧ emp ∨ Φ x.
+Proof.
+  siProp.unseal.
+  Show.
+Abort.
 
 (** Make sure that [siProp]s are parsed in [bi_scope]. *)
 Definition test : siProp := â–· True.
-- 
GitLab