The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-sb.de>]

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

-- 
Regards
Christian