From 4bea88d16f0c5e2dd9b1b736fc7fec6530a24514 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers 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