Zulip Chat Archive

Stream: maths

Topic: finset puzzle


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

view this post on Zulip Johan Commelin (Jan 24 2020 at 18:42):

Yes, use ext

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

view this post on Zulip Kevin Buzzard (Jan 24 2020 at 18:46):

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

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

view this post on Zulip Kevin Buzzard (Jan 24 2020 at 18:49):

the sup is defined as a fold over union.

view this post on Zulip Johan Commelin (Jan 24 2020 at 18:49):

Is there a mem_fold?

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

view this post on Zulip Johan Commelin (Jan 24 2020 at 18:50):

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

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

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

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

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

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

view this post on Zulip Floris van Doorn (Jan 24 2020 at 20:08):

You indeed also need sup_le.

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

view this post on Zulip Kevin Buzzard (Jan 24 2020 at 21:37):

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

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

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

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

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

view this post on Zulip Kevin Buzzard (Jan 30 2020 at 14:10):

A belated thanks for this Mario!


Last updated: May 09 2021 at 10:11 UTC