The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Fri, Mar 26, 2010 at 02:33:33PM +0100, Stéphane Lescuyer wrote:
> > Sorry if I was not clear. Of course, you do not have to perform the proofs
> > by yourself, I was only speaking about a problem of computation:
> >
> > - even if computation is rather good in Coq, it takes some time...
> >
> > - in fact, you even cannot perform this computation, since the proofs that
> > the lists are not redundant in FSets are opaque. So if you try something
> > like :
> >
> > remove (add x empty_set)
> >
> > you will not get what you expect.
> 
> It depends what it is you 'expect'. FSets are well-suited for
> computation (even inside Coq, even with sig-types) and I have complex
> applications which heavily rely on their mechanism anad work quite
> well. From my experience, the overhead of having sig-types instead of
> raw data structures is roughly 50%, which means you won't see any real
> difference for computations under 1s. And there's a lot vm_compute can
> do in that span :)
> 

Some quite remarks on the subject: 

- The old Coq.List.ListSet file that has been mentioned earlier in the
  thread is quite old-fashioned and rather poor. In a word, obsolete.
  I would really advise avoiding it, and it might even disappear some
  day from Coq stdlib.

- Coq 8.3 comes with an additionnal finite set library called MSets,
  which is an evolution of FSets where in particular proofs may be
  left as separate side-conditions (see interface
  MSetInterface.RawSets). It's just like the "Raw" modules (e.g. in
  FSetList), but documented by a legitimate interface. Moreover the
  compare operator is now a pure one.

Best,

Pierre Letouzey