The Coq mailing list

[Chantal Keller <chantal.keller AT wanadoo.fr>]

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.