From 2e475e4638b9543e71ed2feb7c6921eddfe12ddc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 20 Dec 2015 18:12:14 +0100
Subject: [PATCH] Separation type class for singleton maps.

---
 theories/base.v        |  5 +++
 theories/fin_map_dom.v |  9 ++---
 theories/fin_maps.v    | 80 ++++++++++++++++++++----------------------
 theories/hashset.v     |  2 +-
 theories/mapset.v      |  2 +-
 5 files changed, 49 insertions(+), 49 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 8e7817bc..a81acf17 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -468,6 +468,11 @@ Notation "( m !!)" := (λ i, m !! i) (only parsing) : C_scope.
 Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
 Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
 
+(** The singleton map *)
+Class SingletonM K A M := singletonM: K → A → M.
+Instance: Params (@singletonM) 5.
+Notation "{[ x ↦ y ]}" := (singletonM x y) (at level 1) : C_scope.
+
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
 Class Insert (K A M : Type) := insert: K → A → M → M.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index f69fabec..6d6836a8 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -61,11 +61,8 @@ Proof. rewrite (dom_insert _). solve_elem_of. Qed.
 Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
   X ⊆ dom D m → X ⊆ dom D (<[i:=x]>m).
 Proof. intros. transitivity (dom D m); eauto using dom_insert_subseteq. Qed.
-Lemma dom_singleton {A} (i : K) (x : A) : dom D {[(i, x)]} ≡ {[ i ]}.
-Proof.
-  unfold singleton at 1, map_singleton.
-  rewrite dom_insert, dom_empty. solve_elem_of.
-Qed.
+Lemma dom_singleton {A} (i : K) (x : A) : dom D {[i ↦ x]} ≡ {[ i ]}.
+Proof. rewrite <-insert_empty, dom_insert, dom_empty; solve_elem_of. Qed.
 Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}.
 Proof.
   apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
@@ -121,7 +118,7 @@ Lemma dom_alter_L {A} f (m : M A) i : dom D (alter f i m) = dom D m.
 Proof. unfold_leibniz; apply dom_alter. Qed.
 Lemma dom_insert_L {A} (m : M A) i x : dom D (<[i:=x]>m) = {[ i ]} ∪ dom D m.
 Proof. unfold_leibniz; apply dom_insert. Qed.
-Lemma dom_singleton_L {A} (i : K) (x : A) : dom D {[(i, x)]} = {[ i ]}.
+Lemma dom_singleton_L {A} (i : K) (x : A) : dom D {[i ↦ x]} = {[ i ]}.
 Proof. unfold_leibniz; apply dom_singleton. Qed.
 Lemma dom_delete_L {A} (m : M A) i : dom D (delete i m) = dom D m ∖ {[ i ]}.
 Proof. unfold_leibniz; apply dom_delete. Qed.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 46646c7d..791ef2d3 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -56,7 +56,7 @@ Instance map_alter `{PartialAlter K A M} : Alter K A M :=
 Instance map_delete `{PartialAlter K A M} : Delete K M :=
   partial_alter (λ _, None).
 Instance map_singleton `{PartialAlter K A M, Empty M} :
-  Singleton (K * A) M := λ p, <[p.1:=p.2]> ∅.
+  SingletonM K A M := λ i x, <[i:=x]> ∅.
 
 Definition map_of_list `{Insert K A M, Empty M} : list (K * A) → M :=
   fold_right (λ p, <[p.1:=p.2]>) ∅.
@@ -138,6 +138,9 @@ Section setoid.
   Global Instance insert_proper (i : K) :
     Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=M A) i).
   Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
+  Global Instance singleton_proper k :
+    Proper ((≡) ==> (≡)) (singletonM k : A → M A).
+  Proof. by intros ???; apply insert_proper. Qed.
   Global Instance delete_proper (i : K) :
     Proper ((≡) ==> (≡)) (delete (M:=M A) i).
   Proof. by apply partial_alter_proper; [constructor|]. Qed.
@@ -340,7 +343,7 @@ Proof.
 Qed.
 Lemma delete_empty {A} i : delete i (∅ : M A) = ∅.
 Proof. rewrite <-(partial_alter_self ∅) at 2. by rewrite lookup_empty. Qed.
