The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

Dear all,

To wish everybody a happy new year, I'm announcing a first version of my FinSet library which implements finite (sub)sets of countable types. This is based on Cyril Cohen's work on quotients in Coq and its implementation in the Ssreflect and MathComp libraries (FinSet is, however, independent from Ssreflect).

The files can be found in github [ https://github.com/aspiwack/finset ]. There is also a coqdoc-generated documentation [ http://aspiwack.github.io/finset/toc.html ]. It compiles with Coq's trunk.

The basic principle is that quotient by decidable relations of (suitably) countable type can be implemented in plain Coq without axioms (because we can choose canonical representatives of equivalence classes). This FinSet library has been mostly done in my off time, and is not quite stable yet. I'm offering it mostly for exposition. All comments are, of course, welcome.

Compared to Coq's MSet library, FinSet (an admittedly poorly chosen name which is susceptible to change if good suggestions come up) is not focused on efficiency at all. Sets defined in FinSet are effective but they are meant to be used in specification only, any attempt at a non-trivial computation with these is doomed to a terrible and painful failure (seriously, don't). On the other hand equality of FinSet sets is plain Coq equality, which is convenient.

The FinSet library uses a type-class interface to countable types rather than using functors (this can also be seen as a consequence of forgetting about efficiency). This is important as it allows to define a syntax for comprehension (though I must confess that this syntax is a bit poor, I should probably use a plug-in rather than simple notations). Here are examples of sets defined by comprehension:

Intersection: ⦃ x \ st x∈u₂ ⍪ x∈u₁ ⦄
Replacement: ⦃ f x \ ⍪ x∈u ⦄
Cartesian product: ⦃ (x,y) \ ⍪ y∈u₂ ⍪ x∈u₁ ⦄

Thanks to the [simpl never] of the [Argument] command, the [cbn] and [simpl] commands quite pleasantly treat the set theoretical primitives as abstract.


Have fun with it!