The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,
It depends what kind of sets you want.

1) you need to reason about infinite sets? If yes then Ensembles
(+Classical_Sets?) is about everything you have got afaik, in
particular you lose induction principles.

otherwise:
2) Do you want to suppose a decidable equality over elements? If you
want to really compute on them at some point you probably do.

If yes: you can use MSetXXX functors of the standard library. Lots of facts.

otherwise:
- Library Finite_sets  +  Finite_sets_facts  which are built upon Ensembles,
- https://coq.inria.fr/library/Coq.Vectors.Fin.html#t   represents
finite sets as segment of integers of the form :[1..n].
- https://github.com/aspiwack/finset    another representation using numbers

There are probably much more.

Hope this helps
Pierre



which represents sets of consecutive integers [1..n]
Le jeu. 27 sept. 2018 à 15:02, Alyssa N Byrnes 
<abyrnes1 AT cs.unc.edu>
 a écrit :
>
> I'm looking to work with and reason about unordered sets of an abstract 
> variable.
>
> For example, I define variable a as:
>
>     Variable a : Type.
>
> I know I can use Ensembles, but the Ensembles library doesn't have a lot of 
> supporting theorems. Are there any other libraries I can use?
>
> (If you have a suggestion, could you please show an example of how you 
> would instantiate one of these sets?)
>
> Many thanks!
> Alyssa Byrnes