coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>
- To: St�phane Lescuyer <stephane.lescuyer AT inria.fr>
- Cc: Chantal Keller <chantal.keller AT wanadoo.fr>, Thomas Braibant <thomas.braibant AT gmail.com>, Christian Doczkal <doczkal AT ps.uni-sb.de>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] finite sets in proofs
- Date: Fri, 26 Mar 2010 15:15:04 +0100
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
- [Coq-Club] finite sets in proofs, Christian Doczkal
- Re: [Coq-Club] finite sets in proofs, Pierre Casteran
- Re: [Coq-Club] finite sets in proofs, AUGER
- RE: [Coq-Club] finite sets in proofs, Georges Gonthier
- Re: [Coq-Club] finite sets in proofs,
Chantal Keller
- Re: [Coq-Club] finite sets in proofs,
Thomas Braibant
- Re: [Coq-Club] finite sets in proofs,
Chantal Keller
- Re: [Coq-Club] finite sets in proofs, Thomas Braibant
- Re: [Coq-Club] finite sets in proofs,
Stéphane Lescuyer
- Re: [Coq-Club] finite sets in proofs, Pierre Letouzey
- Re: [Coq-Club] finite sets in proofs, Chantal Keller
- [Coq-Club] Yet another dependent type question,
Pierre-Marie Pédrot
- Re: [Coq-Club] Yet another dependent type question,
Adam Chlipala
- Re: [Coq-Club] Yet another dependent type question,
Pierre Corbineau
- Re: [Coq-Club] Yet another dependent type question, Pierre-Marie Pédrot
- Re: [Coq-Club] Yet another dependent type question, Michael Shulman
- Re: [Coq-Club] Yet another dependent type question, Hugo Herbelin
- Re: [Coq-Club] Yet another dependent type question, Michael Shulman
- Re: [Coq-Club] Yet another dependent type question, Hugo Herbelin
- Re: [Coq-Club] Yet another dependent type question,
Pierre Corbineau
- Re: [Coq-Club] Yet another dependent type question,
Adam Chlipala
- Re: [Coq-Club] finite sets in proofs,
Chantal Keller
- Re: [Coq-Club] finite sets in proofs,
Thomas Braibant
Archive powered by MhonArc 2.6.16.