## Stream: new members

### Topic: Using attach with fold

#### Bhavik Mehta (Nov 20 2019 at 12:14):

I'm trying to prove that if z is disjoint from everything in A, then z is disjoint from the union of the things in A:

lemma disjoint_all {α} [decidable_eq α] {A : finset (finset α)} {z : finset α} (h : ∀ x ∈ A, disjoint x z) : disjoint (A.fold (∪) ∅ id) z :=
begin
apply finset.induction_on A,
rw finset.fold_empty,
apply finset.disjoint_empty_left,
intros a s h₂ k,
rw [finset.fold_insert h₂],
rw finset.disjoint_union_left,
split,
apply h,
sorry,
exact k
end


It was all going really well, but I just need to show that the element we're inserting for the fold has come from A - which should be obvious because we're folding over A. (Not entirely sure why induction_on isn't set up so that I can use this...) I'm pretty sure this is the sort of thing attach is meant to fix, but letting B := A.attach means it's no longer clear to me how the induction should work - if I do induction on B how can I prove that the thing we get is equivalent?

#### Mario Carneiro (Nov 20 2019 at 12:18):

You might find it easier working with A.bind id as the union of A, or perhaps ⋃ x ∈ A, ↑x

#### Mario Carneiro (Nov 20 2019 at 12:22):

You need to do induction generalizing h:

lemma disjoint_all {α} [decidable_eq α] {A : finset (finset α)} {z : finset α} (h : ∀ x ∈ A, disjoint x z) : disjoint (A.fold (∪) ∅ id) z :=
begin
revert h,
apply finset.induction_on A,
{ intro,
rw finset.fold_empty,
apply finset.disjoint_empty_left },
{ intros a s h₂ ih h,
rw [finset.fold_insert h₂],
rw finset.disjoint_union_left,
split,
{ exact h _ (finset.mem_insert_self _ _) },
{ exact ih (λ x hx, h _ (finset.mem_insert_of_mem hx)) } }
end


I see, thanks!

#### Bhavik Mehta (Nov 20 2019 at 12:31):

I'm surprised that the generalisation trick works, but it makes sense! I can't use your latter suggestion for the union, since I do need finiteness in another part of my proof, but I'll have a go with bind as well.

#### Reid Barton (Nov 20 2019 at 13:21):

Not sure how helpful this is, but I think the original proof is misguided. You shouldn't be using induction to prove this at all. Instead, you should have a lemma that tells you when something is an element of A.fold (∪) ∅ id (which you will prove by induction).

#### Mario Carneiro (Nov 20 2019 at 13:22):

Using A.bind id basically solves this problem, since it already has the requisite lemmas

#### Reid Barton (Nov 20 2019 at 13:22):

Then this proof becomes easy (intro a, apply lemmas about what it means for a to be an element of various finsets).

#### Reid Barton (Nov 20 2019 at 13:24):

The difference is that knowing the elements of A.fold (∪) ∅ id totally characterizes it as a set, so you won't have to do another induction for the next lemma like this one that you need.

#### Reid Barton (Nov 20 2019 at 13:24):

Yeah, I'm a little surprised there isn't already a definition like A.Union := A.bind id.

#### Mario Carneiro (Nov 20 2019 at 13:27):

Me too, but really I don't think Union will be able to provide better lemmas than bind already has, when specialized to id

#### Bhavik Mehta (Nov 20 2019 at 13:27):

I think your criticism is fair, but this lemma was meant to be used when proving that the cardinality of the union is the sum of the cardinalities when the sets are all disjoint - so this seemed like the natural way of going about it. Perhaps with broader context using bind might turn out better, I will try further. I think I will need to characterise elements at some point anyway.

#### Mario Carneiro (Nov 20 2019 at 13:28):

that theorem generalizes to bind indeed

#### Mario Carneiro (Nov 20 2019 at 13:29):

in fact it already exists - finset.card_bind in algebra.big_operators

#### Bhavik Mehta (Nov 20 2019 at 13:31):

Oh! Big operators sounds very useful, thank you

#### Reid Barton (Nov 20 2019 at 13:35):

Yeah, mainly I think finset.bind id is not that easily discoverable, especially because bind is a notion which doesn't really appear in math.

#### Mario Carneiro (Nov 20 2019 at 13:35):

the name is only useful if you think in monads

#### Mario Carneiro (Nov 20 2019 at 13:36):

the notion of course does appear in math, but it's called "indexed union"

#### Reid Barton (Nov 20 2019 at 13:37):

Tangentially related story. I wanted to prove that if o : roption α and a ∈ o and b ∈ o then a = b. I didn't see it looking through data.pfun so I defined mem_unique and proved it.

#### Bhavik Mehta (Nov 20 2019 at 13:37):

Yeah I was familiar with the notion of bind, but my cardinality theorem felt like the maths proof should use induction

#### Reid Barton (Nov 20 2019 at 13:37):

That worked fine but then Lean gave an error on this later line:

theorem mem_unique : relator.left_unique ((∈) : α → roption α → Prop)


#### Reid Barton (Nov 20 2019 at 13:38):

It's actually exactly the same type but my eyes were looking for a ∈ o → b ∈ o → a = b

#### Bhavik Mehta (Nov 20 2019 at 13:38):

Also I don't think I saw theorems about cardinality of bind, but maybe I looked in the wrong place

#### Mario Carneiro (Nov 20 2019 at 13:39):

I think it has happened to me on at least three separate occasions that I prove a lemma and end up finding that it already exists because the name clashes

#### Mario Carneiro (Nov 20 2019 at 13:40):

I also wouldn't have thought to look there for it; I grepped for card_bind

#### Mario Carneiro (Nov 20 2019 at 13:41):

it makes sense in hindsight, because that's where finset.sum is defined, which is required for the statement

#### Bhavik Mehta (Nov 20 2019 at 13:46):

It wasn't required for my statement :P But yeah this helps a lot, thanks both

#### Bhavik Mehta (Nov 20 2019 at 13:49):

Tangential: if my goal has something like id a or (λ x, _) y, sometimes lean doesn't unify it how I want - what's the tactic I need for simplifying those terms? (I know simp would do it, but it feels like overkill and might screw up other terms)

#### Mario Carneiro (Nov 20 2019 at 13:50):

dsimp

Awesome thanks

#### Johan Commelin (Nov 20 2019 at 15:00):

the name is only useful if you think in monads

Make that CS monads, because the monads that do occur in maths use different terminology, I think.

#### Bhavik Mehta (Nov 21 2019 at 09:47):

You might find it easier working with A.bind id as the union of A, or perhaps ⋃ x ∈ A, ↑x

Using bind turned out to be a lot nicer, thank you!

Last updated: May 09 2021 at 18:17 UTC