Instances

stdpp/fin_map_img.v

@@ -273,3 +273,16 @@ Section fin_map_img.
   Global Instance set_unfold_img_empty i : SetUnfoldElemOf i (img (∅:M A)) False.
   Proof. constructor. by rewrite img_empty, elem_of_empty. Qed.
 End fin_map_img.
+
+Global Instance fin_map_img K A M D
+  `{FinMapToList K A M, Singleton A D, Empty D, Union D}
+: Img M D := map_to_set (fun _ a => a).
+
+Global Instance fin_map_img_spec K A M D
+  `{HFinMap:FinMap K M} `{HFinSet:FinSet A D} : FinMapImg K A M D.
+Proof.
+  split; [exact HFinMap | apply fin_set_set |].
+  unfold img, fin_map_img. intros m v. rewrite elem_of_map_to_set. split.
+  - intros [k [v' [mk_v' v'_v]]]. exists k. rewrite v'_v in mk_v'. exact mk_v'.
+  - intros [k mk_v]. exists k. exists v. split; [exact mk_v|reflexivity].
+Qed.

stdpp/gmap.v

@@ -9,7 +9,7 @@ To compute concrete results, you need to both:
   [gmap]/[gset], does not contain proofs, say via [map_to_list] or [!!]; and
 - use [vm_compute] to run the computation, because it ignores opacity.
 *)
-From stdpp Require Export countable infinite fin_maps fin_map_dom.
+From stdpp Require Export countable infinite fin_maps fin_map_dom fin_map_img.
 From stdpp Require Import pmap mapset propset.
 From stdpp Require Import options.
 
@@ -282,6 +282,11 @@ Section gset.
     pose proof (mapset_dom_spec (M:=gmap K)) as [?? Hdom]; split; auto.
     intros A m. specialize (Hdom A m). by destruct m.
   Qed.
+  Global Instance gmap_img `{Countable A} : Img (gmap A K) (gset K) :=
+    fin_map_img A K (gmap A K) (gset K).
+  Global Instance gset_img_spec `{Countable A} : FinMapImg A K (gmap A) (gset K) :=
+    fin_map_img_spec A K (gmap A) (gset K).
+
 
   (** If you are looking for a lemma showing that [gset] is extensional, see
   [sets.set_eq]. *)