bUnion for set

Stream: Is there code for X?

[Marcus Rossel]

Is there something like docs#finset.bUnion for set?

[Eric Wieser]

docs#set.sUnion?

[Eric Wieser]

Certainly ⋃ (x ∈ s), t x will do what you want

[Kyle Miller]

set.Union does both unbounded and bounded unions, and theorems about specifically ⋃ (x ∈ s), t xtend to have bUnion in the name. This would be the notation that finset.bUnion would use if it had any.

Internal detail that you should be able to ignore: the notation means
set.Union (λ (x : α), set.Union (λ (H : x ∈ s), t x))
which might not be be quite what you'd expect -- it's interesting how doing the union over x ∈ s is a way to conditionally control whether the set t x is included in the union.

[Kyle Miller]

Here's another attempt at making a unified notation for set.Union and finset.bUnion. Some features:

• ⋃ x, f x will try finset.univ.bUnion f if [fintype x].
• ⋃ (x ∈ s), f x will try s.bUnion f.
• These can be mixed, like in ⋃ (x ∈ s) y, f x y.
• ⋃ (i < 5), f i, for example, will try finset.univ.bUnion (λ (x : {i | i < 5}), f x) when the property as a set is a fintype.

All the usual things still work for set unions.

[Kyle Miller]

import data.set.basic
import data.set.lattice
import data.finset.basic
import data.fintype.basic
import data.set.finite

class has_Union {α : Sort*} (x : α) (β : out_param $ Sort*) :=
(Union : β)

local notation `⋃` binders `, ` r:(scoped f, has_Union.Union f) := r

instance set_Union (ι : Sort*) (α : Type*) (f : ι → set α) : has_Union f (set α) :=
{Union := set.Union f}

/-- Ideally this instance would cause an error if it ever were actually used.
It's here to help typeclass inference along -- we need every union in a chain
of unions to have a definition. -/
@[priority 0]
instance finset_Union_default_error (ι : Sort*) (α : Type*) (f : ι → finset α) :
  has_Union f (finset α) :=
{Union := ∅}

instance finset_pred (ι : Type*) (p : ι → Prop) [fintype {x | p x}] (α : Type*) [decidable_eq α] (f : ι → finset α) :
  has_Union (λ x, has_Union.Union (λ (h : p x), f x)) (finset α) :=
{Union := finset.univ.bUnion (λ (y : {x | p x}), f y)}

instance finset_Union (ι : Type*) [fintype ι] (α : Type*) [decidable_eq α] (f : ι → finset α) :
  has_Union f (finset α) :=
{Union := finset.univ.bUnion f}

instance finset_attach_bUnion (ι : Type*) (s : finset ι) (α : Type*) [decidable_eq α] (f : Π (x : ι), x ∈ s → finset α) :
  has_Union (λ x, has_Union.Union (λ (h : x ∈ s), f x h)) (finset α) :=
{Union := s.attach.bUnion (λ p, f p p.property)}

instance finset_bUnion (ι : Type*) (s : finset ι) (α : Type*) [decidable_eq α] (f : ι → finset α) :
  has_Union (λ x, has_Union.Union (λ (h : x ∈ s), f x)) (finset α) :=
{Union := s.bUnion f}

example (ι : Type*) (s : finset ι) (α : Type*) [decidable_eq α] (f : ι → finset α) :
  (⋃ (x ∈ s), f x) = s.bUnion f := rfl

example (ι : Type*) [fintype ι] (α : Type*) [decidable_eq α] (f : ι → finset α) :
  (⋃ x, f x) = finset.univ.bUnion f := rfl

