The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

> 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 :)

Now, regarding your second point, I think you are missing something :
proofs ought to be opaque ; it is precisely what allows you to keep a
reasonable computational behaviour, since this prevents the virtual
machine to spend time reducing them. On the other hand, if you compute
an FSet object as is and try to print it out ([Eval vm_compute in
remove x (add x empty)] in your case), you end up with the whole
structure, with the proofs, which in practice is just a list of lemma
applications [remove_sort x (add_sort x empty_sort)] or something like
that, and indeed it is not what you expect to see. But it is not the
way you should look at the result of the computations, such structures
shouldn't be printed as they are but observed with the [elements]
functions for instance. If you try instead :

Eval vm_compute in (elements (remove x (add x empty))).

Coq will indeed return [nil] and in almost zero time. Similary, you
can try membership checks :

Eval vm_compute in (mem y (remove x (add x empty))). (* returns false *)

So theres a bit of confusion here between being able to print and read
the structure, and being able to compute with this structure.

HTH,

Stéphane L.
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06