Merge branch 'mapsto_ne' into 'master'

Add mapsto_ne helper lemma

See merge request !417

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`):

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.