From d3c31b452c742ac5ee59dcdf014b82c9570f19d5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 14 Apr 2020 15:34:46 +0200
Subject: [PATCH] add notation for inv_mapsto(_own)?

---
 tests/heap_lang.v                      |  9 ++++++++
 theories/base_logic/lib/gen_inv_heap.v | 32 +++++++++++++++-----------
 theories/heap_lang/adequacy.v          |  6 ++---
 theories/heap_lang/lifting.v           | 11 ++++++---
 4 files changed, 39 insertions(+), 19 deletions(-)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 6a9e55e54..8d5216079 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,3 +1,4 @@
+From iris.base_logic.lib Require Import gen_inv_heap.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
 (* Import lang *again*. This used to break notation. *)
@@ -202,6 +203,14 @@ Section tests.
 
 End tests.
 
+Section notation_tests.
+  Context `{!heapG Σ, inv_heapG loc val Σ}.
+
+  (* Make sure these parse and type-check. *)
+  Lemma inv_mapsto_own_test (l : loc) : ⊢ l ↦@ #5 □ (λ _, True). Abort.
+  Lemma inv_mapsto_test (l : loc) : ⊢ l ↦□ (λ _, True). Abort.
+End notation_tests.
+
 Section printing_tests.
   Context `{!heapG Σ}.
 
