Merge branch 'ci/ralf/frame-frac' into 'master'

don't make frame_fractional an instance

Closes #351

See merge request iris/iris!739

CHANGELOG.md

@@ -41,6 +41,10 @@ lemma.
   Proofs that are generic in `PROP` might have to add those new classes as
   assumptions to remain compatible, and code that instantiates the BI interface
   needs to provide instances for the new classes.
+* Make `frame_fractional` not an instance any more; instead fractional
+  propositions that want to support framing are expected to register an
+  appropriate instance themselves. HeapLang and gen_heap `↦` still support
+  framing, but the other fractional propositions in Iris do not.
 
 **Changes in `heap_lang`:**
 

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.

iris/bi/lib/fractional.v

@@ -194,10 +194,13 @@ Section fractional.
   Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
     frame_fractional_hyps_half.
 
-  Global Instance frame_fractional p R r Φ P q RES:
+  (* 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].

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.