From 1c4b98889f116463074c8b74616676c77ef5ba1d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 22 Feb 2016 20:28:44 +0100
Subject: [PATCH] add notation for ndot

---
 barrier/client.v           |  2 +-
 program_logic/namespaces.v | 17 ++++++++++-------
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/barrier/client.v b/barrier/client.v
index 89ed8f4ff..d6717de0a 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -38,7 +38,7 @@ Section ClosedProofs.
     { (* FIXME Really?? set_solver takes forever on "⊆ ⊤"?!? *)
       move=>? _. exact I. }
     apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
-    rewrite -(client_safe (ndot nroot "Heap" ) (ndot nroot "Barrier" )) //.
+    rewrite -(client_safe (nroot .: "Heap" ) (nroot .: "Barrier" )) //.
     (* This, too, should be automated. *)
     apply ndot_ne_disjoint. discriminate.
   Qed.
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 78d7cdf40..84ed58a5e 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -7,19 +7,22 @@ Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
   encode x :: N.
 Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
 
+Infix ".:" := ndot (at level 19, left associativity) : C_scope.
+Notation "(.:)" := ndot : C_scope.
+
 Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
 Proof. by intros N1 x1 N2 x2 ?; simplify_eq. Qed.
 Lemma nclose_nroot : nclose nroot = ⊤.
 Proof. by apply (sig_eq_pi _). Qed.
 Lemma encode_nclose N : encode N ∈ nclose N.
 Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.
-Lemma nclose_subseteq `{Countable A} N x : nclose (ndot N x) ⊆ nclose N.
+Lemma nclose_subseteq `{Countable A} N x : nclose (N .: x) ⊆ nclose N.
 Proof.
   intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
-  destruct (list_encode_suffix N (ndot N x)) as [q' ?]; [by exists [encode x]|].
+  destruct (list_encode_suffix N (N .: x)) as [q' ?]; [by exists [encode x]|].
   by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
 Qed.
-Lemma ndot_nclose `{Countable A} N x : encode (ndot N x) ∈ nclose N.
+Lemma ndot_nclose `{Countable A} N x : encode (N .: x) ∈ nclose N.
 Proof. apply nclose_subseteq with x, encode_nclose. Qed.
 
 Instance ndisjoint : Disjoint namespace := λ N1 N2,
@@ -33,16 +36,16 @@ Section ndisjoint.
   Global Instance ndisjoint_comm : Comm iff ndisjoint.
   Proof. intros N1 N2. rewrite /disjoint /ndisjoint; naive_solver. Qed.
 
-  Lemma ndot_ne_disjoint N (x y : A) : x ≠ y → ndot N x ⊥ ndot N y.
-  Proof. intros Hxy. exists (ndot N x), (ndot N y); naive_solver. Qed.
+  Lemma ndot_ne_disjoint N (x y : A) : x ≠ y → N .: x ⊥ N .: y.
+  Proof. intros Hxy. exists (N .: x), (N .: y); naive_solver. Qed.
 
-  Lemma ndot_preserve_disjoint_l N1 N2 x : N1 ⊥ N2 → ndot N1 x ⊥ N2.
+  Lemma ndot_preserve_disjoint_l N1 N2 x : N1 ⊥ N2 → N1 .: x ⊥ N2.
   Proof.
     intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
     split_and?; try done; []. by apply suffix_of_cons_r.
   Qed.
 
-  Lemma ndot_preserve_disjoint_r N1 N2 x : N1 ⊥ N2 → N1 ⊥ ndot N2 x .
+  Lemma ndot_preserve_disjoint_r N1 N2 x : N1 ⊥ N2 → N1 ⊥ N2 .: x .
   Proof. rewrite ![N1 ⊥ _]comm. apply ndot_preserve_disjoint_l. Qed.
 
   Lemma ndisj_disjoint N1 N2 : N1 ⊥ N2 → nclose N1 ∩ nclose N2 = ∅.
-- 
GitLab