coq
Finite maps and finite sets
There are a lot of finite map and finite set implementations out there and I think it would be good to discuss what the shape of these types should be in stdlib2. Off the top of my head there are implementations in the stdlib, coq-containers, coq-stdpp and probably others I am not aware of or familiar with. Each of these implementations have different characteristics. Here is an incomplete list of some of them:
stdlib
- Finite maps and finite sets based on modules (no inference)
- Finite sets (but not maps) based on typeclasses
- Different implementations:
- Ordered and unordered lists of key-value pairs
- AVL trees
coq-containers
- Based on typeclasses
- Requires a total decidable order on keys, and exhibits many instances:
Z,nat,positive,bool,unit- Pairs and sums of ordered types
- Lists of ordered types
- Finite maps and finite sets of ordered types
- Includes plugin to automatically derive orders for user types which is very convenient
- No extensionality (even for implementations with canonical representations)
- Different implementations:
- Ordered lists of key-value pairs
- AVL trees
stdpp
- Based on typeclasses
- ~Only few types of keys allowed:
Z,nat,positive,string(and from a cursory glance seems a little difficult to implement maps with other key types)~ Maps implemented for any countable type of keys (see comments below) - Sets implemented in terms of maps
- Extensionality for its maps
If I have gotten anything wrong here then feel free to correct or in general just expand on it.
Personally, as a user coming from object oriented languages, I think that coq-containers was the easiest to use in terms of just working like I would expect. For instance, declaring a map with type Map[A, B] just worked out of the box for even complicated A's. In stdpp ~it appears you need to find a concrete implementation of a map with your key (Zmap, Nmap, etc.) which is much less discoverable~ (wrong, there is a finite map for any countable type of keys -- see below). I have not used stdlib extensively, but in my attempts it also seemed to suffer from poor discoverability due to the use of modules. Just figuring out how to make a function that takes an stdlib MSet was a task in itself.
In stdpp it appears you need to find a concrete implementation of a map with your key (Zmap, Nmap, etc.) which is much less discoverable.
The map implementation that you probably want to use is gmap K A, it works for any type of keys K that is countable.
Most of the implementations for concrete types like Nmap and Zmap are legacy, and subsumed by gmap. I guess we should document this somewhere :).
Thank you @robbertkrebbers, I have edited the OP. I need to give stdpp another try in my own development then. 👍