The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

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.

Since the original poster said that he do not requires to compute at
all, FSetList would be ok for him.

Hope this helps,
Thomas