From 4e0e29ebb3402636963b8f181a1f134e26c5cc95 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 20 Nov 2016 16:34:12 +0100
Subject: [PATCH] Prove to_gmap y (dom _ m) = const y <$> m.
---
prelude/gmap.v | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/prelude/gmap.v b/prelude/gmap.v
index 2db7ae45d..cb73640f6 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -159,6 +159,15 @@ Proof.
elem_of_singleton; destruct (decide (i = j)); intuition.
Qed.
+Lemma to_gmap_dom `{Countable K} {A B} (m : gmap K A) (y : B) :
+ to_gmap y (dom _ m) = const y <$> m.
+Proof.
+ apply map_eq; intros j. rewrite lookup_fmap, lookup_to_gmap.
+ destruct (m !! j) as [x|] eqn:?.
+ - by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
+ - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
+Qed.
+
(** * Fresh elements *)
(* This is pretty ad-hoc and just for the case of [gset positive]. We need a
notion of countable non-finite types to generalize this. *)
--
GitLab