finset puzzle

Stream: maths

[Kevin Buzzard]

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]

Yes, use ext

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

is what I'm left with

[Kevin Buzzard]

the sup is defined as a fold over union.

[Johan Commelin]

Is there a mem_fold?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

You indeed also need sup_le.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

@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]

@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]

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

[Mario Carneiro]

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]

A belated thanks for this Mario!