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.

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?

I'm just looking to handle finite sets.

Which library can be used for that?

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

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

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

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.

ensemble means set in french

Ah.. that makes sense.. :D

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.

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`

see a recent discussion on set library choice here

Last updated: Jan 29 2023 at 04:05 UTC