Is there a lightweight way to define a mutable dictionary that can return all of its keys in Coq?

Question

I want to define a mutable dictionary that can return all of its keys in its domain. Keys don't have to be ordered. I searched in the coq library doc on the internet and didn't seem to find anything useful for this purpose. I don't want to write it as a list of pairs because it feels too ad hoc. Is there a standard way to do this?

As an example, how can I define a dictionary d := {a -> 1; b -> 2; c -> 3}, and a function "keys", such that keys d = [a; b; c]?

---

Edit: I forgot to mention that I also want to use datatypes that I defined myself as keys. For example something like:

Inductive a := cons_a : string -> a.
Inductive b := cons_b : string -> b.
Inductive c :=
  | cons_c : int -> cons_c
  | c1
  | c2.
Inductive d :=
  | cons_d1 : string -> d
  | cons_d2 : string -> d

and I want to define a map for each of a b c d as keys. Like d1 := {cons_a "a" -> 1; cons_a "b" -> 2}, d2 := {cons_d1 "a" -> 1; cons_d2 "a" -> 2}, d3 := {cons_c 1 -> 1; c1 -> 0}, etc.

Answer 1

The standard library Coq.FSets.FMapxxx is what you are looking for (although there are many equivalents out there). First find the functor corresponding to the maps you want (here I take FMapAVL), and instantiate it with an OrderedType for keys (here I take the already defined OrderedTypeEx.String_as_OT). Note the type of elements is left quantified:

Require FSets.FMapInterface FSets FMapAVL.
Module Import FMapInt := FMapAVL.Make(OrderedTypeEx.String_as_OT).

(* Let us define a map string -> t *)
Require Import String.
Open Scope string_scope.

Definition foo:= (add "a" 1 (add "b" 2 (add "c" 3 (empty _)))).

(* this gives the list of pairs (key,val) *)
Eval compute in elements foo.

(* A simple map gives the list of keys. With AVL this list
   is ordered, but it is not necessary the case with other
   kinds of maps. *)
Eval compute in (List.map fst (elements foo)).

(* see the list of lemmas about FMapInt: *)
Search FMapInt.t .

Answer 2

stdpp has gmap, which has a dom function (returning a gset) and that has a to_list function. These compute reasonably well for concrete instances, but in general they work by de- and re-encoding keys into numbers, which might not be what you want.

See https://plv.mpi-sws.org/coqdoc/stdpp/stdpp.gmap.html.