-Lemma delete_singleton {A} i (x : A) : delete i {[i, x]} = ∅.
+Lemma delete_singleton {A} i (x : A) : delete i {[i ↦ x]} = ∅.
 Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
 Lemma delete_commute {A} (m : M A) i j :
   delete i (delete j m) = delete j (delete i m).
@@ -476,43 +479,39 @@ Proof.
   * by rewrite lookup_fmap, !lookup_insert.
   * by rewrite lookup_fmap, !lookup_insert_ne, lookup_fmap by done.
 Qed.
-Lemma insert_empty {A} i (x : A) : <[i:=x]>∅ = {[i,x]}.
+Lemma insert_empty {A} i (x : A) : <[i:=x]>∅ = {[i ↦ x]}.
 Proof. done. Qed.
 
 (** ** Properties of the singleton maps *)
 Lemma lookup_singleton_Some {A} i j (x y : A) :
-  {[i, x]} !! j = Some y ↔ i = j ∧ x = y.
+  {[i ↦ x]} !! j = Some y ↔ i = j ∧ x = y.
 Proof.
-  unfold singleton, map_singleton.
-  rewrite lookup_insert_Some, lookup_empty. simpl. intuition congruence.
+  rewrite <-insert_empty,lookup_insert_Some, lookup_empty; intuition congruence.
 Qed.
-Lemma lookup_singleton_None {A} i j (x : A) : {[i, x]} !! j = None ↔ i ≠ j.
-Proof.
-  unfold singleton, map_singleton.
-  rewrite lookup_insert_None, lookup_empty. simpl. tauto.
-Qed.
-Lemma lookup_singleton {A} i (x : A) : {[i, x]} !! i = Some x.
+Lemma lookup_singleton_None {A} i j (x : A) : {[i ↦ x]} !! j = None ↔ i ≠ j.
+Proof. rewrite <-insert_empty,lookup_insert_None, lookup_empty; tauto. Qed.
+Lemma lookup_singleton {A} i (x : A) : {[i ↦ x]} !! i = Some x.
 Proof. by rewrite lookup_singleton_Some. Qed.
-Lemma lookup_singleton_ne {A} i j (x : A) : i ≠ j → {[i, x]} !! j = None.
+Lemma lookup_singleton_ne {A} i j (x : A) : i ≠ j → {[i ↦ x]} !! j = None.
 Proof. by rewrite lookup_singleton_None. Qed.
-Lemma map_non_empty_singleton {A} i (x : A) : {[i,x]} ≠ ∅.
+Lemma map_non_empty_singleton {A} i (x : A) : {[i ↦ x]} ≠ ∅.
 Proof.
   intros Hix. apply (f_equal (!! i)) in Hix.
   by rewrite lookup_empty, lookup_singleton in Hix.
 Qed.
-Lemma insert_singleton {A} i (x y : A) : <[i:=y]>{[i, x]} = {[i, y]}.
+Lemma insert_singleton {A} i (x y : A) : <[i:=y]>{[i ↦ x]} = {[i ↦ y]}.
 Proof.
-  unfold singleton, map_singleton, insert, map_insert.
+  unfold singletonM, map_singleton, insert, map_insert.
   by rewrite <-partial_alter_compose.
 Qed.
-Lemma alter_singleton {A} (f : A → A) i x : alter f i {[i,x]} = {[i, f x]}.
+Lemma alter_singleton {A} (f : A → A) i x : alter f i {[i ↦ x]} = {[i ↦ f x]}.
 Proof.
   intros. apply map_eq. intros i'. destruct (decide (i = i')) as [->|?].
   * by rewrite lookup_alter, !lookup_singleton.
   * by rewrite lookup_alter_ne, !lookup_singleton_ne.
 Qed.
 Lemma alter_singleton_ne {A} (f : A → A) i j x :
-  i ≠ j → alter f i {[j,x]} = {[j,x]}.
+  i ≠ j → alter f i {[j ↦ x]} = {[j ↦ x]}.
 Proof.
   intros. apply map_eq; intros i'. by destruct (decide (i = i')) as [->|?];
     rewrite ?lookup_alter, ?lookup_singleton_ne, ?lookup_alter_ne by done.
@@ -524,7 +523,7 @@ Proof. apply map_empty; intros i. by rewrite lookup_fmap, lookup_empty. Qed.
 Lemma omap_empty {A B} (f : A → option B) : omap f ∅ = ∅.
 Proof. apply map_empty; intros i. by rewrite lookup_omap, lookup_empty. Qed.
 Lemma omap_singleton {A B} (f : A → option B) i x y :
