From 4cd21e6289cfdbb6c808a2c106235da23d181616 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 3 Nov 2020 17:29:10 +0100
Subject: [PATCH] forgot to propagate gen_heap / gen_inv_heap changes to
 heap_lang

---
 tests/heap_lang.ref                 |  2 +-
 tests/heap_lang.v                   | 16 ++--------------
 theories/heap_lang/primitive_laws.v | 22 ++++------------------
 3 files changed, 7 insertions(+), 33 deletions(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 4a40a842e..a3530755c 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -121,7 +121,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   I : val → Prop
   Heq : ∀ v : val, I v ↔ I #true
   ============================
-  ⊢ l ↦□ (λ _ : val, I #true)
+  ⊢ l ↦_(λ _ : val, I #true) □
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 68bfa9ab2..421093021 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -234,29 +234,17 @@ Section tests.
   Qed.
 End tests.
 
-Section mapsto_tests.
-  Context `{!heapG Σ}.
-
-  (* Make sure certain tactic sequences can solve certain goals. *)
-  Lemma mapsto_combine l v :
-    l ↦{1/2} - ∗ l ↦{1/2} v -∗ l ↦ -.
-  Proof.
-    iIntros "[Hl1 Hl2]". iFrame. iExists _. done.
-  Qed.
-
-End mapsto_tests.
-
 Section inv_mapsto_tests.
   Context `{!heapG Σ}.
 
   (* Make sure these parse and type-check. *)
   Lemma inv_mapsto_own_test (l : loc) : ⊢ l ↦_(λ _, True) #5. Abort.
-  Lemma inv_mapsto_test (l : loc) : ⊢ l ↦□ (λ _, True). Abort.
+  Lemma inv_mapsto_test (l : loc) : ⊢ l ↦_(λ _, True) □. Abort.
 
   (* Make sure [setoid_rewrite] works. *)
   Lemma inv_mapsto_setoid_rewrite (l : loc) (I : val → Prop) :
     (∀ v, I v ↔ I #true) →
-    ⊢ l ↦□ (λ v, I v).
+    ⊢ l ↦_(λ v, I v) □.
   Proof.
     iIntros (Heq). setoid_rewrite Heq. Show.
   Abort.
diff --git a/theories/heap_lang/primitive_laws.v b/theories/heap_lang/primitive_laws.v
index 2de2bcbcf..8d50d9d91 100644
--- a/theories/heap_lang/primitive_laws.v
+++ b/theories/heap_lang/primitive_laws.v
@@ -32,9 +32,6 @@ Notation "l ↦{ q } v" := (mapsto (L:=loc) (V:=option val) l q (Some v%V))
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
 Notation "l ↦ v" := (mapsto (L:=loc) (V:=option val) l 1%Qp (Some v%V))
   (at level 20) : bi_scope.
-Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
-  (at level 20, q at level 50, format "l  ↦{ q }  -") : bi_scope.
-Notation "l ↦ -" := (l ↦{1} -)%I (at level 20) : bi_scope.
 
 (** Same for [gen_inv_heap], except that these are higher-order notations so to
 make setoid rewriting in the predicate [I] work we need actual definitions
@@ -51,8 +48,8 @@ Instance: Params (@inv_mapsto_own) 4 := {}.
 Instance: Params (@inv_mapsto) 3 := {}.
 
 Notation inv_heap_inv := (inv_heap_inv loc (option val)).
-Notation "l ↦□ I" := (inv_mapsto l I%stdpp%type)
-  (at level 20, format "l  ↦□  I") : bi_scope.
+Notation "l '↦_' I □" := (inv_mapsto l I%stdpp%type)
+  (at level 20, I at level 9, format "l  '↦_' I  '□'") : bi_scope.
 Notation "l ↦_ I v" := (inv_mapsto_own l v I%stdpp%type)
   (at level 20, I at level 9, format "l  ↦_ I  v") : bi_scope.
 
@@ -280,17 +277,6 @@ Qed.
 (** We need to adjust the [gen_heap] and [gen_inv_heap] lemmas because of our
 value type being [option val]. *)
 
-Global Instance ex_mapsto_fractional l : Fractional (λ q, l ↦{q} -)%I.
-Proof.
-  intros p q. iSplit.
-  - iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
-  - iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
-    iDestruct (mapsto_agree with "H1 H2") as %->. iExists v2. by iFrame.
-Qed.
-Global Instance ex_mapsto_as_fractional l q :
-  AsFractional (l ↦{q} -) (λ q, l ↦{q} -)%I q.
-Proof. split. done. apply _. Qed.
-
 Lemma mapsto_valid_2 l q1 q2 v1 v2 :
   l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜✓ (q1 + q2)%Qp ∧ v1 = v2⌝.
 Proof.
@@ -331,7 +317,7 @@ Lemma make_inv_mapsto l v (I : val → Prop) E :
   I v →
   inv_heap_inv -∗ l ↦ v ={E}=∗ l ↦_I v.
 Proof. iIntros (??) "#HI Hl". iApply make_inv_mapsto; done. Qed.
-Lemma inv_mapsto_own_inv l v I : l ↦_I v -∗ l ↦□ I.
+Lemma inv_mapsto_own_inv l v I : l ↦_I v -∗ l ↦_I □.
 Proof. apply inv_mapsto_own_inv. Qed.
 
 Lemma inv_mapsto_own_acc_strong E :
@@ -358,7 +344,7 @@ Qed.
 
 Lemma inv_mapsto_acc l I E :
   ↑inv_heapN ⊆ E →
-  inv_heap_inv -∗ l ↦□ I ={E, E ∖ ↑inv_heapN}=∗
+  inv_heap_inv -∗ l ↦_I □ ={E, E ∖ ↑inv_heapN}=∗
     ∃ v, ⌜I v⌝ ∗ l ↦ v ∗ (l ↦ v ={E ∖ ↑inv_heapN, E}=∗ ⌜True⌝).
 Proof.
   iIntros (?) "#Hinv Hl".
-- 
GitLab