Add variant of mapsto_mapsto_ne that does not require further fraction reasoning

CHANGELOG.md

@@ -130,6 +130,8 @@ With this release, we dropped support for Coq 8.9.
   `⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝`.
 * Change `gen_heap_init` to also return ownership of the points-to facts for the
   initial heap.
+* Rename `mapsto_mapsto_ne` to `mapsto_frac_ne`, and add a simpler
+  `mapsto_ne` that does not require reasoning about fractions.
 
 **Changes in `program_logic`:**
 
@@ -159,6 +161,8 @@ s/\bauth_both_frac_valid\b/auth_both_frac_valid_discrete/g
 # gen_heap_ctx and proph_map_ctx
 s/\bgen_heap_ctx\b/gen_heap_interp/g
 s/\bproph_map_ctx\b/proph_map_interp/g
+# other gen_heap changes
+s/\bmapsto_mapsto_ne\b/mapsto_frac_ne/g
 EOF
 ```
 

theories/base_logic/lib/gen_heap.v

@@ -172,12 +172,14 @@ Section gen_heap.
     iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
   Qed.
 
-  Lemma mapsto_mapsto_ne l1 l2 q1 q2 v1 v2 :
+  Lemma mapsto_frac_ne l1 l2 q1 q2 v1 v2 :
     ¬ (q1 + q2 ≤ 1)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
   Proof.
     iIntros (?) "Hl1 Hl2"; iIntros (->).
     by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
   Qed.
+  Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+  Proof. apply mapsto_frac_ne, Qp_not_add_le_l. Qed.
 
   (** General properties of [meta] and [meta_token] *)
   Global Instance meta_token_timeless l N : Timeless (meta_token l N).

theories/heap_lang/primitive_laws.v

@@ -294,9 +294,11 @@ Proof.
   iCombine "Hl1 Hl2" as "Hl". eauto with iFrame.
 Qed.
 
-Lemma mapsto_mapsto_ne l1 l2 q1 q2 v1 v2 :
+Lemma mapsto_frac_ne l1 l2 q1 q2 v1 v2 :
   ¬ (q1 + q2 ≤ 1)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
-Proof. apply mapsto_mapsto_ne. Qed.
+Proof. apply mapsto_frac_ne. Qed.
+Lemma mapsto_ne l1 l2 q2 v1 v2 : l1 ↦ v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝.
+Proof. apply mapsto_ne. Qed.
 
 Global Instance inv_mapsto_own_proper l v :
   Proper (pointwise_relation _ iff ==> (≡)) (inv_mapsto_own l v).