finset implementation

Stream: general

[Kenny Lau]

What is the advantage of implementing finset as it is now, over implementing it as multiset quotient by extensionality?

[Chris Hughes]

I'm guessing efficiency of computation, but also perhaps some of the proofs are easier, since the functions are more or less identical to the multiset versions. Something like finset.sum is harder to implement with finsets as a quotient.

[Kenny Lau]

But if we implement it as a quotient, then we can have finset.union

[Chris Hughes]

Without decidable_eq you mean? Hooray. On the downside we'll need decidable_eq for finset.sum and finset.card

[Simon Hudon]

@Kenny Lau I think both implementations can be valuable. Find a different name and then you can provide that new implementation.

[Kenny Lau]

great

[Kenny Lau]

could you help me think of a name?

[Simon Hudon]

One benefit of finset's current implementation is in writing programs that are meant to be executed. Keeping the list minimal is more economical on memory.

[Simon Hudon]

The most obvious candidate would be finset' but I'm not sure that it's good. We could go with variations on finset (like finite_set) but I think that's more confusing than anything else. How about no_eq.finset?

[Simon Hudon]

The other alternative would be to change the name of the current implementation to compact.finset or minimal.finset or efficient.finset

[Simon Hudon]

I like your idea. Your kind of implementation makes a set that is easier to use as a monad and as a traversable collection.

[Mario Carneiro]

I would suggest something like qfinset or stacked_finset

[Mario Carneiro]

I'm not seeing where the gains are though

[Kevin Buzzard]

you can have union without decidable equality :-)

[Mario Carneiro]

gains plural

[Kevin Buzzard]

:-)

[Kevin Buzzard]

Presumably this means that the two definitions can't be proved to be equal without decidable equality?

[Mario Carneiro]

For the most part anything you can do with a stacked finset you can also do with a multiset

[Mario Carneiro]

There is a computable function finset -> qfinset but the reverse is erase_dup which requires decidable eq

[Kevin Buzzard]

gotcha

[Mario Carneiro]

But all these functions already exist, between finset and multiset

[Simon Hudon]

I can see three reasons for using stacked sets.

1. you mean it to form a monad (or a similar kind of functor)
2. you need it to be traversable
3. you want to work with finite sets while using set equality directly without translating back and forth between set and multiset.

[Simon Hudon]

qfinset is then like set+ finiteness invariant, similarly to multiset