From 4bea88d16f0c5e2dd9b1b736fc7fec6530a24514 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 30 Mar 2022 13:40:08 +0200
Subject: [PATCH] Clarify relationship between `gset_to_gmap` and `set_to_map`.

---
 theories/gmap.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/theories/gmap.v b/theories/gmap.v
index 9b49181e..256b05e9 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -286,6 +286,11 @@ Section gset.
   (** If you are looking for a lemma showing that [gset] is extensional, see
   [sets.set_eq]. *)
 
+  (** The function [gset_to_gmap x X] converts a set [X] to a map with domain
+  [X] where each key has value [x]. Compared to the generic conversion
+  [set_to_map], the function [gset_to_gmap] has [O(n)] instead of [O(n log n)]
+  complexity and has an easier and better developed theory. *)
+
   Definition gset_to_gmap {A} (x : A) (X : gset K) : gmap K A :=
     (λ _, x) <$> mapset_car X.
 
@@ -342,6 +347,13 @@ Section gset.
     - rewrite gset_to_gmap_empty, dom_empty_L; done.
     - rewrite gset_to_gmap_union_singleton, dom_insert_L, IH; done.
   Qed.
+
+  Lemma gset_to_gmap_set_to_map {A} (X : gset K) (x : A) :
+    gset_to_gmap x X = set_to_map (.,x) X.
+  Proof.
+    apply map_eq; intros k. apply option_eq; intros y.
+    rewrite lookup_gset_to_gmap_Some, lookup_set_to_map; naive_solver.
+  Qed.
 End gset.
 
 Typeclasses Opaque gset.
-- 
GitLab