Make mapsto_valid_2 consistent with ghost_var_valid_2

CHANGELOG.md

@@ -123,6 +123,8 @@ With this release, we dropped support for Coq 8.9.
   and looked very confusing in context: `l ↦ - ∗ P` looks like a magic wand.
 * Change `gen_inv_heap` notation `l ↦□ I` to `l ↦_I □`, so that `↦□` can be used
   by `gen_heap`.
+* Strengthen `mapsto_valid_2` to provide both a bound on the fractions and
+  agreement.
 
 **Changes in `program_logic`:**
 

theories/base_logic/lib/gen_heap.v

@@ -157,11 +157,23 @@ Section gen_heap.
     AsFractional (l ↦{q} v) (λ q, l ↦{q} v)%I q.
   Proof. split. done. apply _. Qed.
 
+  Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
+  Proof.
+    rewrite mapsto_eq. iIntros "Hl".
+    iDestruct (own_valid with "Hl") as %?%gmap_view_frag_valid. done.
+  Qed.
+  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝.
+  Proof.
+    rewrite mapsto_eq. iIntros "H1 H2".
+    iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_frag_op_valid_L.
+    eauto.
+  Qed.
+  (** Almost all the time, this is all you really need. *)
   Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
-    apply wand_intro_r.
-    rewrite mapsto_eq /mapsto_def -own_op own_valid discrete_valid.
-    apply pure_mono. intros [_ ?]%gmap_view_frag_op_valid_L. done.
+    iIntros "H1 H2".
+    iDestruct (mapsto_valid_2 with "H1 H2") as %[_ ?].
+    done.
   Qed.
 
   Lemma mapsto_combine l q1 q2 v1 v2 :
@@ -171,22 +183,11 @@ Section gen_heap.
     iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
   Qed.
 
-  Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
-  Proof.
-    rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
-    rewrite gmap_view_frag_valid //.
-  Qed.
-  Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ✓ (q1 + q2)%Qp.
-  Proof.
-    iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %->.
-    iApply (mapsto_valid l _ v2). by iFrame.
-  Qed.
-
   Lemma mapsto_mapsto_ne l1 l2 q1 q2 v1 v2 :
     ¬ ✓(q1 + q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
   Proof.
     iIntros (?) "Hl1 Hl2"; iIntros (->).
-    by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %?.
+    by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
   Qed.
 
   (** General properties of [meta] and [meta_token] *)

theories/base_logic/lib/gen_inv_heap.v

@@ -201,7 +201,7 @@ Section inv_heap.
     destruct (h !! l) as [v'| ] eqn: Hlookup.
     - (* auth map contains l --> contradiction *)
       iDestruct (big_sepM_lookup with "HsepM") as "[_ Hl']"; first done.
-      by iDestruct (mapsto_valid_2 with "Hl Hl'") as %?.
+      by iDestruct (mapsto_valid_2 with "Hl Hl'") as %[??].
     - iMod (own_update with "H●") as "[H● H◯]".
       { apply lookup_to_inv_heap_None in Hlookup.
         apply (auth_update_alloc _

theories/heap_lang/primitive_laws.v

@@ -291,6 +291,12 @@ Global Instance ex_mapsto_as_fractional l q :
   AsFractional (l ↦{q} -) (λ q, l ↦{q} -)%I q.
 Proof. split. done. apply _. Qed.
 
+Lemma mapsto_valid_2 l q1 q2 v1 v2 :
+  l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝.
+Proof.
+  iIntros "H1 H2". iDestruct (mapsto_valid_2 with "H1 H2") as %[? [=?]]. done.
+Qed.
+
 Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝.
 Proof. iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %[=?]. done. Qed.
 
@@ -303,8 +309,6 @@ Qed.
 
 Lemma mapsto_valid l q v : l ↦{q} v -∗ ✓ q.
 Proof. apply mapsto_valid. Qed.
-Lemma mapsto_valid_2 l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ✓ (q1 + q2)%Qp.
-Proof. apply mapsto_valid_2. Qed.
 Lemma mapsto_mapsto_ne l1 l2 q1 q2 v1 v2 :
   ¬ ✓(q1 + q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
 Proof. apply mapsto_mapsto_ne. Qed.