-  f x = Some y → omap f {[ i,x ]} = {[ i,y ]}.
+  f x = Some y → omap f {[ i ↦ x ]} = {[ i ↦ y ]}.
 Proof.
   intros; apply map_eq; intros j; destruct (decide (i = j)) as [->|].
   * by rewrite lookup_omap, !lookup_singleton.
@@ -874,10 +873,9 @@ Lemma insert_merge m1 m2 i x y z :
   <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) (<[i:=z]>m2).
 Proof. by intros; apply partial_alter_merge. Qed.
 Lemma merge_singleton i x y z :
-  f (Some y) (Some z) = Some x → merge f {[i,y]} {[i,z]} = {[i,x]}.
+  f (Some y) (Some z) = Some x → merge f {[i ↦ y]} {[i ↦ z]} = {[i ↦ x]}.
 Proof.
-  intros. unfold singleton, map_singleton; simpl.
-  by erewrite <-insert_merge, merge_empty by eauto.
+  intros. by erewrite <-!insert_empty, <-insert_merge, merge_empty by eauto.
 Qed.
 Lemma insert_merge_l m1 m2 i x y :
   f (Some y) (m2 !! i) = Some x →
@@ -977,23 +975,23 @@ Proof. rewrite map_disjoint_spec, eq_None_not_Some. intros ?? [??]; eauto. Qed.
 Lemma map_disjoint_Some_r {A} (m1 m2 : M A) i x:
   m1 ⊥ₘ m2 → m2 !! i = Some x → m1 !! i = None.
 Proof. rewrite (symmetry_iff map_disjoint). apply map_disjoint_Some_l. Qed.
-Lemma map_disjoint_singleton_l {A} (m: M A) i x : {[i, x]} ⊥ₘ m ↔ m !! i = None.
+Lemma map_disjoint_singleton_l {A} (m: M A) i x : {[i↦x]} ⊥ₘ m ↔ m !! i = None.
 Proof.
   split; [|rewrite !map_disjoint_spec].
-  * intro. apply (map_disjoint_Some_l {[i, x]} _ _ x);
+  * intro. apply (map_disjoint_Some_l {[i ↦ x]} _ _ x);
       auto using lookup_singleton.
   * intros ? j y1 y2. destruct (decide (i = j)) as [->|].
     + rewrite lookup_singleton. intuition congruence.
     + by rewrite lookup_singleton_ne.
 Qed.
 Lemma map_disjoint_singleton_r {A} (m : M A) i x :
-  m ⊥ₘ {[i, x]} ↔ m !! i = None.
+  m ⊥ₘ {[i ↦ x]} ↔ m !! i = None.
 Proof. by rewrite (symmetry_iff map_disjoint), map_disjoint_singleton_l. Qed.
 Lemma map_disjoint_singleton_l_2 {A} (m : M A) i x :
-  m !! i = None → {[i, x]} ⊥ₘ m.
+  m !! i = None → {[i ↦ x]} ⊥ₘ m.
 Proof. by rewrite map_disjoint_singleton_l. Qed.
 Lemma map_disjoint_singleton_r_2 {A} (m : M A) i x :
-  m !! i = None → m ⊥ₘ {[i, x]}.
+  m !! i = None → m ⊥ₘ {[i ↦ x]}.
 Proof. by rewrite map_disjoint_singleton_r. Qed.
 Lemma map_disjoint_delete_l {A} (m1 m2 : M A) i : m1 ⊥ₘ m2 → delete i m1 ⊥ₘ m2.
 Proof.
@@ -1210,7 +1208,7 @@ Proof. by rewrite map_disjoint_union_l. Qed.
 Lemma map_disjoint_union_r_2 {A} (m1 m2 m3 : M A) :
   m1 ⊥ₘ m2 → m1 ⊥ₘ m3 → m1 ⊥ₘ m2 ∪ m3.
 Proof. by rewrite map_disjoint_union_r. Qed.
-Lemma insert_union_singleton_l {A} (m : M A) i x : <[i:=x]>m = {[i,x]} ∪ m.
+Lemma insert_union_singleton_l {A} (m : M A) i x : <[i:=x]>m = {[i ↦ x]} ∪ m.
 Proof.
   apply map_eq. intros j. apply option_eq. intros y.
   rewrite lookup_union_Some_raw.
