Lemma for combining `- ↦C -`.

theories/lib/locking_heap.v

@@ -165,6 +165,25 @@ Section properties.
     apply lvl_included. destruct x; eauto.
   Qed.
 
+  Lemma mapsto_value_agree x x' l q q' v v' : l ↦C[x]{q} v -∗ l ↦C[x']{q'} v' -∗ ⌜v = v'⌝.
+  Proof.
+    rewrite mapsto_eq /mapsto_def.
+    iDestruct 1 as (b1 ?) "[Hl1 Ho1]".
+    iDestruct 1 as (b2 ?) "[Hl2 Ho2]".
+    iDestruct (mapsto_agree with "Hl1 Hl2") as %->. done.
+  Qed.
+
+  Lemma mapsto_combine x x' l q q' v : l ↦C[x]{q} v -∗ l ↦C[x']{q'} v -∗ l ↦C[x ⋅ x']{q+q'} v.
+  Proof.
+    rewrite mapsto_eq /mapsto_def.
+    iDestruct 1 as (b1 Hb1) "[Hl1 Ho1]".
+    iDestruct 1 as (b2 Hb2) "[Hl2 Ho2]".
+    iExists (b1 ⋅ b2). iSplitR.
+    { iPureIntro. destruct x,x',b1,b2; eauto. }
+    iCombine "Hl1 Hl2" as "Hl". rewrite Qp_mult_plus_distr_l.
+    iCombine "Ho1 Ho2" as "Ho". rewrite frac_op'. iFrame.
+  Qed.
+
   Lemma to_locking_heap_insert σ l x :
     to_locking_heap (<[l := x]> σ) = <[l := (1%Qp, x)]>(to_locking_heap σ).
   Proof. by rewrite /to_locking_heap fmap_insert. Qed.