From 35ba9ba1710a46e6f57e49381c0d8d49a4ac4001 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Feb 2018 19:06:15 +0100
Subject: [PATCH] Some test cases/uses for stronger framing in disjunctions.

---
 theories/base_logic/lib/na_invariants.v | 4 ++--
 theories/tests/proofmode.v              | 6 ++++++
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 2e736737e..f0cb73628 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -47,8 +47,8 @@ Section proofs.
   Proof.
     iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
     iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
-    iNext. iAlways. iSplit; (iIntros "[[? Ho]|?]";
-      [iLeft; iFrame "Ho"; by iApply "HPQ"|by iRight]).
+    iNext; iAlways.
+    iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
   Qed.
 
   Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 44a04c5b5..45717fcca 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -104,6 +104,12 @@ Lemma test_iFrame_pure (x y z : M) :
   ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
 Proof. iIntros (Hv) "Hxy". by iFrame (Hv Hv) "Hxy". Qed.
 
+Lemma test_iFrame_disjunction_1 P1 P2 Q1 Q2 :
+  □ P1 -∗ Q2 -∗ P2 -∗ (P1 ∗ P2 ∗ False ∨ P2) ∗ (Q1 ∨ Q2).
+Proof. iIntros "#HP1 HQ2 HP2". iFrame "HP1 HQ2 HP2". Qed.
+Lemma test_iFrame_disjunction_2 P : P -∗ (True ∨ True) ∗ P.
+Proof. iIntros "HP". iFrame "HP". auto. Qed.
+
 Lemma test_iAssert_persistent P Q : P -∗ Q -∗ True.
 Proof.
   iIntros "HP HQ".
-- 
GitLab