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.
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 .