Commit 6ee0e09e authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'gset-gmap-delete' into 'master'

Prove theorem about delete of gset_to_gmap

See merge request !162
parents aa5e294c a04b0a88
Pipeline #29927 passed with stage
in 10 minutes and 48 seconds
......@@ -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.
Lemma gset_to_gmap_difference_singleton {A} (x : A) i Y :
gset_to_gmap x (Y {[i]}) = delete i (gset_to_gmap x Y).
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.
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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment