`FromSep` instance for the locking heap mapsto

theories/lib/locking_heap.v

@@ -175,7 +175,7 @@ Section properties.
     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.
+  Lemma mapsto_combine l x x' 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]".
@@ -186,6 +186,13 @@ Section properties.
     iCombine "Ho1 Ho2" as "Ho". rewrite frac_op'. iFrame.
   Qed.
 
+  Global Instance from_sep_mapsto l x x' q q' v :
+    FromSep (l ↦C[x⋅x']{q+q'} v) (l ↦C[x]{q} v) (l ↦C[x']{q'} v).
+  Proof.
+    rewrite /FromSep. iIntros "[Hl1 Hl2]".
+    iApply (mapsto_combine with "Hl1 Hl2").
+  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.

theories/tests/test1.v

@@ -8,10 +8,11 @@ Section test.
   Context `{amonadG Σ}.
 
   Lemma test1 (l : loc) :
-    l ↦C[LLvl] #1 -∗
+    l ↦C[LLvl]{1/2} #1 -∗ l ↦C[LLvl]{1/2} #1 -∗
     awp (a_seq #();;; a_load (a_ret #l)) True (λ v, ⌜v = #1⌝ ∗ l ↦C #1).
   Proof.
-    iIntros "Hl".
+    iIntros "Hl1 Hl2". iCombine "Hl1 Hl2" as "Hl".
+    rewrite Qp_half_half.
     iApply awp_bind.
     iApply a_seq_spec.
     iModIntro.

theories/vcgen/denv.v

@@ -193,7 +193,7 @@ Section denv_spec.
            rewrite /denv_interp_aux. simpl. Transparent denv_insert.
            iDestruct "H1" as "[H1 $]".
            iDestruct (mapsto_value_agree with "H1 H2") as %->.
-           iDestruct (mapsto_combine with "H1 H2") as "H".
+           iCombine "H1 H2" as "H".
            iApply (mapsto_downgrade' with "H").
            apply lvl_included. destruct x,x'; eauto.
           * iIntros "[H1 H2]".
@@ -240,7 +240,7 @@ Section denv_spec.
        (* TODO: this can be factored away *)
        destruct dio1 as [d1|], dio2 as [d2|]; simpl; iFrame.
        + destruct d1, d2. simpl. iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->.
-         iDestruct (mapsto_combine with "Hl1 Hl2") as "$".
+         iCombine "Hl1 Hl2" as "$".
          iApply (big_sepL_mono with "IH1"). intros n y ?. simpl.
          assert ((k + S n)%nat = ((S k) + n)%nat) as -> by omega. done.
        + iApply (big_sepL_mono with "IH1"). intros n y ?. simpl.