From a932b1948d03124675d893531b697a66eb9f8091 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 20 Mar 2020 13:23:01 +0100
Subject: [PATCH] More general instance for framing under `<affine>`.
---
tests/proofmode.v | 7 +++++++
theories/proofmode/frame_instances.v | 9 +++++----
2 files changed, 12 insertions(+), 4 deletions(-)
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 485d249c6..28d3d010d 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -455,6 +455,13 @@ Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
Lemma test_iFrame_later `{!BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
Proof. iIntros "H1 H2". by iFrame "H1". Qed.
+Lemma test_iFrame_affinely_1 P Q `{!Affine P} :
+ P -∗ <affine> Q -∗ <affine> (P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+Lemma test_iFrame_affinely_2 P Q `{!Affine P, !Affine Q} :
+ P -∗ Q -∗ <affine> (P ∗ Q).
+Proof. iIntros "HP HQ". iFrame "HQ". iExact "HP". Qed.
+
Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
Proof.
iIntros "HF".
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index ff71e3a10..6d4a660ed 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -204,11 +204,12 @@ Proof. by rewrite /KnownMakeAffinely /MakeAffinely affinely_True_emp affinely_em
Global Instance make_affinely_default P : MakeAffinely P (<affine> P) | 100.
Proof. by rewrite /MakeAffinely. Qed.
-Global Instance frame_affinely R P Q Q' :
- Frame true R P Q → MakeAffinely Q Q' → Frame true R (<affine> P) Q'.
+Global Instance frame_affinely p R P Q Q' :
+ TCOr (TCEq p true) (Affine R) →
+ Frame p R P Q → MakeAffinely Q Q' → Frame p R (<affine> P) Q'.
Proof.
- rewrite /Frame /MakeAffinely=> <- <- /=.
- rewrite -{1}(affine_affinely (â–¡ R)%I) affinely_sep_2 //.
+ rewrite /Frame /MakeAffinely=> -[->|?] <- <- /=;
+ by rewrite -{1}(affine_affinely (_ R)%I) affinely_sep_2.
Qed.
Global Instance make_intuitionistically_emp :
--
GitLab