Tests for framing under conjunctions.

19f72a60 · Robbert Krebbers · 082ba8f2 · 19f72a60
Commit 19f72a60 authored Feb 02, 2018 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 7 additions and 0 deletions

theories/tests/proofmode.v theories/tests/proofmode.v +7 -0

No files found.
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -110,6 +110,13 @@ 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_iFrame_conjunction_1 P Q :
+  P -∗ Q -∗ (P ∗ Q) ∧ (P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
+Lemma test_iFrame_conjunction_2 P Q :
+  P -∗ Q -∗ (P ∧ P) ∗ (Q ∧ Q).
+Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
+
 Lemma test_iAssert_persistent P Q : P -∗ Q -∗ True.
 Proof.
  iIntros "HP HQ".