Zulip Chat Archive

Stream: new members

Topic: Using attach with fold


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Nov 20 2019 at 12:30):

I see, thanks!

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Nov 20 2019 at 13:22):

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

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 20 2019 at 13:28):

that theorem generalizes to bind indeed

view this post on Zulip Mario Carneiro (Nov 20 2019 at 13:29):

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

view this post on Zulip Bhavik Mehta (Nov 20 2019 at 13:31):

Oh! Big operators sounds very useful, thank you

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 20 2019 at 13:35):

the name is only useful if you think in monads

view this post on Zulip Mario Carneiro (Nov 20 2019 at 13:36):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 20 2019 at 13:40):

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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Nov 20 2019 at 13:46):

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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Nov 20 2019 at 13:50):

dsimp

view this post on Zulip Bhavik Mehta (Nov 20 2019 at 13:51):

Awesome thanks

view this post on Zulip 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.

view this post on Zulip 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