Using attach with fold

Stream: new members

[Bhavik Mehta]

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]

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

[Mario Carneiro]

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

[Bhavik Mehta]

I see, thanks!

[Bhavik Mehta]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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]

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]

that theorem generalizes to bind indeed

[Mario Carneiro]

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

[Bhavik Mehta]

Oh! Big operators sounds very useful, thank you

[Reid Barton]

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]

the name is only useful if you think in monads

[Mario Carneiro]

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

[Reid Barton]

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]

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

[Reid Barton]

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

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

[Reid Barton]

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

[Bhavik Mehta]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

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]

dsimp

[Bhavik Mehta]

Awesome thanks

[Johan Commelin]

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]

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!