The Coq mailing list

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

Sweet (interestingly enough this is the third ssreflect-based library that has been reported to me since I posted this announcement).

Some remarks:

• My initial implementation had duplicates in the representatives because it was easier to hack together, I quickly switched to representatives without duplicate because it's got many advantages (I've just updated the online doc now, though).
• I haven't added anything about cardinality yet, because it should come as a corollary of a more general operation which is that commutative monoids can be "folded" over a finite set. I haven't implemented this operation yet, because I don't quite see how to specify it elegantly (maybe using the retraction from sets to multisets? But what are its relevant property). For the case of idempotent (commutative) monoids, it's easier: sets are free.
  
• In the ssreflect library so far, comprehension is given a non-extensible syntax (extended an existing set of notations for list). In my library I've elected for a compositional syntax with the cost of a reasonably ugly syntax. It makes me wonder if we could get the best of both words with some syntax plugin written in ocaml. That would be totally sweet (especially if it can be bound to notation scopes). I'll be thinking about it.
  

On 3 February 2015 at 10:52, Christian Doczkal <doczkal AT ps.uni-saarland.de> wrote:

Hello,

Arnaud's design is actually quite similar to a library I created a while
ago as background theory for some of my developments. My library uses
Ssreflect and its design is inspired by Ssreflect's "finset" library.
The main motivation was to relax the requirement on the base type from
finite types to countable types and recover those lemmas from the
"finset" library that still hold.

The library includes most of the basic theory of finite sets
(separation, replacement, powerset, cardinality, ...)

The library also includes some other useful constructions such as a
construction for least and gratest fixpoints for bounded monotone functions.

I represent finite sets over types with choice (e.g., countable types)
using canonical duplicate free lists. I use duplicate free
representatives because because this allows me to use the length of the
list as cardinality and lift some lemmas for list length to sets.
Incidentally, this also uniquely determines the representatives
for {} and {x}, which is handy at a few places. But of course one can
also deduplicate in the definition of cardinality.

I don't have a working Coq trunk/beta, so I could not run Arnaud's
development, but it looks like his library uses representatives with
duplicates.

Arnaud's email prompted me to clean up the library and make it available
at:

        https://www.ps.uni-saarland.de/formalizations/fset.php

(I missed the original email, but it came up in a discussion at our lab)

If you use and extend the library, please drop me an email. I'm happy to
incorporate any improvements/additional lemmas sent so me.

I'm also willing to help porting some of the constructions to Arnaud's
plain Coq library.

Have fun with it!

--
Cheers
Christian


Am 05.01.2015 um 12:54 schrieb Arnaud Spiwack:

> 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!