diff --git a/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v
index 02843da24..f5c4faeaa 100644
--- a/theories/base_logic/lib/gen_inv_heap.v
+++ b/theories/base_logic/lib/gen_inv_heap.v
@@ -49,7 +49,7 @@ Instance subG_inv_heapPreG (L V : Type) `{Countable L} {Σ} :
   subG (inv_heapΣ L V) Σ → inv_heapPreG L V Σ.
 Proof. solve_inG. Qed.
 
-Section defs.
+Section definitions.
   Context {L V : Type} `{Countable L}.
   Context `{!invG Σ, !gen_heapG L V Σ, gG: !inv_heapG L V Σ}.
 
@@ -66,7 +66,13 @@ Section defs.
   Definition inv_mapsto (l : L) (I : V → Prop) : iProp Σ :=
     own (inv_heap_name gG) (â—¯ {[l := (None, to_agree I)]}).
 
-End defs.
+End definitions.
+
+Local Notation "l ↦□ I" := (inv_mapsto l I%stdpp%type)
+  (at level 20, format "l  ↦□  I") : bi_scope.
+
+Local Notation "l ↦@ v □ I" := (inv_mapsto_own l v I%stdpp%type)
+  (at level 20, format "l  ↦@  v  □  I") : bi_scope.
 
 (* [inv_heap_inv] has no parameters to infer the types from, so we need to
    make them explicit. *)
@@ -128,7 +134,7 @@ Section inv_heap.
   (** * Helpers *)
 
   Lemma inv_mapsto_lookup_Some l h I :
-    inv_mapsto l I -∗ own (inv_heap_name gG) (● to_inv_heap h) -∗
+    l ↦□ I -∗ own (inv_heap_name gG) (● to_inv_heap h) -∗
     ⌜∃ v I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
   Proof.
     iIntros "Hl_inv Hâ—¯".
@@ -141,7 +147,7 @@ Section inv_heap.
   Qed.
 
   Lemma inv_mapsto_own_lookup_Some l v h I :
-    inv_mapsto_own l v I -∗ own (inv_heap_name gG) (● to_inv_heap h) -∗
+    l ↦@ v □ I -∗ own (inv_heap_name gG) (● to_inv_heap h) -∗
     ⌜ ∃ I', h !! l = Some (v, I') ∧ ∀ w, I w ↔ I' w ⌝.
   Proof.
     iIntros "Hl_inv H●".
@@ -171,13 +177,13 @@ Section inv_heap.
     apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
   Qed.
 
-  Global Instance inv_mapsto_persistent l I : Persistent (inv_mapsto l I).
+  Global Instance inv_mapsto_persistent l I : Persistent (l ↦□ I).
   Proof. rewrite /inv_mapsto. apply _. Qed.
 
-  Global Instance inv_mapsto_timeless l I : Timeless (inv_mapsto l I).
+  Global Instance inv_mapsto_timeless l I : Timeless (l ↦□ I).
   Proof. rewrite /inv_mapsto. apply _. Qed.
 
-  Global Instance inv_mapsto_own_timeless l v I : Timeless (inv_mapsto_own l v I).
+  Global Instance inv_mapsto_own_timeless l v I : Timeless (l ↦@ v □ I).
   Proof. rewrite /inv_mapsto. apply _. Qed.
 
   (** * Public lemmas *)
@@ -185,7 +191,7 @@ Section inv_heap.
   Lemma make_inv_mapsto l v I E :
     ↑inv_heapN ⊆ E →
     I v →
-    inv_heap_inv L V -∗ l ↦ v ={E}=∗ inv_mapsto_own l v I.
+    inv_heap_inv L V -∗ l ↦ v ={E}=∗ l ↦@ v □ I.
   Proof.
     iIntros (HN HI) "#Hinv Hl".
     iMod (inv_acc_timeless _ inv_heapN with "Hinv") as "[HP Hclose]"; first done.
@@ -207,7 +213,7 @@ Section inv_heap.
       + iModIntro. by rewrite /inv_mapsto_own to_inv_heap_singleton.
   Qed.
 
-  Lemma inv_mapsto_own_inv l v I : inv_mapsto_own l v I -∗ inv_mapsto l I.
+  Lemma inv_mapsto_own_inv l v I : l ↦@ v □ I -∗ l ↦□ I.
   Proof.
     apply own_mono, auth_frag_mono. rewrite singleton_included pair_included.
     right. split; [apply: ucmra_unit_least|done].
@@ -218,7 +224,7 @@ Section inv_heap.
     this before opening an atomic update that provides [inv_mapsto_own]!. *)
   Lemma inv_mapsto_own_acc_strong E :
     ↑inv_heapN ⊆ E →
-    inv_heap_inv L V ={E, E ∖ ↑inv_heapN}=∗ ∀ l v I, inv_mapsto_own l v I -∗
+    inv_heap_inv L V ={E, E ∖ ↑inv_heapN}=∗ ∀ l v I, l ↦@ v □ I -∗
       (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ==∗
         inv_mapsto_own l w I ∗ |={E ∖ ↑inv_heapN, E}=> True)).
   Proof.
@@ -246,8 +252,8 @@ Section inv_heap.
   (** Derive a more standard accessor. *)
   Lemma inv_mapsto_own_acc E l v I:
     ↑inv_heapN ⊆ E →
-    inv_heap_inv L V -∗ inv_mapsto_own l v I ={E, E ∖ ↑inv_heapN}=∗
-      (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ={E ∖ ↑inv_heapN, E}=∗ inv_mapsto_own l w I)).
+    inv_heap_inv L V -∗ l ↦@ v □ I ={E, E ∖ ↑inv_heapN}=∗
+      (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ={E ∖ ↑inv_heapN, E}=∗ l ↦@ w □ I)).
   Proof.
     iIntros (?) "#Hinv Hl".
     iMod (inv_mapsto_own_acc_strong with "Hinv") as "Hacc"; first done.
@@ -258,7 +264,7 @@ Section inv_heap.
 
   Lemma inv_mapsto_acc l I E :
     ↑inv_heapN ⊆ E →
-    inv_heap_inv L V -∗ inv_mapsto l I ={E, E ∖ ↑inv_heapN}=∗
+    inv_heap_inv L V -∗ l ↦□ I ={E, E ∖ ↑inv_heapN}=∗
     ∃ v, ⌜I v⌝ ∗ l ↦ v ∗ (l ↦ v ={E ∖ ↑inv_heapN, E}=∗ ⌜True⌝).
   Proof.
     iIntros (HN) "#Hinv Hl_inv".
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 2ed93d2c0..d3fc86c70 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -1,6 +1,5 @@
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth.
-From iris.base_logic.lib Require Import proph_map.
 From iris.program_logic Require Export weakestpre adequacy.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
@@ -8,10 +7,11 @@ Set Default Proof Using "Type".
 Class heapPreG Σ := HeapPreG {
   heap_preG_iris :> invPreG Σ;
   heap_preG_heap :> gen_heapPreG loc val Σ;
-  heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ
+  heap_preG_proph :> proph_mapPreG proph_id (val * val) Σ;
 }.
 
-Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id (val * val)].
+Definition heapΣ : gFunctors :=
+  #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_id (val * val)].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. solve_inG. Qed.
 
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 8619893ad..28cf6b2e4 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -1,8 +1,8 @@
 From stdpp Require Import fin_maps.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import auth gmap.
-From iris.base_logic Require Export gen_heap.
-From iris.base_logic.lib Require Export proph_map.
+From iris.base_logic.lib Require Export gen_heap proph_map.
+From iris.base_logic.lib Require Import gen_inv_heap.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
 From iris.heap_lang Require Export lang.
@@ -12,7 +12,7 @@ Set Default Proof Using "Type".
 Class heapG Σ := HeapG {
   heapG_invG : invG Σ;
   heapG_gen_heapG :> gen_heapG loc val Σ;
-  heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ
+  heapG_proph_mapG :> proph_mapG proph_id (val * val) Σ;
 }.
 
 Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
@@ -31,6 +31,11 @@ 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.
 
+Notation "l ↦□ I" := (inv_mapsto (L:=loc) (V:=val) l I%stdpp%type)
+  (at level 20, format "l  ↦□  I") : bi_scope.
+Notation "l ↦@ v □ I" := (inv_mapsto_own (L:=loc) (V:=val) l v I%stdpp%type)
+  (at level 20, format "l  ↦@  v  □  I") : bi_scope.
+
 (** The tactic [inv_head_step] performs inversion on hypotheses of the shape
 [head_step]. The tactic will discharge head-reductions starting from values, and
 simplifies hypothesis related to conversions from and to values, and finite map
-- 
GitLab