The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Hello,

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

Out of curiosity, what were the other two?

>       • 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.

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) :

Lemma subsize_eq X Y : X `<=` Y -> size Y <= size X -> X = Y. 

In the particular case of Ssreflect, this has a one line proof by lifting a 
similar lemma from the list (seq) library. On the other hand, there are cases 
where the proof via monoids is more natural (in fact I do specialize some of 
Ssreflects "big operator" lemmas to "weight" functions from the carrier T 
type to nat (`|` = union, `&` = intersection, fsum w X = sum_(x \in X) w x):

Lemma fsumU (w : T -> nat) (X Y : {fset T}),
       fsum w (X `|` Y) = fsum w X + fsum w Y - fsum w (X `&` Y)

Which for example specializes to

Lemma fsizeU X Y : size (X `|` Y) <= size X + size 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.

-- 
Cheers
Christian