From 8812a3a319c2c1ad106cdb72f6db0962d1e824db Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 31 Oct 2022 08:07:32 +0100
Subject: [PATCH] =?UTF-8?q?Tests,=20the=20same=20we=20have=20for=20`?=
 =?UTF-8?q?=E2=8C=9C=20=CF=86=20=E2=8C=9D=20=E2=86=92=20...`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 tests/proofmode.ref | 44 ++++++++++++++++++++++++++++++++++++++++++++
 tests/proofmode.v   | 32 ++++++++++++++++++++++++++++++++
 2 files changed, 76 insertions(+)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 57992ccc9..9db702ed6 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -178,6 +178,50 @@ Tactic failure: iSpecialize: Q not persistent.
   ⌜φ⌝
 1 goal
   
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  "H1" : P
+  --------------------------------------â–¡
+  ⌜φ⌝
+"test_iSpecialize_impl_pure"
+     : string
+1 goal
+  
+  PROP : bi
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  --------------------------------------∗
+  <affine> ⌜φ⌝
+1 goal
+  
+  PROP : bi
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  "H1" : P
+  --------------------------------------â–¡
+  <affine> ⌜φ⌝
+"test_iSpecialize_impl_pure_affine"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  --------------------------------------∗
+  ⌜φ⌝
+1 goal
+  
   PROP : bi
   BiAffine0 : BiAffine PROP
   φ : Prop
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 8a48e4930..700bb4382 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -480,6 +480,38 @@ Restart.
   by iFrame.
 Abort.
 
+Check "test_iSpecialize_impl_pure".
+Lemma test_iSpecialize_forall_pure (φ : Prop) P Q :
+  φ → □ (∀ _ : φ, P) -∗ (∀ _ : φ, Q) -∗ P ∗ Q.
+Proof.
+  iIntros (?) "#H1 H2".
+  (* Adds an affine modality *)
+  iSpecialize ("H1" with "[]"). { Show. done. }
+  iSpecialize ("H2" with "[]"). { Show. done. }
+Restart.
+  iIntros (?) "#H1 H2".
+  (* Solving it directly as a pure goal also works. *)
+  iSpecialize ("H1" with "[% //]").
+  iSpecialize ("H2" with "[% //]").
+  by iFrame.
+Abort.
+
+Check "test_iSpecialize_impl_pure_affine".
+Lemma test_iSpecialize_forall_pure_affine `{!BiAffine PROP} (φ : Prop) P Q :
+  φ → □ (∀ _ : φ, P) -∗ (∀ _ : φ, Q) -∗ P ∗ Q.
+Proof.
+  iIntros (?) "#H1 H2".
+  (* Does not add an affine modality *)
+  iSpecialize ("H1" with "[]"). { Show. done. }
+  iSpecialize ("H2" with "[]"). { Show. done. }
+Restart.
+  iIntros (?) "#H1 H2".
+  (* Solving it directly as a pure goal also works. *)
+  iSpecialize ("H1" with "[% //]").
+  iSpecialize ("H2" with "[% //]").
+  by iFrame.
+Abort.
+
 Check "test_iAssert_intuitionistic".
 Lemma test_iAssert_intuitionistic `{!BiBUpd PROP} P :
   □ P -∗ □ |==> P.
-- 
GitLab