finsets, unions, and cardinality

Stream: general

[Jeremy Avigad]

Is there a good way to deal with finset-indexed unions of finsets, their cardinalities, and so on? I don't see much in the library -- only some workarounds with supr, and some cardinality operations on fintypes. Am I missing something obvious?

[Mario Carneiro]

You can use finset.bind to take a finset union of a finset

[Mario Carneiro]

and we have docs#finset.card_bind to prove a cardinality theorem about it

[Jeremy Avigad]

Ah, I forgot. s.bind t is what we call bUnion when we talk about sets. Someone should document that! Thanks.

[Kyle Miller]

I've been using finset.bind recently, and I appreciate where the name comes from, but if a sufficiently motivated individual were up to a rename, would anyone be opposed to it being called something like finset.Union?

[Kevin Buzzard]

finset.fUnion ;-)

[Adam Topaz]

finset.finUnion?

[Adam Topaz]

seems to match *set.*Union

[Mario Carneiro]

I prefer bUnion since it matches the set naming

[Aaron Anderson]

We also have finset.sup, shouldn't this be the same thing?

[Adam Topaz]

Isn't sup just for two things?

[Kyle Miller]

It looks like finset.bind is a specialized finset.sup.

def finset.bind (s : finset α) (t : α → finset β) : finset β
def finset.sup (s : finset β) (f : β → α) : α

The first is defined using multiset.bind (which is iterated unions of multisets), and the second by iterated unions of finsets. Computationally, the second one removes duplicates as it goes.

[Eric Wieser]

Do we have a lemma equating them?

[Kyle Miller]

It didn't look like it, so I created #5717. I'm waiting to see if mathlib still compiles labeling it with awaiting-review.

[Kyle Miller]

Instead of (or in addition to) renaming finset.bind, there's an option of reworking the notation for Union to use a typeclass and use finset.bind to implement it. I got something that seems to work for both sets and finsets (with the correct decidability requirements):

import order.complete_lattice
import data.set.lattice
import data.finset.basic
import data.fintype.basic

class has_Union (α : Type*) (β : out_param $ Type*) (f : α) :=
(Union : β)

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

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

lemma set.mem_Union' {ι β : Type*} {x : β} {s : ι → set β} : x ∈ (⋃i, s i) ↔ ∃ i, x ∈ s i :=
set.mem_Union

instance finset.has_Union_prop_nodep (p : Prop) (β : Type*) (s : finset β) :
  has_Union (p → finset β) (finset β) (λ h, s) :=
{ Union := s }

instance finset.has_Union_prop (p : Prop) [decidable p] (β : Type*) (f : p → finset β) :
  has_Union (p → finset β) (finset β) f :=
{ Union := if h : p then f h else ∅ }

instance finset.has_bUnion_nodep (ι : Type*) (s : finset ι) (β : Type*) [decidable_eq β]
  (f : ι → finset β) :
  has_Union (Π (x : ι), finset β) (finset β) (λ x, ⋃(h : x ∈ s), f x) :=
{ Union := (finset.univ : finset (s : set ι)).bind (λ x, f x.1) }

instance finset.has_bUnion (ι : Type*) (s : finset ι) (β : Type*) [decidable_eq ι] [decidable_eq β]
  (f : Π (x : ι), x ∈ s → finset β) :
  has_Union (Π (x : ι), finset β) (finset β) (λ x, ⋃(h : x ∈ s), f x h) :=
{ Union := (finset.univ : finset (s : set ι)).bind (λ x, f x.1 x.2) }

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

lemma finset.bUnion_eq_bind (ι α : Type*) [decidable_eq α]
  (s : finset ι) (f : ι → finset α) :
  (⋃i∈s, f i) = s.bind f :=
by { ext a, simp [has_Union.Union] }

lemma finset.Union_eq_univ_bind (ι α : Type*) [fintype ι] [decidable_eq α]
  (f : ι → finset α) :
  (⋃i, f i) = finset.univ.bind f :=
by { ext a, simp [has_Union.Union] }

lemma finset.bUnion_bUnion_eq (ι ι' α : Type*) [decidable_eq α]
  (s : finset ι) (s' : finset ι') (f : ι → ι' → finset α) :
  (⋃(i∈s) (j∈s'), f i j) = s.bind (λ x, s'.bind (λ y, f x y)) :=
by { ext a, simp [has_Union.Union] }

[Eric Wieser]

Why do you have f in the typeclass arguments?

[Eric Wieser]

Oh, I guess the variant instances answer that

[Bryan Gin-ge Chen]

Getting the notation to work for both sets and finsets (and multisets?) seems like a great change to me!

[Kyle Miller]

If ⋃i∈s, f i means to union over every i with multiplicity when s is a multiset, then these two additional instances give fancy notation for multiset.bind:

instance multiset.has_Union_prop_nodep (p : Prop) (β : Type*) (s : multiset β) :
  has_Union (p → multiset β) (multiset β) (λ h, s) :=
{ Union := s }

instance multiset.has_bUnion (ι : Type*) (s : multiset ι) (β : Type*) [decidable_eq β]
  (f : ι → multiset β) :
  has_Union (ι → multiset β) (multiset β) (λ x, ⋃(h : x ∈ s), f x) :=
{ Union := s.bind f }

lemma multiset.bUnion_eq_bind (ι α : Type*) [decidable_eq α]
  (s : multiset ι) (f : ι → multiset α) : (⋃i∈s, f i) = s.bind f := rfl

[Kyle Miller]

#5813 is renaming multiset.bind to multiset.bUnion and finset.bind to finset.bUnion.

(Is there a way to create a definition that causes a deprecation warning to show up if you use it? Or maybe a linter error?)

[Anne Baanen]

Kyle Miller said:

(Is there a way to create a definition that causes a deprecation warning to show up if you use it? Or maybe a linter error?)

It might be possible to adapt the >/≥` linter to do so. But in this case, the mathlib development style is to just get rid of the old name and let the existing usages cause an error. Then the new name will be used soon enough.

[Kyle Miller]

@Bhavik Mehta pointed out that multiset.bind is not actually the union of the indexed family of multisets, but the sum, so #5813 is now just for renaming finset.bind to finset.bUnion.

It might be good having the corresponding multiset union of an indexed family:

def multiset.bUnion {α β : Type*} [decidable_eq β] (s : multiset α) (t : α → multiset β) : multiset β :=
(s.map t).sup

(It turns out finset.sup and multiset.sup have different interfaces, hence the multiset.map in there.)

[Bryan Gin-ge Chen]

Any objections to #5813 (renaming finset.bind to finset.bUnion)? It's a big change and likely to break a lot of code that depends on mathlib, but should make the function much easier to find.

(One thing we should also really do that would help with that is greatly expand the module docstring of data.finset.basic.)

[Hanting Zhang]

Yes, please rename. I couldn't find finset.bUnion in any searches. It seems like the most obvious name. Also why is finset.attach called finset.attach? Why is it not finset.to_idk_fintype_val? (I doubt this is any better.)

[Alex J. Best]

It doesn't spit out a fintype though right? I guess it is analogous to docs#list.attach

[Hanting Zhang]

Oops. My bad.

[Alex J. Best]

I agree its not an obvious name though!

[Mario Carneiro]

it's not an easy thing to name

[Mario Carneiro]

A lot of definitions on finset (including finset.bind) got their names because they are analogous to definitions on multiset and/or list

[Mario Carneiro]

unfortunately this clashes in some places with naming on set

[Mario Carneiro]

and for the most part finset prefers set like naming over list like, for example the empty thing is called list.nil, multiset.zero, finset.empty and set.empty

[Mario Carneiro]

I think we should try to minimize naming variation where we can, so if this is called list.attach already then the finset version should be called finset.attach unless there is a much stronger name association on sets

[Alex J. Best]

Yeah at least something like map_subtype_mem seems vaguely more descriptive than attach, if you asked me what list.attach does I'd never be able to guess. Of course if things have well known name in Haskell/FP that's a reason to use a less descriptive name if its to remain consistent with those languages, but it doesn't seem like that is the case here?

[Mario Carneiro]

I think that definitions should have single word names (or at least single name segment names) where possible, because otherwise it makes it much more confusing when reading theorems about the definition

[Mario Carneiro]

list.filter_map is a naming nightmare

[Yakov Pechersky]

Is it possible to have both finset.bind and finset.bUnion with aliases?

[Mario Carneiro]

yes, although does that mean we're duplicating the theorems too?

[Mario Carneiro]

if we do add an alias we still shouldn't use it in mathlib

[Hanting Zhang]

In lieu of @Bryan Gin-ge Chen's comment on expanding finset.basic docs, I've made a very rough PR (#5893) that is not finished. I'm not entirely sure what standards there are for writing paragraphs upon paragraphs of documentation, so I've just taken my best shot at it for now.

Anyone who has time to add something, please do!

[Alex J. Best]

Looks good so far, unfinished PRs are Ok, you can tag it with WIP and help-wanted if you want.
You can also preview (roughly) how it will look using @Bryan Gin-ge Chen s previewer https://observablehq.com/@bryangingechen/github-lean-file-viewer?url=%22https://github.com/leanprover-community/mathlib/pull/5893/%22#docs here it looks like the numbered lists aren't displaying properly, I think markdown syntax needs to be like

1. blah
2. blah blah

to work properly

[Alex J. Best]

Thanks for doing this :smile:!

[Kyle Miller]

Here's another attempt at generalized big union notation, and it seems to work, but it should be tested with some real math rather than my basic examples. One wart, to make the code simpler, is to have a default instance for the Union class called Union.failure to help with defining the instances for finset bounded unions -- the issue has to do with missing decidable instances.

A cool thing is that you can define instances for unioning over properties whose support is finite: (⋃(i<10), finset.range i) = finset.range 9. It can even handle dependent finite unions: (⋃i (h:i<10), ({⟨i, h⟩} : finset (fin 10))) = finset.univ.

I imagine this design pattern would work for summation and product notation, too.

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

universes u v w

namespace new_Union

class Union {α : Sort u} (x : α) (γ : out_param $ Sort v) :=
(union : γ)

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

/-- To have bounded unions, there needs to be a `Union.union` instance for the internal
union (the `⋃(h : x ∈ s), f x`) even when one doesn't technically exist, for example
due to a lack of decidable equality for `finset`.  As a hack, we have this `Union.failure`
type that gives a low-priority default instance. -/
structure Union.failure (α : Sort u) := (f : α)

@[priority 0]
instance Union.default_failure (α : Sort u) (x : α) : Union x (Union.failure α) :=
{ union := Union.failure.mk x }

instance set_Union {α} {β} (f : α → set β) : Union f (set β) :=
{ union := set.Union f }

instance fintype_Union {α} {β} [fintype α] (t : α → finset β) [decidable_eq β] :
  Union t (finset β) :=
{ union := finset.univ.bUnion t }

instance finset_dep_bUnion {α} {β} (s : finset α) [decidable_eq β]
  (t : Π(x : α) (h : x ∈ s), finset β) :
  Union (λ x, Union.union (λ (h : x ∈ s), t x h)) (finset β) :=
{ union := s.attach.bUnion (λ x, t x.1 x.2) }

instance finset_bUnion {α} {β} (s : finset α) (t : α → finset β) [decidable_eq β] :
  Union (λ x, Union.union (λ (h : x ∈ s), t x)) (finset β) :=
{ union := s.bUnion t }

instance finset_dep_bUnion_fin_prop {α : Type*} {β}
  (p : α → Prop) [decidable_pred p] [fintype {x | p x}]
  (t : Π(x : α), p x → finset β) [decidable_eq β] :
  Union (λ x, Union.union (λ (h : p x), t x h)) (finset β) :=
{ union := (finset.univ : finset {x | p x}).bUnion (λ x, t x.1 x.2) }

instance finset_bUnion_fin_prop {α : Type*} {β}
  (p : α → Prop) [decidable_pred p] [fintype {x | p x}]
  (t : α → finset β) [decidable_eq β] :
  Union (λ x, Union.union (λ (h : p x), t x)) (finset β) :=
{ union := (finset.univ : finset {x | p x}).bUnion (λ x, t x.1) }

section set_test

example {α β} (f : α → set β) : (⋃x, f x) = {y : β | ∃ x, y ∈ f x} :=
by { ext, simp [Union.union] }

example {α β} (f : α → set β) (s : set α) : (⋃x∈s, f x) = {y : β | ∃ x, x ∈ s ∧ y ∈ f x} :=
by { ext, simp [Union.union] }

example {α β γ} (s : set α) (t : α → β → set γ) :
  (⋃(x∈s) y, t x y) = {z : γ | ∃ (x∈s) y, z ∈ t x y} :=
by { ext, simp [Union.union] }

example {α β γ} (s : set α) (t : α → β → set γ) :
  (⋃y (x∈s), t x y) = {z : γ | ∃ (x∈s) y, z ∈ t x y} :=
by { ext, simp [Union.union], tidy, }

end set_test

section finset_test

variables {α β : Type*} [decidable_eq β] (t : α → finset β) (s : finset α)

example : (⋃x∈s, t x) = s.bUnion t := rfl

example [fintype α] : (⋃x, t x) = finset.univ.bUnion t := rfl

example {γ : Type*} [decidable_eq γ] (u : α → β → finset γ) (z : γ) :
  z ∈ (⋃(x∈s) (y∈t x), u x y) ↔  ∃ (x ∈ s) (y ∈ t x), z ∈ u x y :=
by { simp [Union.union] }

example {γ} [decidable_eq γ] (t : α → β → finset γ) [fintype β] (z : γ) :
  z ∈ (⋃(x∈s) y, t x y) ↔ ∃ (x∈s) y, z ∈ t x y :=
by { simp [Union.union], }

example : (⋃(i<10), finset.range i) = finset.range 9 :=
by { ext, simp [Union.union], tidy, omega, }

example : (⋃i (h:i<10), ({⟨i, h⟩} : finset (fin 10))) = finset.univ :=
by { ext, simp [Union.union], tidy, }

end finset_test

end new_Union

[Kyle Miller]

It works for summation notation, too. For example, 2 * (∑(i ≤ n), i) = n * (n + 1).

This also gives a nice way to do summations over multisets. We can define (∑ (x ∈ s), f x) = (s.map f).sum, where the sum is done with multiplicity. (This is also another notation for multiset.bind, since it's defined to be the sum of an indexed family of multisets.)

import data.finset.basic
import data.fintype.basic
import algebra.big_operators.basic
import tactic

universes u v w

namespace new_sum

class has_sum {α : Sort u} (x : α) (γ : out_param $ Sort v) :=
(sum : γ)

local notation `∑` binders `, ` r:(scoped f, has_sum.sum f) := r

/-- This is a hack to help define bounded sums.  Try removing it to see why it's necessary. -/
structure has_sum.failure (α : Sort u) := (f : α)

@[priority 0]
instance has_sum.default_failure (α : Sort u) (x : α) : has_sum x (has_sum.failure α) :=
{ sum := has_sum.failure.mk x }

instance fintype_sum {α} {β} [fintype α] [add_comm_monoid β] (t : α → β) :
  has_sum t β :=
{ sum := finset.univ.sum t }

instance finset_dep_sum {α} {β} (s : finset α) [add_comm_monoid β]
  (t : Π(x : α) (h : x ∈ s), β) :
  has_sum (λ x, has_sum.sum (λ (h : x ∈ s), t x h)) β :=
{ sum := s.attach.sum (λ x, t x.1 x.2) }

instance finset_sum {α} {β} (s : finset α) (t : α → β) [add_comm_monoid β] :
  has_sum (λ x, has_sum.sum (λ (h : x ∈ s), t x)) β :=
{ sum := s.sum t }

instance finset_dep_sum_fin_prop {α : Type*} {β} [add_comm_monoid β]
  (p : α → Prop) [decidable_pred p] [fintype {x | p x}]
  (t : Π(x : α), p x → β) :
  has_sum (λ x, has_sum.sum (λ (h : p x), t x h)) β :=
{ sum := (finset.univ : finset {x | p x}).sum (λ x, t x.1 x.2) }

instance finset_sum_fin_prop {α : Type*} {β} [add_comm_monoid β]
  (p : α → Prop) [decidable_pred p] [fintype {x | p x}]
  (t : α → β) :
  has_sum (λ x, has_sum.sum (λ (h : p x), t x)) β :=
{ sum := (finset.univ : finset {x | p x}).sum (λ x, t x.1) }

lemma sum_le_eq_sum_range {n : ℕ} (f : ℕ → ℕ) : (∑(i ≤ n), f i) = (∑(i ∈ finset.range (n + 1)), f i) :=
begin
  simp [has_sum.sum],
  rw ←finset.sum_image,
  congr, ext, simp, omega,
  tidy,
end

lemma sum_le_succ {n : ℕ} (f : ℕ → ℕ) : (∑(i ≤ n + 1), f i) = f (n + 1) + (∑(i ≤ n), f i) :=
begin
  repeat { rw sum_le_eq_sum_range, },
  dunfold has_sum.sum,
  rw finset.sum_range_succ,
end

example {n : ℕ} : 2 * (∑(i ≤ n), i) = n * (n + 1) :=
begin
  induction n,
  { rw sum_le_eq_sum_range, simp [has_sum.sum], },
  { rw [sum_le_succ, mul_add, n_ih, nat.succ_eq_add_one],
    ring, },
end

example {α β} (f : α → multiset β) (s : finset α) : (∑ (x ∈ s), f x) = s.val.bind f :=
rfl

/-- Sum over a multiset with repeats -/
instance multiset_sum {α} {β} (s : multiset α) (t : α → β) [add_comm_monoid β] :
  has_sum (λ x, has_sum.sum (λ (h : x ∈ s), t x)) β :=
{ sum := (s.map t).sum }

example {α β} (f : α → multiset β) (s : multiset α) : (∑ (x ∈ s), f x) = s.bind f :=
rfl

end new_sum

[Kyle Miller]

(A downside with this right now is that lemma statements that use the notation are in terms of has_sum.sum, where the current notation is guaranteed to be finset.sum, so you can easily use it without open_locale big_operators.)

[Johan Commelin]

@Kyle Miller that looks really nice! And those downsides aren't very big downsides to me.
If you have a generic class for using some sort of notation, like Union.union or has_sum.sum etc, then I don't think it needs to be local notation anymore.

[Eric Wieser]

Does your sum/union notation allow arbitrarily nested dependent binders like are allowed today? Or only ones that match your patterns?

[Johan Commelin]

I guess the litmus test would be to see whether we need to change 95% of the library when switching to this or only 5%.

[Eric Wieser]

It would be cool if something like docs#finset.sum_hom were part of the has_sum typeclass too, since that would unify a lot of lemmas

[Kyle Miller]

@Eric Wieser It supports arbitrary nesting. The patterns are applied "outside-in" so to speak. There are some examples of nesting in the union example.

[Kyle Miller]

@Johan Commelin Switching to has_union, starting with just set.Union, probably should be a small change. Switching finset.bUnion uses to has_union.union notation would probably be not so much bigger than the rename to finset.bUnion (something like 25 files). I'm not sure how much effort summation/product notation would be yet.

[Johan Commelin]

back when I introduced notation for finset.sum it was an "OK" refactor, I think

[Kyle Miller]

Eric Wieser said:

It would be cool if something like docs#finset.sum_hom were part of the has_sum typeclass too, since that would unify a lot of lemmas

Either that or a companion typeclass that indicates that it's a "lawful" sum would be nice. I'm not sure how you'd fit it into the has_sum typeclass itself, but let me know if you find a way.

[Kyle Miller]

Another interesting application is that you can sum over sets that have a fintype instance without having to write to_finset yourself:

instance finite_set_sum {α} {β} (s : set α) [fintype s] (t : α → β) [add_comm_monoid β] :
  has_sum (λ x, has_sum.sum (λ (h : x ∈ s), t x)) β :=
{ sum := s.to_finset.sum t }

lemma sum_neighbors (V : Type*) [fintype V] (G : simple_graph V) (v : V) :
  (∑(w ∈ G.neighbor_set v), 1) = G.degree v :=
by  simp [has_sum.sum],

(Then we can get rid of the combinatorial explosion of definitions like simple_graph.neighbor_finset and maybe rename simple_graph.neighbor_set to just simple_graph.neighbors.)