Is there a library for sets that works with bool in Coq?

I am looking to work with mathematical sets and subsets of some universal type.
I know this is normally represented as U -> Prop, such as in the Ensembles library.

I was wondering if there is perhaps some representation of sets that is decidable, perhaps where sets are represented as S : U -> bool where we can decide for any element of U whether it is in S, or is this simply impossible?

Ideally, I would like to be able to compute, given a collection of elements of type U, the subset of those elements that are in some set S as well.

You might want to have a look at the finset library of the mathcomp/ssreflect framework, if you don't know about it already: finset.v.

There are several libraries to work with sets in Coq:

• Ensembles: available in the Coq standard library, the sets can be infinite, a bit clunky.
• MSets: available in the Coq standard library, finite sets only, behaves well once extracted but the interface is clunky. See also this paper on the implementation.
• fin_sets from std++: finite sets only, membership is decidable, includes a set_solver tactic for some kinds of set goals.
• finset from MathComp: finite sets for finite types, membership is decidable. See also this guide on finset and finmap (the next item).
• finmap from MathComp: finite sets for choice types (eg coutable types), membership is decidable.

Typically, once you use some part of std++ or of MathComp you are better off using all of it, in part because there is some non-trivial learning curve to these libraries (worth it, IMO).

Discussion on set libraries pops up often on Zulip (1, 2).