## Stream: maths

### Topic: finset puzzle

#### Kevin Buzzard (Jan 24 2020 at 18:41):

import data.finset

example (α : Type*) (s : finset α) (β : Type*) [decidable_eq β]
(f : α → finset β) :
finset.bind s f = finset.sup s f  := sorry

-- or to put it another way
example (α : Type*) (β : Type*) [decidable_eq β] :
@finset.bind α β _ = @finset.sup (finset β) α _  := sorry


There are two different ways to take a finite union of finite sets. Trying to prove directly that they are equal seems hard to me -- but am I missing something? Perhaps one should prove instead that they have the same elements?

#### Johan Commelin (Jan 24 2020 at 18:42):

Yes, use ext

#### Kevin Buzzard (Jan 24 2020 at 18:45):

This came up when I was trying to prove this:

import data.mv_polynomial

example {R : Type*} [comm_semiring R] {σ : Type*} {p : mv_polynomial σ R}
[decidable_eq σ] :
mv_polynomial.vars p = p.support.bind finsupp.support := sorry


vars is something in the mv_polynomial API which I had not come across until the other day, but its interface seems very basic. Chris' instinct was to use bind to do unions like this -- but apparently it wasn't Johannes'. Of course as long as the API is there it doesn't matter, but when Chris proved for me that evaluating a polynomial at two different assignments of the variables which agree on the variables of the polynomial will give the same answer, he used bind and it came out really nicely.

#### Kevin Buzzard (Jan 24 2020 at 18:46):

gaargh, finset.mem_sup is not there because it's working in some arbitrary lattice

#### Kevin Buzzard (Jan 24 2020 at 18:48):

⊢ (∃ (i : α) (H : i ∈ s), a ∈ f i) ↔ a ∈ finset.sup s f


is what I'm left with

#### Kevin Buzzard (Jan 24 2020 at 18:49):

the sup is defined as a fold over union.

#### Johan Commelin (Jan 24 2020 at 18:49):

Is there a mem_fold?

#### Kevin Buzzard (Jan 24 2020 at 18:50):

I just don't know whether I'm supposed to be digging this low. All I want to prove is that evaluating a polynomial at two different assignments which agree on all the variables of the polynomial gives the same answer :-)

#### Johan Commelin (Jan 24 2020 at 18:50):

So, sorry the statement and feed it to an UG at xena (-;

#### Kevin Buzzard (Jan 24 2020 at 18:53):

There's no mem_fold anywhere. I could prove it by induction I guess :-/ But when I launched into a proof the other day involving evaluations of mv_polynomials, Mario just came along and proved it with a very well-judged simp, and at Xena on Thursday when we were proving that the evaluations were equal if the assignments agreed on the support (as defined by bind) Chris stopped at some point and said "automation should do it from here". I am not sure I understand the full power of simp with these things.

#### Kevin Buzzard (Jan 24 2020 at 19:00):

oh I see what to do -- there is sup_le and le_sup and those should give it me.

#### Kevin Buzzard (Jan 24 2020 at 19:30):

gaargh le_sup isn't enough. I'm left with

1 goal
α : Type u_1,
s : finset α,
β : Type u_2,
_inst_2 : decidable_eq β,
f : α → finset β,
x : β,
hx : x ∈ finset.sup s f
⊢ ∃ (a : α) (H : a ∈ s), x ∈ f a


#### Floris van Doorn (Jan 24 2020 at 19:57):

Here is a proof assuming decidable equality on \a:

import data.finset

example (α : Type*) (s : finset α) (β : Type*) [decidable_eq α] [decidable_eq β]
(f : α → finset β) : finset.bind s f = finset.sup s f  :=
finset.induction_on s rfl (λ x s hx IH, by simp [IH])


#### Floris van Doorn (Jan 24 2020 at 20:07):

And here is a proof without that assumption:

import data.finset

example (α : Type*) (s : finset α) (β : Type*) [decidable_eq β]
(f : α → finset β) : finset.bind s f = finset.sup s f :=
begin
apply le_antisymm,
{ intro y, rw finset.mem_bind, rintro ⟨x, hx, hy⟩, have := @finset.le_sup _ _ _ _ f _ hx, exact this hy },
{ refine finset.sup_le _, intros x hx y hy, rw finset.mem_bind, exact ⟨x, hx, hy⟩ }
end


#### Floris van Doorn (Jan 24 2020 at 20:08):

You indeed also need sup_le.

#### Kevin Buzzard (Jan 24 2020 at 21:36):

Thanks a lot Floris. What frustrates me is that I still can't do an arbitrary puzzle like this immediately. Mulling things over I wondered whether it was worth proving that if you had a predicate on lattices with the property that P(x union y) was true iff P(x) or P(y) was true then some statement about sups was true

#### Kevin Buzzard (Jan 24 2020 at 21:37):

True for sup iff true for one of the elements. Need P(bot) false too

#### Kevin Buzzard (Jan 24 2020 at 22:01):

@Floris van Doorn do you think it's crazy to prove the vars question and I should instead just re-define mv_polynomial.vars? Chris seemed to think that the bind version was much easier to work with. See for example his (untidied) proof of the thing I needed yesterday: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Algebraic.20geometry.20course/near/186420269

#### Mario Carneiro (Jan 25 2020 at 00:34):

@Floris van Doorn Here's a shorter proof without the assumption:

example (α : Type*) (s : finset α) (β : Type*) [decidable_eq β]
(f : α → finset β) : finset.bind s f = finset.sup s f  :=
by classical; exact finset.induction_on s rfl (λ x s hx IH, by simp [IH])


#### Kevin Buzzard (Jan 25 2020 at 01:12):

Thanks Mario. Can you prove @Chris Hughes ' vars defined via the bind is the same as @Johannes Hölzl's '?

#### Mario Carneiro (Jan 25 2020 at 01:30):

theorem finset.bind_eq_sup {α β} [decidable_eq β] (s : finset α)
(f : α → finset β) : finset.bind s f = finset.sup s f :=
by classical; exact finset.induction_on s rfl (λ x s hx IH, by simp [IH])

@[simp] theorem multiset.union_to_finset {α} [decidable_eq α] (s t : multiset α) :
(s ∪ t).to_finset = s.to_finset ∪ t.to_finset :=
by ext a; simp

theorem multiset.sup_to_finset (α : Type*) (s : finset α) (β : Type*) [decidable_eq β]
(f : α → multiset β) : (finset.sup s f).to_finset = finset.bind s (λ x, (f x).to_finset) :=
by classical; exact finset.induction_on s rfl (λ x s hx IH, by simp [IH])

example {R : Type*} [comm_semiring R] {σ : Type*} {p : mv_polynomial σ R}
[decidable_eq σ] : mv_polynomial.vars p = p.support.bind finsupp.support :=
begin
unfold mv_polynomial.vars mv_polynomial.degrees,
rw multiset.sup_to_finset, congr, funext x,
apply finsupp.to_finset_to_multiset,
end


#### Kevin Buzzard (Jan 30 2020 at 14:10):

A belated thanks for this Mario!

Last updated: May 09 2021 at 10:11 UTC