Stream: Coq users

Topic: Set operations in coq


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Julin S (Nov 21 2021 at 11:39):

I'm just looking to handle finite sets.

view this post on Zulip Julin S (Nov 21 2021 at 11:40):

Which library can be used for that?

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 21 2021 at 11:41):

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

view this post on Zulip Paolo Giarrusso (Nov 21 2021 at 11:42):

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

view this post on Zulip 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.

view this post on Zulip Gaƫtan Gilbert (Nov 21 2021 at 11:49):

ensemble means set in french

view this post on Zulip Julin S (Nov 21 2021 at 11:49):

Ah.. that makes sense.. :D

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Nov 21 2021 at 14:04):

see a recent discussion on set library choice here


Last updated: Jan 29 2023 at 04:05 UTC