The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

If you want to stick with the standard library, I think you have to chose between FSets and MSets (http://coq.inria.fr/stdlib/). MMaps does not seem to exist. But as far as I can remember, FSets and FMaps are really painful. (You can take a look at the coq mailing list archive, there you will find many people having hard time to understand how it works).

I did never tried Stéphane Lescuyer’s Containers, but I am pretty sure that it is more convenient than the stdlib ones. I think Pierre Letouzey wanted to rewrite the stdlib libraries on Sets and Maps (not sure though, and maybe is it what resulted in MSet).

But if you do not really need computation (I mean efficient computation, or computation with big amounts of data, or many add/delete calls in the maps), I would recommend to use a naive one.

Something like:

Definition map (key : Type) (value : Type) := key -> option value.

Definition empty_map (key : Type) (value : Type) : map key value
:= fun _ => None.

Definition add (key : Type) (eq_key : forall x y : key, {x=y}+{x<>y}) (value : Type)
  (m : map key value) (k : key) (v : value) : map key value
:= fun k' => if eq_key k k' then (Some v) else m k'.

…

This is often a lot more convenient than the FMap current implementation which requires to build the module using a functor, then recall the name of many theorems defined by the FMapInterface.

You can also start with the naive implementation to have a skeleton of the program, and once it is done, translate the code using non naive, and this time efficient, data structures such as FMaps, and try to play with concrete stuff.

2013/8/2 Kevin Sullivan <sullivan.kevinj AT gmail.com>

Dear Coq Club:

A student and I need to write Coq code using simple finite sets and maps (e.g., to build symbol tables, do lookups in 1-n relations, and that sort of thing). Types are known statically. Are we best advised to use Coq's FSets library, Stéphane Lescuyer's First-Class Containers in Coq, or perhaps something else that we don't know about yet? 

Kind regards,

Kevin

--
.../Sedrikov\...