From f227f6fa140095c2adc131972ad555e86ccc5add Mon Sep 17 00:00:00 2001
From: Abel Nieto <abeln@cs.au.dk>
Date: Fri, 3 Apr 2020 12:12:06 +0200
Subject: [PATCH] Add mapsto_mapsto_ne helper lemma
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Here's one case this lemma might be useful. Suppose we want to
programmatically generate namespaces for e.g. locks:

```
Definition lockN (l : loc) := nroot .@ "lock" .@ l.
```

Then to know that two such namespaces are disjoint, we need to know
that the corresponding locations are distinct. For that we use
the lemma here introduced.

```
Lemma ne l1 l2 v1 v2 :
  l1 ↦ v1 -∗ l2 ↦ v2 -∗ ⌜l1 ≠ l2⌝.
Proof. iApply mapsto_mapsto_ne. (* goal ¬ ✓ 2%Qp *) by intros []. Qed.
```
---
 CHANGELOG.md                       | 1 +
 theories/base_logic/lib/gen_heap.v | 7 +++++++
 2 files changed, 8 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7af05c2cf..3174c1738 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -157,6 +157,7 @@ Coq development, but not every API-breaking change is listed.  Changes marked
     version `coreP_entails'` for `coreP P` with `P` affine.
   + Add instance `coreP_affine P : Affine P → Affine (coreP P)` and
     lemma `coreP_wand P Q : <affine> ■ (P -∗ Q) -∗ coreP P -∗ coreP Q`.
+* Add lemma `mapsto_mapsto_ne : ¬ ✓(q1 + q2)%Qp → l1 ↦{q1} v1 -∗ l2 ↦{q2} v2 -∗ ⌜l1 ≠ l2⌝`.
 
 The following `sed` script should perform most of the renaming (FIXME: incomplete)
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 091e77d61..afeaad208 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -233,6 +233,13 @@ Section gen_heap.
     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 %?.
+  Qed.
+
   (** General properties of [meta] and [meta_token] *)
   Global Instance meta_token_timeless l N : Timeless (meta_token l N).
   Proof. rewrite meta_token_eq /meta_token_def. apply _. Qed.
-- 
GitLab