The Coq mailing list

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

Hi,

I already had the same problem.

I used ListSet for a while, but it is not a good solution for two
reasons:

- the "map" function is not correct, since the resulting list can be
  redundant (I reported this bug a while ago, but it did not change
  however);

- there are not a lot of the properties one could expect over finite
  sets.

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.

To avoid this problem, I finally found more efficient to change a little
the implementation of FSets with lists, such that we do not need all the
time a proof that the list is not redundant. You can mainly do it both
ways:

- change the function "remove" such that it does not suppose that the
  list is not redundant;

- change the function "remove" such that it first removes all the
  redundancies in the list.

Of course, all these modifications slow down a little the remove
function, but we avoid having big proofs, and the computation goes well
in my case.

Finally, if your decidable type is finite, you can also use the
SSReflect library "finset"
<http://coqfinitgroup.gforge.inria.fr/finset.html>.

Hope this helps,
Chantal.




Christian Doczkal a écrit :
> Hi
>
> I have a proof development where I want to reason about finite sets over
> decidable types. Im not interested in extracting code but I would like
> to make as much use of definitional equality as possible to simplify
> reasoning.
>
> The Coq Standard Library offers several developments on finte sets
>
> Coq.Sets.Finite_sets 
> Coq.FSets
> Coq.ListSet 
>
> The last seems looks most promising for what I would like to do, except
> that one always needs to explicitly provide the decision procedure for
> the equality and there are not a whole lot of lemmas proven in this
> library.
>
> Which route would you recommend? Is there a more complete (proof
> oriented) development on finite decidable sets that I am missing