[Coq-Club] Reasoning About and Working With Unordered Sets of Abstract Variables in Coq

[Alyssa N Byrnes]

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

[Pierre Courtieu]

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]

Post by Alyssa N Byrnes
I'm looking to work with and reason about unordered sets of an abstract variable.
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

[Alyssa N Byrnes]

This is very helpful. Thank you!!

Alyssa Byrnes

Post by Pierre Courtieu
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.
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.
- 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]

Post by Alyssa N Byrnes
I'm looking to work with and reason about unordered sets of an abstract variable.
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