The Coq mailing list

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

On 6 February 2015 at 14:57, Strub, Pierre-Yves <pierre-yves AT strub.nu> wrote:

One of the two must be that one, that I wrote after the third time somebody asked me "How would you do finite sets over an infinite carrier in ssr". This is not something I'm planing to maintain anyway.

https://github.com/strub/ssrmisc/blob/master/fset.v

Indeed, and I don't feel at liberty to say anything more about the other one which hasn't been, to the best of my knowledge, publicly announced. Ssreflect has much of the needed material to write such a library already built-in. It's not surprising that several people that use ssreflect would turn to write it. Me… I'm just fooling around (for instance, the list part of my library is way longer than it needs to be, just because I wanted to experiment with something).


On 6 February 2015 at 11:19, Christian Doczkal <doczkal AT ps.uni-saarland.de> wrote:

Of this I'm not entirely sure. Some (most) of the typical facts about cardinality connect set inclusion to the order on nat. Thus the generalization would likely be ordered commutative monoids. However, some lemmas explicitly exploit, that you are "folding" with a constant non-zero function such as (X `<=` Y means X is a subset of Y) :

⋮

I guess the bottom line is that, regardless of the actual definition of cardinality, you want to know that it is equivalent to both, list length and "folding" with the constant 1 function.

I'm not sure the order is that relevant, as the order comes from the monoid structure. And, of course, list length is a particular case of lists being the free monoid so the correspondance with lists may very well come for free in the "folding a commutative monoid" perspective. Except I don't know yet how to relate these free instances. Meh…