Commit 249891cd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add lemma `dom_map_kmap`.

parent e18f9a7d
......@@ -198,6 +198,15 @@ Proof.
naive_solver.
Qed.
Lemma dom_map_kmap `{!Elements K D, !FinSet K D, FinMapDom K2 M2 D2}
{A} (f : K K2) `{!Inj (=) (=) f} (m : M A) :
dom D2 (map_kmap (M2:=M2) f m) set_map f (dom D m).
Proof.
apply set_equiv. intros i.
rewrite !elem_of_dom, (lookup_map_kmap_is_Some _), elem_of_map.
by setoid_rewrite elem_of_dom.
Qed.
(** If [D] has Leibniz equality, we can show an even stronger result. This is a
common case e.g. when having a [gmap K A] where the key [K] has Leibniz equality
(and thus also [gset K], the usual domain) but the value type [A] does not. *)
......@@ -252,6 +261,11 @@ Section leibniz.
Proof. unfold_leibniz. apply dom_union_inv. Qed.
End leibniz.
Lemma dom_map_kmap_L `{!Elements K D, !FinSet K D, FinMapDom K2 M2 D2}
`{!LeibnizEquiv D2} {A} (f : K K2) `{!Inj (=) (=) f} (m : M A) :
dom D2 (map_kmap (M2:=M2) f m) = set_map f (dom D m).
Proof. unfold_leibniz. by apply dom_map_kmap. Qed.
(** * Set solver instances *)
Global Instance set_unfold_dom_empty {A} i : SetUnfoldElemOf i (dom D (:M A)) False.
Proof. constructor. by rewrite dom_empty, elem_of_empty. Qed.
......
Supports Markdown
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