@@ -1219,7 +1217,7 @@ Proof.
   * rewrite !lookup_singleton_ne, lookup_insert_ne; intuition congruence.
 Qed.
 Lemma insert_union_singleton_r {A} (m : M A) i x :
-  m !! i = None → <[i:=x]>m = m ∪ {[i,x]}.
+  m !! i = None → <[i:=x]>m = m ∪ {[i ↦ x]}.
 Proof.
   intro. rewrite insert_union_singleton_l, map_union_commutative; [done |].
   by apply map_disjoint_singleton_l.
@@ -1423,15 +1421,15 @@ End theorems.
 (** * Tactics *)
 (** The tactic [decompose_map_disjoint] simplifies occurrences of [disjoint]
 in the hypotheses that involve the empty map [∅], the union [(∪)] or insert
-[<[_:=_]>] operation, the singleton [{[ _ ]}] map, and disjointness of lists of
+[<[_:=_]>] operation, the singleton [{[_↦ _]}] map, and disjointness of lists of
 maps. This tactic does not yield any information loss as all simplifications
 performed are reversible. *)
 Ltac decompose_map_disjoint := repeat
   match goal with
   | H : _ ∪ _ ⊥ₘ _ |- _ => apply map_disjoint_union_l in H; destruct H
   | H : _ ⊥ₘ _ ∪ _ |- _ => apply map_disjoint_union_r in H; destruct H
-  | H : {[ _ ]} ⊥ₘ _ |- _ => apply map_disjoint_singleton_l in H
-  | H : _ ⊥ₘ {[ _ ]} |- _ =>  apply map_disjoint_singleton_r in H
+  | H : {[ _ ↦ _ ]} ⊥ₘ _ |- _ => apply map_disjoint_singleton_l in H
+  | H : _ ⊥ₘ {[ _ ↦ _ ]} |- _ =>  apply map_disjoint_singleton_r in H
   | H : <[_:=_]>_ ⊥ₘ _ |- _ => apply map_disjoint_insert_l in H; destruct H
   | H : _ ⊥ₘ <[_:=_]>_ |- _ => apply map_disjoint_insert_r in H; destruct H
   | H : ⋃ _ ⊥ₘ _ |- _ => apply map_disjoint_union_list_l in H
@@ -1455,9 +1453,9 @@ Ltac solve_map_disjoint :=
 Hint Extern 1 (_ ⊥ₘ _) => done : map_disjoint.
 Hint Extern 2 (∅ ⊥ₘ _) => apply map_disjoint_empty_l : map_disjoint.
 Hint Extern 2 (_ ⊥ₘ ∅) => apply map_disjoint_empty_r : map_disjoint.
-Hint Extern 2 ({[ _ ]} ⊥ₘ _) =>
+Hint Extern 2 ({[ _ ↦ _ ]} ⊥ₘ _) =>
   apply map_disjoint_singleton_l_2 : map_disjoint.
-Hint Extern 2 (_ ⊥ₘ {[ _ ]}) =>
+Hint Extern 2 (_ ⊥ₘ {[ _ ↦ _ ]}) =>
   apply map_disjoint_singleton_r_2 : map_disjoint.
 Hint Extern 2 (_ ∪ _ ⊥ₘ _) => apply map_disjoint_union_l_2 : map_disjoint.
 Hint Extern 2 (_ ⊥ₘ _ ∪ _) => apply map_disjoint_union_r_2 : map_disjoint.
@@ -1489,7 +1487,7 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
     rewrite lookup_alter in H || rewrite lookup_alter_ne in H by tac
   | H : context[ (delete _ _) !! _] |- _ =>
     rewrite lookup_delete in H || rewrite lookup_delete_ne in H by tac
-  | H : context[ {[ _ ]} !! _ ] |- _ =>
+  | H : context[ {[ _ ↦ _ ]} !! _ ] |- _ =>
     rewrite lookup_singleton in H || rewrite lookup_singleton_ne in H by tac
   | H : context[ (_ <$> _) !! _ ] |- _ => rewrite lookup_fmap in H
   | H : context[ (omap _ _) !! _ ] |- _ => rewrite lookup_omap in H
@@ -1506,7 +1504,7 @@ Tactic Notation "simpl_map" "by" tactic3(tac) := repeat
     rewrite lookup_alter || rewrite lookup_alter_ne by tac
   | |- context[ (delete _ _) !! _ ] =>
     rewrite lookup_delete || rewrite lookup_delete_ne by tac
-  | |- context[ {[ _ ]} !! _ ] =>
+  | |- context[ {[ _ ↦ _ ]} !! _ ] =>
     rewrite lookup_singleton || rewrite lookup_singleton_ne by tac
   | |- context[ (_ <$> _) !! _ ] => rewrite lookup_fmap
   | |- context[ (omap _ _) !! _ ] => rewrite lookup_omap
@@ -1523,7 +1521,7 @@ Tactic Notation "simpl_map" := simpl_map by eauto with simpl_map map_disjoint.
 
 Hint Extern 80 ((_ ∪ _) !! _ = Some _) => apply lookup_union_Some_l : simpl_map.
 Hint Extern 81 ((_ ∪ _) !! _ = Some _) => apply lookup_union_Some_r : simpl_map.
-Hint Extern 80 ({[ _ ]} !! _ = Some _) => apply lookup_singleton : simpl_map.
+Hint Extern 80 ({[ _↦_ ]} !! _ = Some _) => apply lookup_singleton : simpl_map.
 Hint Extern 80 (<[_:=_]> _ !! _ = Some _) => apply lookup_insert : simpl_map.
 
 (** Now we take everything together and also discharge conflicting look ups,
@@ -1535,8 +1533,8 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
   | _ => progress simpl_map by tac
   | _ => progress simplify_equality
   | _ => progress simpl_option_monad by tac
-  | H : {[ _ ]} !! _ = None |- _ => rewrite lookup_singleton_None in H
-  | H : {[ _ ]} !! _ = Some _ |- _ =>
+  | H : {[ _ ↦ _ ]} !! _ = None |- _ => rewrite lookup_singleton_None in H
+  | H : {[ _ ↦ _ ]} !! _ = Some _ |- _ =>
     rewrite lookup_singleton_Some in H; destruct H
   | H1 : ?m1 !! ?i = Some ?x, H2 : ?m2 !! ?i = Some ?y |- _ =>
     let H3 := fresh in
@@ -1549,8 +1547,8 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
     apply map_union_cancel_l in H; [|by tac|by tac]
   | H : _ ∪ ?m = _ ∪ ?m |- _ =>
     apply map_union_cancel_r in H; [|by tac|by tac]
-  | H : {[?i,?x]} = ∅ |- _ => by destruct (map_non_empty_singleton i x)
-  | H : ∅ = {[?i,?x]} |- _ => by destruct (map_non_empty_singleton i x)
+  | H : {[?i ↦ ?x]} = ∅ |- _ => by destruct (map_non_empty_singleton i x)
+  | H : ∅ = {[?i ↦ ?x]} |- _ => by destruct (map_non_empty_singleton i x)
   | H : ?m !! ?i = Some _, H2 : ?m !! ?j = None |- _ =>
      unless (i ≠ j) by done;
      assert (i ≠ j) by (by intros ?; simplify_equality)
diff --git a/theories/hashset.v b/theories/hashset.v
index f517f0e7..d01bf1b8 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -23,7 +23,7 @@ Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, ∃ l,
 Program Instance hashset_empty: Empty (hashset hash) := Hashset ∅ _.
 Next Obligation. by intros n X; simpl_map. Qed.
 Program Instance hashset_singleton: Singleton A (hashset hash) := λ x,
-  Hashset {[ hash x, [x] ]} _.
+  Hashset {[ hash x ↦ [x] ]} _.
 Next Obligation.
   intros n l. rewrite lookup_singleton_Some. intros [<- <-].
   rewrite Forall_singleton; auto using NoDup_singleton.
diff --git a/theories/mapset.v b/theories/mapset.v
index 586a099a..317b6fc7 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -17,7 +17,7 @@ Instance mapset_elem_of: ElemOf K (mapset M) := λ x X,
   mapset_car X !! x = Some ().
 Instance mapset_empty: Empty (mapset M) := Mapset ∅.
 Instance mapset_singleton: Singleton K (mapset M) := λ x,
-  Mapset {[ (x,()) ]}.
+  Mapset {[ x ↦ () ]}.
 Instance mapset_union: Union (mapset M) := λ X1 X2,
   let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∪ m2).
 Instance mapset_intersection: Intersection (mapset M) := λ X1 X2,
-- 
GitLab