Commit 4a5056da authored by Robbert Krebbers's avatar Robbert Krebbers

Prove to_gmap y (dom _ m) = const y <$> m.

parent 64cafa57
......@@ -159,6 +159,15 @@ Proof.
elem_of_singleton; destruct (decide (i = j)); intuition.
Lemma to_gmap_dom `{Countable K} {A B} (m : gmap K A) (y : B) :
to_gmap y (dom _ m) = const y <$> m.
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).
(** * 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. *)
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment