Zulip Chat Archive

Stream: general

Topic: finsets, unions, and cardinality


Jeremy Avigad (Jan 12 2021 at 17:07):

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 (Jan 12 2021 at 17:58):

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

Mario Carneiro (Jan 12 2021 at 17:59):

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

Jeremy Avigad (Jan 12 2021 at 18:09):

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

Kyle Miller (Jan 12 2021 at 18:12):

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 (Jan 12 2021 at 18:43):

finset.fUnion ;-)

Adam Topaz (Jan 12 2021 at 18:52):

finset.finUnion?

Adam Topaz (Jan 12 2021 at 18:52):

seems to match *set.*Union

Mario Carneiro (Jan 12 2021 at 19:01):

I prefer bUnion since it matches the set naming

Aaron Anderson (Jan 12 2021 at 19:35):

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

Adam Topaz (Jan 12 2021 at 19:44):

Isn't sup just for two things?

Kyle Miller (Jan 12 2021 at 20:02):

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 (Jan 12 2021 at 20:50):

Do we have a lemma equating them?

Kyle Miller (Jan 12 2021 at 22:45):

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 (Jan 13 2021 at 21:31):

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 α) :
  (is, 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 α) :
  ((is) (js'), f i j) = s.bind (λ x, s'.bind (λ y, f x y)) :=
by { ext a, simp [has_Union.Union] }

Eric Wieser (Jan 13 2021 at 23:20):

Why do you have f in the typeclass arguments?

Eric Wieser (Jan 13 2021 at 23:22):

Oh, I guess the variant instances answer that

Bryan Gin-ge Chen (Jan 14 2021 at 15:09):

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

Kyle Miller (Jan 14 2021 at 17:56):

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 α) : (is, f i) = s.bind f := rfl

Kyle Miller (Jan 19 2021 at 21:03):

#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 (Jan 20 2021 at 09:40):

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 (Jan 20 2021 at 18:03):

@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 (Jan 25 2021 at 01:57):

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 (Jan 25 2021 at 02:38):

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 (Jan 25 2021 at 02:42):

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

Hanting Zhang (Jan 25 2021 at 02:47):

Oops. My bad.

Alex J. Best (Jan 25 2021 at 02:47):

I agree its not an obvious name though!

Mario Carneiro (Jan 25 2021 at 02:48):

it's not an easy thing to name

Mario Carneiro (Jan 25 2021 at 02:49):

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 (Jan 25 2021 at 02:49):

unfortunately this clashes in some places with naming on set

Mario Carneiro (Jan 25 2021 at 02:50):

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 (Jan 25 2021 at 02:52):

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 (Jan 25 2021 at 02:54):

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 (Jan 25 2021 at 02:57):

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 (Jan 25 2021 at 02:57):

list.filter_map is a naming nightmare

Yakov Pechersky (Jan 25 2021 at 02:58):

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

Mario Carneiro (Jan 25 2021 at 02:59):

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

Mario Carneiro (Jan 25 2021 at 02:59):

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

Hanting Zhang (Jan 26 2021 at 05:58):

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 (Jan 26 2021 at 06:05):

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 (Jan 26 2021 at 06:07):

Thanks for doing this :smile:!

Kyle Miller (Jan 27 2021 at 01:31):

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 α) : (xs, f x) = {y : β |  x, x  s  y  f x} :=
by { ext, simp [Union.union] }

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

example {α β γ} (s : set α) (t : α  β  set γ) :
  (y (xs), t x y) = {z : γ |  (xs) 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 : (xs, t x) = s.bUnion t := rfl

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

example {γ : Type*} [decidable_eq γ] (u : α  β  finset γ) (z : γ) :
  z  ((xs) (yt 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  ((xs) y, t x y)   (xs) 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 (Jan 27 2021 at 02:25):

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 (Jan 27 2021 at 02:29):

(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 (Jan 27 2021 at 04:22):

@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 (Jan 27 2021 at 08:08):

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

Johan Commelin (Jan 27 2021 at 08:10):

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 (Jan 27 2021 at 08:27):

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 (Jan 27 2021 at 19:29):

@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 (Jan 27 2021 at 19:41):

@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 (Jan 27 2021 at 19:42):

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

Kyle Miller (Jan 27 2021 at 19:45):

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 (Jan 27 2021 at 19:48):

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


Last updated: Dec 20 2023 at 11:08 UTC