Using set_like

Stream: general

[Yaël Dillies]

How to use docs#set_like in practice? Consider the following definition

import data.finset.basic
import data.set.pairwise
import data.set_like.basic

/-- A finpartition of a finset `s` is a collection of disjoint subsets of `s` which cover it. -/
@[ext] structure finpartition_on {α : Type*} [decidable_eq α] (s : finset α) :=
(parts : finset (finset α))
(disjoint : set.pairwise_disjoint (parts : set (finset α)))
(cover : ∀ ⦃x⦄, x ∈ s → ∃ (a ∈ parts), x ∈ a)
(subset : ∀ ⦃a⦄, a ∈ parts → a ⊆ s)
(not_empty_mem : ∅ ∉ parts)

I set-likified in

/-- A finpartition of an set-like object `s` is a collection of disjoint subset-like objects of `s` which cover it. -/
@[ext] structure finpartition_on {α β : Type*} [set_like α β] (s : α) :=
(parts : finset α)
(disjoint : (coe '' (parts : set α) : set (set β)).pairwise_disjoint)
(cover : (s : set β) ⊆ ⋃ x ∈ parts, (x : set β))
(subset : ∀ ⦃a⦄, a ∈ parts → (a : set β) ⊆ s)
(not_empty_mem : (∅ : set β) ∉ (coe '' (parts : set α) : set (set β)))

but that's pretty unsatisfactory as I've added a bunch of coercions. In particular, I could already express ∅ ∉ parts without going through set β but that requires knowing there's an ∅ : α and that it gets coerced to ∅ : set β.
Am I right in thinking we have no way of relating the structures on α and set β? And is this the right approach?

[Yaël Dillies]

By the way, @Eric Wieser, thanks for this masterpiece!

[Eric Wieser]

Your setified version doesn't require the entries of parts be finite; is that what yo uwanted?

[Yaël Dillies]

Yeah. I can recover the "finite parts" case by taking s : finset α, so this second definition is strictly more general, right?

[Yaël Dillies]

What I can't do is to generalize the outer finset.

[Eric Wieser]

Do we even have docs#finset.set_like (edit: not under that name). I didn't design set_like for anything more than subobject, so have no suggestions for this type of use

[Yaël Dillies]

Oh really? Using it for finset α, multiset α, ... was for me the obvious application.

[Eric Wieser]

It would put the wrong partial_order on multiset, I think

[Eric Wieser]

Does multiset even have a coercion to set? I wouldn't be surprised if it didn't

[Yaël Dillies]

Oh yeah, maybe not multiset.

[Yaël Dillies]

But I always regarded set_like as the common generalization of set and finset.

[Eric Wieser]

I'm not opposed to adding the instance for finset, but we should have some evidence its going to be useful before doing it

[Yaël Dillies]

To reuse the above example, there are four kinds of partitions one could care about

• set (set α): partitions with parts
• finset (set α): finite partitions with parts
• set (finset α): partitions with finite parts
• finset (finset α): finite partitions with finite parts

[Yaël Dillies]

Having set_like (finset α) α would reduce that number to two.

[Yaël Dillies]

There are also, I assume, some of the finset and set APIs that are duplicated because not established in the set_like generality.

[Bhavik Mehta]

You should be able to generalise this further - to a lattice with bot: cover/subset can say the (finite) sup is s, not_empty_mem can say the bottom element isn't in parts and disjoint can say pairwise disjoint

[Yaël Dillies]

Damn, Bhavik always do be right.

[Kyle Miller]

I think that you should be careful with creating things that use set_like as a hypothesis -- if something is set_like, (in my opinion) the API is to just treat the thing like a set using the coercion. I see the typeclass as a mixin that causes functionality to be added to a type, rather than adding the functionality directly.

The only case I can think of where you might want set_like as a hypothesis is if you're defining a structure and you want it to have the correct extensionality properties. Most set_likes are subobjects of algebraic objects, so for a finpartition_on you'll have a hard time achieving disjointness.

[Kyle Miller]

I'd like to see finset get its set-like-ness from set_like someday, for uniformity. Maybe it's not so much work if you figure out a nice way to define the injection to set?