From 249891cd6fb877403b684efad0b1952de9fd0785 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 26 May 2021 15:23:58 +0200
Subject: [PATCH] Add lemma `dom_map_kmap`.

---
 theories/fin_map_dom.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index f0e3e9b1..c8b7097a 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -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.
-- 
GitLab