From a04b0a88e9c3dcc81b178726e94661c3e4d1e537 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 26 May 2020 13:10:41 -0500
Subject: [PATCH] Prove theorem about delete of gset_to_gmap

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

diff --git a/theories/gmap.v b/theories/gmap.v
index 8684a92c..3b0405e8 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -265,6 +265,13 @@ Section gset.
     rewrite lookup_insert_Some, !lookup_gset_to_gmap_Some, elem_of_union,
       elem_of_singleton; destruct (decide (i = j)); intuition.
   Qed.
+  Lemma gset_to_gmap_difference_singleton {A} (x : A) i Y :
+    gset_to_gmap x (Y ∖ {[i]}) = delete i (gset_to_gmap x Y).
+  Proof.
+    apply map_eq; intros j; apply option_eq; intros y.
+    rewrite lookup_delete_Some, !lookup_gset_to_gmap_Some, elem_of_difference,
+      elem_of_singleton; destruct (decide (i = j)); intuition.
+  Qed.
 
   Lemma fmap_gset_to_gmap {A B} (f : A → B) (X : gset K) (x : A) :
     f <$> gset_to_gmap x X = gset_to_gmap (f x) X.
-- 
GitLab