The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Le 26/03/2010 12:56, Christian Doczkal a écrit :
> Hi
>
> I have a proof development where I want to reason about finite sets over
> decidable types. Im not interested in extracting code but I would like
> to make as much use of definitional equality as possible to simplify
> reasoning.
>
> The Coq Standard Library offers several developments on finte sets
>
> Coq.Sets.Finite_sets
> Coq.FSets
> Coq.ListSet
>
> The last seems looks most promising for what I would like to do, except
> that one always needs to explicitly provide the decision procedure for
> the equality and there are not a whole lot of lemmas proven in this
> library.
>
> Which route would you recommend? Is there a more complete (proof
> oriented) development on finite decidable sets that I am missing
>
>    
Hello,

  Did you look at the FSets library ? It contains a lot of already 
proven lemmas on finite sets.
This library uses the module system. Stéphane Lescuyer wrote a version 
bases on type classes, with most of the same functionalities.

Pierre