I want to be able to have a map from any type to any type in Coq. So far I have had some success using Coq.FSets.FMapList from the standard library, but I have only been able to create maps where the key is a natural number, by doing the following.
Require Import Coq.FSets.FMapList.
Require Import Coq.Structures.OrderedTypeEx.
Module Import NatMap := FMapList.Make(Nat_as_OT).
(* whatever I want to do with my NatMap *)
I know that NatMap := FMapList.Make(Nat_as_OT). is declaring that I want to use a map whose keys are Nat_as_OT. However, FMapList.Make will only accept an OrderedType as an argument. Its there a way I can make my own OrderedType? Or is there a better way of creating a map?
You won't easily find maps from any type to any type, because for such a map to work you at least need to be able to distinguish two element of the type used for keys. If you only have this capability (testing whether two elements are the same), then maps can be implemented in a fairly inefficient way: you basically handle a list of pairs (key, value) and the cost of retrieving the value associated to a key is proportional to the number of keys that are already handled in your map, on average.
If you want to be slightly more efficient, a usual trick is to have hash keys, but you need to be able to compute hash values, so your type cannot be completely arbitrary.
In the end, there is the possibility to use maps based on a type that has an order. In this case, it is quite easy to implement the map is such a way that retrieving the value for a key with a cost that is logarithmic in the number of keys, on average.
Now, how do you create an OrderedType object? You need to instantiate module type MiniOrderedType. So, for your type you need to say what function will play the role of eq, lt, and show the various important properties listed in the MiniOrderedType module type (see this file). There are several example of this construction in this example file).