The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On 08/05/2011 10:58 AM, Marco Servetto wrote:

> I do need for setting my workbench a concept of finite map (and thus
> finite set) where keys K have the following good properties:
> [having a total, decidable order]
> Can someone suggest me how to proceed?
> Is there a librariy already implementing something similar?

Yes!  The FMaps library from Coq's standard distribution fits exactly
your needs, including an equality test between maps, and a nifty
induction principle:

http://coq.inria.fr/stdlib/Coq.FSets.FMapInterface.html
http://coq.inria.fr/stdlib/Coq.FSets.FMapFacts.html

Moreover, given the beq and blt functions available for your type K of
keys, you can even use the algorithmically-efficient implementation
FMapAVL, which comes very handy if extract to executable Caml code or
do a lot of computations over maps within Coq.

Enjoy,

- Xavier Leroy