From 07b3a7dbf8ac9e25cd6c20e986dc29f1e5f0420c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 5 Nov 2020 11:26:36 +0100
Subject: [PATCH] Add variant of mapsto_mapsto_ne that does not require further
 fraction reasoning

---
 CHANGELOG.md                        | 4 ++++
 theories/base_logic/lib/gen_heap.v  | 4 +++-
 theories/heap_lang/primitive_laws.v | 6 ++++--
 3 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 61ee78e40..93c63457d 100644
--- a/CHANGELOG.md
+++ b/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
 ```
 
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index d368da7b6..73d9aa5a5 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/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).
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index 425121877..ce297d8e6 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/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).
-- 
GitLab