The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello. To simplify a little bit the use of FSet/FMap and see some examples, you can have a look at the CoLoR library, files Util/FSet/FSetUtil, Util/FMap/FMapUtil, Util/FGraph/FGraph, Util/FGraph/TransClos, ... available on http://color.inria.fr . For potentially infinite sets, see Util/Set/SetUtil. Best regards, Frédéric.

Le 03/08/2013 01:30, Kevin Sullivan a écrit :

Thank you, Cedric. Yeah, we're currently using a simple, home-grown "library", along the lines you suggest here. My concern with F/M/Sets mirrors your suggesting that working with them is painful. I don't want to inflict an unreasonable burden on the graduate student who has to deal with whatever library we choose. I'm happy to receive additional advice. Best, --Kevin

On Fri, Aug 2, 2013 at 1:22 PM, Cedric Auger <sedrikov AT gmail.com> wrote:

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