coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Chantal Keller <chantal.keller AT wanadoo.fr>
- To: Thomas Braibant <thomas.braibant AT gmail.com>
- Cc: 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 14:12:27 +0100
Thomas Braibant a écrit :
Sorry if I misunderstood you, but this sentence bugs me:
I then tried to use FSets, but it is not well-suited for computation,
since you have to compute a lot of proofs: for instance, in the
implementation with lists, you always need a proof that this list is not
redundant, otherwise the "remove" function would not be correct.
using FSets, you do not have to compute a lot of proofs by hand. I
reckon that the FSetList.Raw modules somehow hides the fact that the
lists are not redundant, but this is nicely packaged inside the
module. If you create an instance of FSetList using a given ordered
type (say M), using
Module FS := Coq.FSets.FSetList.Make (M).
then FS.remove has type FS.elt -> FS.t -> FS.t. (FS complies to
FSetInteface.S)
What I fear, is that you are trying to use the FSetList.Raw functor,
which indeed requires additionnal hypotheses when you apply lemmas
(the information that the list representing a set is well-formed is
not hidden by the signature, and you could provide the function with
an ill-formed list)
Otherwise, I reckon that the actual type of FS.t is a sig type which
encapsulates a proof that the list is well-formed, proof that must be
computed. But, in my own experience, even with huge computations in
Coq, this is not a real problem.
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.
Since the original poster said that he do not requires to compute at
all, FSetList would be ok for him.
Perhaps.
Hope this helps,
Thomas
Chantal.
- [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,
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.