From 89129662006f7cee0fde9d7beb56a19e8753f8aa Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 27 Sep 2017 16:08:00 +0200
Subject: [PATCH] strengthen qp_eq_loc; add a test

---
 _CoqProject               |  1 +
 theories/lang/lib/tests.v | 18 ++++++++++++++++++
 theories/lang/lifting.v   | 27 +++++++++++++++------------
 3 files changed, 34 insertions(+), 12 deletions(-)
 create mode 100644 theories/lang/lib/tests.v

diff --git a/_CoqProject b/_CoqProject
index c447a2bc..34b5eeb8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -27,6 +27,7 @@ theories/lang/lib/new_delete.v
 theories/lang/lib/spawn.v
 theories/lang/lib/lock.v
 theories/lang/lib/arc.v
+theories/lang/lib/tests.v
 theories/typing/base.v
 theories/typing/type.v
 theories/typing/util.v
diff --git a/theories/lang/lib/tests.v b/theories/lang/lib/tests.v
new file mode 100644
index 00000000..135f2fe7
--- /dev/null
+++ b/theories/lang/lib/tests.v
@@ -0,0 +1,18 @@
+From iris.program_logic Require Import weakestpre.
+From iris.proofmode Require Import tactics.
+From lrust.lang Require Import lang proofmode notation.
+Set Default Proof Using "Type".
+
+Section tests.
+  Context `{!lrustG Σ}.
+
+  Lemma test_location_cmp E (l1 l2 : loc) q1 q2 v1 v2 :
+    {{{ ▷ l1 ↦{q1} v1 ∗ ▷ l2 ↦{q2} v2 }}}
+      #l1 = #l2 @ E
+    {{{ (b: bool), RET LitV (lit_of_bool b); (if b then ⌜l1 = l2⌝ else ⌜l1 ≠ l2⌝) ∗
+                                     l1 ↦{q1} v1 ∗ l2 ↦{q2} v2 }}}.
+  Proof.
+    iIntros (Φ) "[Hl1 Hl2] HΦ". wp_op; try (by eauto); [|];
+      intros ?; iApply "HΦ"; by iFrame.
+  Qed.
+End tests.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 436cdcaf..40d5c149 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -278,13 +278,13 @@ Proof.
 Qed.
 
 Lemma wp_eq_loc E (l1 : loc) (l2: loc) P Φ :
+  (P -∗ ∃ q v, ▷ l1 ↦{q} v) →
+  (P -∗ ∃ q v, ▷ l2 ↦{q} v) →
   (l1 = l2 → P -∗ ▷ Φ (LitV true)) →
   (l1 ≠ l2 → P -∗ ▷ Φ (LitV false)) →
-  (P -∗ ∃ q v, l1 ↦{q} v) →
-  (P -∗ ∃ q v, l2 ↦{q} v) →
   P -∗ WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.
 Proof.
-  iIntros (Heq Hne Hl1 Hl2) "HP".
+  iIntros (Hl1 Hl2 Heq Hne) "HP".
   destruct (bool_decide_reflect (l1 = l2)).
   - rewrite Heq // {Heq Hne}. iApply wp_bin_op_pure; subst.
     + intros. apply BinOpEqTrue. constructor.
@@ -294,23 +294,26 @@ Proof.
     iSplitR.
     { iPureIntro. eexists _, _, _. constructor. apply BinOpEqFalse. by auto. }
     (* We need to do a little gymnastics here to apply Hne now and strip away a
-       â–· but also keep the P. *)
-    iAssert (P ∧ ▷ Φ (LitV false))%I with "[HP]" as "HP".
-    { iSplit; first done. by iApply Hne. }
-    iNext.
+       ▷ but also have the ↦s. *)
+    iAssert ((▷ ∃ q v, l1 ↦{q} v) ∧ (▷ ∃ q v, l2 ↦{q} v) ∧ ▷ Φ (LitV false))%I with "[HP]" as "HP".
+    { iSplit; last iSplit.
+      - iDestruct (Hl1 with "HP") as (??) "?". iNext. eauto.
+      - iDestruct (Hl2 with "HP") as (??) "?". iNext. eauto.
+      - by iApply Hne. }
+    clear Hne Hl1 Hl2. iNext.
     iIntros (e2 σ2 efs Hs) "!>".
     inv_head_step. iSplitR=>//.
     match goal with [ H : bin_op_eval _ _ _ _ _ |- _ ] => inversion H end;
       inv_lit=>//.
-    * iExFalso. iDestruct "HP" as "[HP _]".
-      iDestruct (Hl1 with "HP") as (??) "Hl1".
+    * iExFalso. iDestruct "HP" as "[Hl1 _]".
+      iDestruct "Hl1" as (??) "Hl1".
       iDestruct (heap_read σ2 with "Hσ1 Hl1") as (n') "%".
       simplify_eq.
-    * iExFalso. iDestruct "HP" as "[HP _]".
-      iDestruct (Hl2 with "HP") as (??) "Hl2".
+    * iExFalso. iDestruct "HP" as "[_ [Hl2 _]]".
+      iDestruct "Hl2" as (??) "Hl2".
       iDestruct (heap_read σ2 with "Hσ1 Hl2") as (n') "%".
       simplify_eq.
-    * iDestruct "HP" as "[_ $]". done.
+    * iDestruct "HP" as "[_ [_ $]]". done.
 Qed.
 
 Lemma wp_eq_loc_0_r E (l : loc) P Φ :
-- 
GitLab