example (ι ι' : Type*) (s : finset ι) (s' : finset ι') (α : Type*) [decidable_eq α] (f : ι → ι' → finset α) :
  (⋃ (x ∈ s) (y ∈ s'), f x y) = s.bUnion (λ x, s'.bUnion (f x)) := rfl

example (ι ι' : Type*) (s : finset ι) [fintype ι'] (α : Type*) [decidable_eq α] (f : ι → ι' → finset α) :
  (⋃ (x ∈ s) y, f x y) = s.bUnion (λ x, finset.univ.bUnion (f x)) := rfl

example (ι : Type*) (α : Type*) [decidable_eq α] (s : finset ι) (f : s → finset α) :
  (⋃ x (h : x ∈ s), f ⟨x, h⟩) = s.attach.bUnion f :=
begin
  ext, simp [has_Union.Union],
end

example (ι ι' α : Type*) (f : ι → ι' → set α) :
  (⋃ x y, f x y) = {z | ∃ x y, z ∈ f x y} :=
begin
  ext, simp [has_Union.Union],
end

example (ι α : Type*) (s : set ι) (f : ι → set α) :
  (⋃ (x ∈ s), f x) = {z | ∃ x, x ∈ s ∧ z ∈ f x} :=
begin
  ext, simp [has_Union.Union],
end

example (α : Type*) (f : ℕ → set α) :
  (⋃ (i < 5), f i) = {z | ∃ i, i < 5 ∧ z ∈ f i} :=
begin
  ext, simp [has_Union.Union],
end

example (α : Type*) [decidable_eq α] (f : ℕ → finset α) :
  (⋃ (i < 5), f i) = (finset.range 5).bUnion f :=
begin
  ext, simp [has_Union.Union],
end

[Kyle Miller]

There seems to be just one wart: if typeclass inference can't properly resolve has_Union for finset-valued unions, the union is the empty set. It would be nice if there were a way to make it be an error if this instance were to ever be used. (sorry is one possibility.)

[Kyle Miller]

This has_Union typeclass could be easily modified for sums, products, and intersections.

[Eric Wieser]

Didn't you post this before? Can you find the old thread?

[Kyle Miller]

@Eric Wieser I rewrote it from scratch, and I was too lazy to dig up the old thread.

[Kyle Miller]

Maybe I should have, because I apparently went through exactly the same exercise with exactly the same results... Not sure exactly what that suggests, but I'll go with maybe it's a workable idea.

[Kyle Miller]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/finsets.2C.20unions.2C.20and.20cardinality/near/224129427

[Kyle Miller]

I had tried getting this generalized union class to work a while back, but the dependent types made it completely unworkable in practice, which is why it's never seemed to go anywhere.

[Kyle Miller]

I took another crack at it this morning with a new approach, and it seems like it might actually work.

[Kyle Miller]

import data.set.basic
import data.set.lattice
import data.finset.basic
import data.fintype.basic
import data.set.finite

@[reducible]
def Union_binder (α : Sort*) : Sort* := α

@[inline, reducible]
def Union_binder.mk {α : Sort*} (x : α) : Union_binder α := x

@[simp] lemma Union_binder.mk_eq {α : Sort*} (x : α) : Union_binder.mk x = x := rfl

class has_Union (α : Sort*) (β : out_param $ Sort*) :=
(Union : α → β)

local notation `⋃` binders `, ` r:(scoped f, Union_binder.mk f) := has_Union.Union r

instance set_Union (ι : Sort*) (α : Type*) : has_Union (Union_binder $ ι → set α) (set α) :=
{ Union := set.Union }

instance set_bUnion (ι : Sort*) (p : ι → Prop) (α : Type*) :
  has_Union (Union_binder $ Π (x : ι), Union_binder $ p x → set α) (set α) :=
{ Union := λ f, set.Union (λ x, set.Union (λ h, f x h)) }

instance finset_Union (ι : Type*) [fintype ι] (α : Type*) [decidable_eq α] :
  has_Union (Union_binder $ ι → finset α) (finset α) :=
{ Union := finset.univ.bUnion }

instance finset_pred (ι : Type*) (p : ι → Prop) [fintype {x | p x}] (α : Type*) [decidable_eq α] :
  has_Union (Union_binder $ Π (x : ι), Union_binder $ p x → finset α) (finset α) :=
{ Union := λ f, ({x | p x}).to_finset.attach.bUnion (λ x, f x (by { convert x.property, simp })) }

instance finset_attach_bUnion (ι : Type*) (s : finset ι) (α : Type*) [decidable_eq α] :
  has_Union (Union_binder $ Π (x : ι), Union_binder $ x ∈ s → finset α) (finset α) :=
{Union := λ f, s.attach.bUnion (λ p, f p p.property) }

example (ι : Type*) (s : finset ι) (α : Type*) [decidable_eq α] (f : ι → finset α) :
  (⋃ (x ∈ s), f x) = s.bUnion f :=
by { ext, simp [has_Union.Union] }

example (ι : Type*) [fintype ι] (α : Type*) [decidable_eq α] (f : ι → finset α) :
  (⋃ x, f x) = finset.univ.bUnion f := rfl

example (ι ι' : Type*) (s : finset ι) (s' : finset ι') (α : Type*) [decidable_eq α] (f : ι → ι' → finset α) :
  (⋃ (x ∈ s), ⋃ (y ∈ s'), f x y) = s.bUnion (λ x, s'.bUnion (f x)) :=
by { ext, simp [has_Union.Union] }

example (ι ι' : Type*) (s : finset ι) [fintype ι'] (α : Type*) [decidable_eq α] (f : ι → ι' → finset α) :
  (⋃ (x ∈ s), ⋃ y, f x y) = s.bUnion (λ x, finset.univ.bUnion (f x)) :=
by { ext, simp [has_Union.Union] }

example (ι : Type*) (α : Type*) [decidable_eq α] (s : finset ι) (f : s → finset α) :
  (⋃ x (h : x ∈ s), f ⟨x, h⟩) = s.attach.bUnion f :=
by { ext, simp [has_Union.Union] }

--set_option pp.notation false

example (ι α : Type*) (f : ι → set α) :
  (⋃ x, f x) = {z | ∃ x, z ∈ f x} :=
by { ext, simp [has_Union.Union] }

-- Cannot combine unions into a single union with this approach:
example (ι ι' α : Type*) (f : ι → ι' → set α) :
--  (⋃ x y, f x y) = {z | ∃ x y, z ∈ f x y} :=
  (⋃ x, ⋃ y, f x y) = {z | ∃ x y, z ∈ f x y} :=
by { ext, simp [has_Union.Union] }

example (ι α : Type*) (s : set ι) (f : ι → set α) :
  (⋃ (x ∈ s), f x) = {z | ∃ x, x ∈ s ∧ z ∈ f x} :=
by { ext, simp [has_Union.Union] }

example (α : Type*) (f : ℕ → set α) :
  (⋃ (i < 5), f i) = {z | ∃ i, i < 5 ∧ z ∈ f i} :=
by { ext, simp [has_Union.Union] }

example (α : Type*) [decidable_eq α] (f : ℕ → finset α) :
  (⋃ (i < 5), f i) = (finset.range 5).bUnion f :=
by { ext, simp [has_Union.Union] }

-- rewrite works:
example (ι α : Type*) (s t : set ι) (f g : ι → set α) (h1 : s = t) (h2 : f = g) :
  (⋃ (x ∈ s), f x) = (⋃ (y ∈ t), g y) :=
begin
  rw [h1, h2],
end

-- rewrite works:
example (ι α : Type*) [decidable_eq α] (s t : finset ι) (f g : ι → finset α) (h1 : s = t) (h2 : f = g) :
  (⋃ (x ∈ s), f x) = (⋃ (y ∈ t), g y) :=
begin
  rw [h1, h2],
end

theorem Union_diff {ι β : Type*} (s : set β) (t : ι → set β) :
  (⋃ i, t i) \ s = ⋃ i, t i \ s :=
by { ext, simp [has_Union.Union] }

[Kyle Miller]

This code demonstrates a has_Union class that works for both set and finset. The only tradeoff seems to be that, like big_operators, you can only have one binder per union. So rather than ⋃ x y, f x y, you have to write ⋃ x, ⋃ y, f x y.

[Kyle Miller]

It also works for bounded quantification, like ⋃ (x ∈ s), f x. To pull this off, there is a special identity function called Union_binder to help typeclass search know which arguments are meant to be binders.

[Kyle Miller]

You can also do ⋃ (i < 5), f i as a finset union, which is fun.

[Kyle Miller]

I haven't done any large tests of whether there are any further problems when it comes to rewrites -- this version does have the complication that to do a Union for finset, it has to do s.attach.bUnion rather than just s.bUnion universally, since it's not able to peer into the term to decide whether the union is dependent on the proof of finset membership.

[Kyle Miller]

In principle, this technique seems like it should work for big_operators, too. That means we'd be able to write ∑ (x ∈ s), f x instead of ∑ x in s, f x. However, that's with the caveat that the sum would be dependent on x ∈ s... The ∑ (x : α), f x notation would have the same meaning as before.

[Kyle Miller]

I'm not sure exactly why this additional instance would be necessary yet, but if you have

instance finset_set (ι : Type*) (s : set ι) [fintype s] (α : Type*) [decidable_eq α] :
  has_Union (Union_binder $ Π (x : ι), Union_binder $ x ∈ s → finset α) (finset α) :=
{ Union := λ f, s.to_finset.attach.bUnion (λ x, f x (by simpa using x.property)) }

then you can do finset unions over finite sets:

example (ι α : Type*) [decidable_eq α] (s : set ι) [fintype s] (f : ι → finset α) :
  (⋃ (x ∈ s), f x) = s.to_finset.bUnion f :=
by { ext, simp [has_Union.Union] }

(similarly, we'd be able to do sums over finite sets)

[Yaël Dillies]

How does that interact with #11516?

[Kyle Miller]

@Yaël Dillies Oh good, you're already refactoring these things. I was going to ask you, actually, if you wanted to take this up and investigate whether we can switch over this (or something like it).

[Kyle Miller]

For set, I am hoping that the only problem is that this setup doesn't have multi-index unions -- do you think that's a big loss? There's probably some way to add them back in, but it's sort of brittle.

[Yaël Dillies]

What exactly are you expecting from this typeclass? I can think of a few things in this area:

• Homogeneize between set and finset. To me that's low priority, and I've actually worked against a bit as I'm trying to phase docs#finset.bUnion out of existence in favor of docs#finset.sup. An alternative scenario would be to actually extend the ⨆/⨅ to finsets, in which case having finset.bUnion/finset.bInter could make sense, at least in notation.
• Make bounded operators the primitive thing. Again, I've worked against that. #11516 is literally about ensuring the library really treats bounded operators as nested operators and not as things of their own.
• Fix the conditional supremum/infimum. This, to me, is high priority, because currently bounded conditional supremums do not do what you expect.

[Yaël Dillies]

I can already see a few problems with your implementation:

• It breaks the heuristic of how nested infinitary operators work. Well, big operators already do.
• Your set_bUnion instance has p : ι → Prop rather than p : ι → Sort*. Easily fixable, I think?
• finset.bUnion doesn't translate to your notation. It is propeq to it but not defeq. And if it translates, where will the coercion in example (s : finset ι) (f : ι → finset α) : set α := ⋃ i ∈ s, f i be inserted?
• It is using docs#finset.range rather than docs#finset.Iio. That should be easily fixable.
• I expect it to be generally less robust than the current simpler implementation.

[Kyle Miller]

I'd like there to be a uniform style of interface for various fold-like operations on sets, finsets, potentially multisets, and so on.

Unions/intersections are one test for this, but of course Sup/Inf would be great, too. Sums and products are another target, to give more freedom for what we are summing over (we could sum over a multiset with multiplicity).

[Kyle Miller]

• It breaks the heuristic of how nested infinitary operators work. Well, big operators already do.

Yes, when I said "this setup doesn't have multi-index unions" that's what I was referring to -- do you think this is a big loss?

• Your set_bUnion instance has p : ι → Prop rather than p : ι → Sort*. Easily fixable, I think?

Why would it be Sort*-valued? I mean, it could be, but the point of that instance is for bounded unions.

• finset.bUnion doesn't translate to your notation. It is propeq to it but not defeq. And if it translates, where will the coercion in example (s : finset ι) (f : ι → finset α) : set α := ⋃ i ∈ s, f i be inserted?

I didn't think it was high-priority for it to be finset.bUnion, so I'm not sure non-defeq is a problem here (as you said, you're wanting to phase out finset.bUnion).

For your example, you need to choose the interpretation with a type ascription with the way the code currently is written:

example {α ι : Type*} [decidable_eq α] (s : finset ι) (f : ι → finset α) : set α := ⋃ i ∈ s, (f i : set α)
example {α ι : Type*} [decidable_eq α] (s : finset ι) (f : ι → finset α) : set α := (⋃ i ∈ s, f i : finset α)

• It is using docs#finset.range rather than docs#finset.Iio. That should be easily fixable.

That's the sort of thing why I was going to ask you whether you'd look into this -- you've been looking at lattices and have done a lot with intervals. This is only a proof-of-concept.

• I expect it to be generally less robust than the current simpler implementation.

Please get back with examples where it's less robust, and hopefully they can be fixed. In any case, maybe even if it might be less robust, having a uniform interface for these things will help with ergonomics/usability across mathlib, so on balance it might still be better than what we have.