The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  Well, you might be interested in the ssreflect library, which includes an 
extensive treatment of finite sets and functions, including cardinals, 
partitions, iterated unions and interections, functional image, etc. You can 
browse it at
  http://coqfinitgroup.gforge.inria.fr/ssreflect/
The library uses Coq's Canonical Structure mechanism to supply implicitly the 
comparison function. Unlike the libraries below, it is based on finite types 
(using Canonical Structures to supply a standard enumeration). For a fairly 
modest investment in framing the problem at hand, this allows the free use of 
naive set theory, in particular unrestricted comprehensions and complement, 
which make the library considerably more useful.

Georges Gonthier

-----Original Message-----
From: Christian Doczkal 
[mailto:doczkal AT ps.uni-sb.de]
 
Sent: 26 March 2010 11:56
To: 
coq-club AT inria.fr
Subject: [Coq-Club] finite sets in proofs

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