Stream: Coq users

Topic: Set operations in coq

Julin S (Nov 21 2021 at 11:00):

Is there a built-in/predefined way to do set operations like union in coq?

Found https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.SetIsType.html#:::'Set' but that didn't seem to be it.

Paolo Giarrusso (Nov 21 2021 at 11:38):

Quick partial answer: Set is a built-in but not what you want (you can read it mostly as Type), and the sets you want aren't builtins. But lots of libraries exist! Do you want data structures for finite sets, or do you want to also handle infinite sets via their defining predicates?

Julin S (Nov 21 2021 at 11:39):

I'm just looking to handle finite sets.

Julin S (Nov 21 2021 at 11:40):

Which library can be used for that?

Paolo Giarrusso (Nov 21 2021 at 11:40):

The stdlib has Ensembles and IIRC some data structures (FSet?) using modules; stdpp and math-comp have other options.

Paolo Giarrusso (Nov 21 2021 at 11:41):

(I'm sure that doesn't cover all options)

Paolo Giarrusso (Nov 21 2021 at 11:42):

In stdpp, we use gset; I'll leave answers on math-comp to others.

Julin S (Nov 21 2021 at 11:47):

Thanks. Let me try looking into them. Never tried stdpp and mathcomp before.
Had seen the ensemble thing (don't really know what it's about. Not a math person) at https://coq.inria.fr/library/Coq.Sets.Ensembles.html but wasn't sure if it was something else at the time.

Gaëtan Gilbert (Nov 21 2021 at 11:49):

ensemble means set in french

Julin S (Nov 21 2021 at 11:49):

Ah.. that makes sense.. :D

Ana de Almeida Borges (Nov 21 2021 at 11:50):

math-comp has finset for finite sets over finite types and finmap for finite sets over types with a choice operator. But yeah, if you don't otherwise use math-comp, it will not be seamless to use these libraries.

Paolo Giarrusso (Nov 21 2021 at 11:50):

Ensembles represent (not-necessarily-finite) sets on A by a membership predicate A -> Prop. Outside classical logic, that's not even enough to actually implement a membership test A -> Ensemble A -> bool

Karl Palmskog (Nov 21 2021 at 14:04):

see a recent discussion on set library choice here

Last updated: Dec 05 2023 at 11:01 UTC