From fd49bcbe2194fcfec59eb128e01aa87edb61f169 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 29 Nov 2021 14:07:20 -0500
Subject: [PATCH] =?UTF-8?q?add=20back=20explicit=20framing=20instance=20fo?=
 =?UTF-8?q?r=20=E2=86=A6?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris/base_logic/lib/gen_heap.v | 6 ++++++
 iris/bi/lib/fractional.v       | 6 ++++--
 tests/heap_lang.v              | 8 ++++++++
 3 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index 467b9f90c..7df5ef405 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -177,6 +177,12 @@ Section gen_heap.
   Lemma mapsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
   Proof. rewrite mapsto_eq. apply ghost_map_elem_persist. Qed.
 
+  (** Framing support *)
+  Global Instance frame_mapsto p l v q1 q2 RES :
+    FrameFractionalHyps p (l ↦{#q1} v) (λ q, l ↦{#q} v)%I RES q1 q2 →
+    Frame p (l ↦{#q1} v) (l ↦{#q2} v) RES | 5.
+  Proof. apply: frame_fractional. Qed.
+
   (** General properties of [meta] and [meta_token] *)
   Global Instance meta_token_timeless l N : Timeless (meta_token l N).
   Proof. rewrite meta_token_eq. apply _. Qed.
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 81552437d..9b48116c8 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -194,11 +194,13 @@ Section fractional.
   Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
     frame_fractional_hyps_half.
 
-  (* Not an instance because of performance; you can locally add it if you are willing to pay the cost. *)
+  (* Not an instance because of performance; you can locally add it if you are
+  willing to pay the cost. We have concrete instances for certain fractional
+  assertions such as ↦. *)
   Lemma frame_fractional p R r Φ P q RES:
     AsFractional R Φ r → AsFractional P Φ q →
     FrameFractionalHyps p R Φ RES r q →
-    Frame p R P RES. (* No explicit priority, as default prio > [frame_here]'s 1. *)
+    Frame p R P RES.
   Proof.
     rewrite /Frame=>-[HR _][->?]H.
     revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 1c4d73212..0e80ada63 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -373,6 +373,14 @@ Section mapsto_tests.
     l ↦{#1 / 2} v -∗  ∃ q, l ↦{#1 / 2 + q} v.
   Proof. iIntros "H". iExists _. iSplitL; first by iAssumption. Abort.
 
+  Lemma mapsto_frame_1 l v q1 q2 :
+    l ↦{#q1} v -∗ l ↦{#q2} v -∗ l ↦{#q1 + q2} v.
+  Proof. iIntros "H1 H2". iFrame "H1". iExact "H2". Qed.
+
+  Lemma mapsto_frame_2 l v q :
+    l ↦{#q/2} v -∗ l ↦{#q/2} v -∗ l ↦{#q} v.
+  Proof. iIntros "H1 H2". iFrame "H1". iExact "H2". Qed.
+
 End mapsto_tests.
 
 Section inv_mapsto_tests.
-- 
GitLab