From 7da8952e3cb5783e9dc91ea3abc60fa2706d08a4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Mar 2021 19:28:58 +0100
Subject: [PATCH] add more tests

---
 tests/proofmode.v         |  6 +++---
 tests/proofmode_monpred.v | 11 +++++++++++
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 9628ea7e4..97aa9604a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -457,17 +457,17 @@ Proof. iIntros (?) "HP #HQ HR". iPureIntro; eauto. Qed.
 
 (* Ensure that [% ...] works as a pattern when the left-hand side of and/sep is
 pure. *)
-Lemma test_pure_and_sep_destruct_affine `{!BiAffine PROP} (φ : Prop) (P : PROP) :
+Lemma test_pure_and_sep_destruct_affine `{!BiAffine PROP} (φ : Prop) P :
   ⌜φ⌝ ∧ (⌜φ⌝ ∗ P) -∗ P.
 Proof.
   iIntros "[% [% $]]".
 Qed.
-Lemma test_pure_and_sep_destruct_1 (φ : Prop) (P : PROP) :
+Lemma test_pure_and_sep_destruct_1 (φ : Prop) P :
   ⌜φ⌝ ∧ (<affine> ⌜φ⌝ ∗ P) -∗ P.
 Proof.
   iIntros "[% [% $]]".
 Qed.
-Lemma test_pure_and_sep_destruct_2 (φ : Prop) (P : PROP) :
+Lemma test_pure_and_sep_destruct_2 (φ : Prop) P :
   ⌜φ⌝ ∧ (⌜φ⌝ ∗ <absorb> P) -∗ <absorb> P.
 Proof.
   iIntros "[% [% $]]".
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 6e69c5c88..80612f2c0 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -103,6 +103,17 @@ Section tests.
     iAssumption.
   Qed.
 
+  Lemma test_monPred_at_and_pure P i j :
+    (monPred_in j ∧ P) i ⊢ ⌜ j ⊑ i ⌝ ∧ P i.
+  Proof.
+    iDestruct 1 as "[% $]". done.
+  Qed.
+  Lemma test_monPred_at_sep_pure P i j :
+    (monPred_in j ∗ <absorb> P) i ⊢ ⌜ j ⊑ i ⌝ ∧ <absorb> P i.
+  Proof.
+    iDestruct 1 as "[% ?]". auto.
+  Qed.
+
   Context (FU : BiFUpd PROP).
 
   Lemma test_apply_fupd_intro_mask_subseteq E1 E2 P :
-- 
GitLab