Commit fd49bcbe authored by Ralf Jung's avatar Ralf Jung
Browse files

add back explicit framing instance for ↦

parent ea51b43b
......@@ -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.
......
......@@ -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].
......
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment