Zulip Chat Archive

Stream: Is there code for X?

Topic: to_list_map_prod

Damiano Testa (Jul 14 2022 at 04:34):

Dear All,

is the lemma below in mathlib? I am finding it hard getting Lean to accept that since A is commutative, the order in which you multiply the elements of s does not matter.

Thanks!

lemma multiset.to_list_map_prod {ι A : Type*} [comm_monoid A] (s : multiset ι) (f : ι → A) :
  (s.to_list.map f).prod = (s.map f).prod :=
begin
  sorry
end

Junyan Xu (Jul 14 2022 at 04:47):

There're just a few lemmas about multiset.to_list and this isn't one of them as far as I can see. Some maintainers are against usage of multiset.to_list because it involves an arbitrary choice. But anyway here's a proof:

import algebra.big_operators.multiset
lemma to_list_map_prod {ι A : Type*} [comm_monoid A] (s : multiset ι) (f : ι → A) :
  (s.to_list.map f).prod = (s.map f).prod :=
by rw [← multiset.coe_prod, ← multiset.coe_map, s.coe_to_list]

Damiano Testa (Jul 14 2022 at 04:47):

Great, thank you very much!

Damiano Testa (Jul 14 2022 at 04:48):

Oh, and sorry for not putting in imports: I had forgotten about them!

Eric Wieser (Jul 14 2022 at 07:09):

@Damiano Testa, if you're proving stuff about to_list you might have taken a wrong turn

Eric Wieser (Jul 14 2022 at 07:09):

induction s using quotient.induction is a better direction to turn a statement about multisets into a statement about lists

Damiano Testa (Jul 14 2022 at 07:20):

Ok, but I would like to go the other way: multiplying over a list does not require commutativity, while over multisets does. So, I wanted to prove the list statement first and then deduce the multiset version from it.

Damiano Testa (Jul 14 2022 at 07:21):

I can also simply duplicate the proof of the list statement to prove the multiset one, but since choice is already part of the assumptions, Junyax Xu's proof did the job.

(We can take this conversation to #15296, if you prefer! :smile:

Damiano Testa (Jul 14 2022 at 07:22):

(Let me try what you suggest, though, since I am probably misunderstanding something.)

Yaël Dillies (Jul 14 2022 at 07:22):

Damiano Testa said:

Ok, but I would like to go the other way: multiplying over a list does not require commutativity, while over multisets does. So, I wanted to prove the list statement first and then deduce the multiset version from it.

This is exactly what induction on multiset does. When Eric says "turn a statement about multisets into a statement about lists", he means "turn the multisets in your goal into lists".

Damiano Testa (Jul 14 2022 at 07:25):

Ok, I am trying it, though:

unknown declaration 'quotient.induction'

Should I import something?

Yaël Dillies (Jul 14 2022 at 07:27):

Use docs#quot.induction_on and take inspiration from file#data/multiset/basic.

Damiano Testa (Jul 14 2022 at 07:27):

Got it: induction F using quot.induction_on!

Damiano Testa (Jul 14 2022 at 07:29):

Thank you all: the proof is now:

  induction F using quot.induction_on,
  rw [multiset.quot_mk_to_coe'', multiset.coe_map, multiset.coe_sum, multiset.coe_prod],
  exact sup_support_list_prod_le D0 Dm F,

Yaël Dillies (Jul 14 2022 at 07:30):

Try removing the rw!

Damiano Testa (Jul 14 2022 at 07:30):

Without the rw, I need convert and simp.

Damiano Testa (Jul 14 2022 at 07:30):

This is now going down Junyan Xu's ladder, instead of up!

Yaël Dillies (Jul 14 2022 at 07:31):

That's unexpected. Because everything to do with multiset is defined by induction from list, this ought to work. But I guess I don't know the full statement.

Damiano Testa (Jul 14 2022 at 07:34):

The point is that there is some (very small) content: I am mapping a multiset over a function and then summing.

Essentially if F is a multiset and a is another element, I am doing ((a::F).map f).to_list.sum vs ((a..F.to:list).map f).sum. So there is some property that you actually have to check. I think...

Yaël Dillies (Jul 14 2022 at 07:35):

Are you still using multiset.to_list?

Damiano Testa (Jul 14 2022 at 07:36):

No, not anymore, this was before. Now the full proof is what I wrote above. The statement is purely about multisets, no lists.

Yaël Dillies (Jul 14 2022 at 07:36):

What is the statement?

Damiano Testa (Jul 14 2022 at 07:36):

You can check it out in #15296 (still has the old statement).

Damiano Testa (Jul 14 2022 at 07:37):

lemma sup_support_multiset_prod_le
  {D : A → B} (D0 : D 0 ≤ 0) (Dm : ∀ a b, D (a + b) ≤ D a + D b)
  (F : multiset (add_monoid_algebra R A)) :
  F.prod.support.sup D ≤ (F.map (λ f : add_monoid_algebra R A, f.support.sup D)).sum :=
begin
  induction F using quot.induction_on,
  rw [multiset.quot_mk_to_coe'', multiset.coe_map, multiset.coe_sum, multiset.coe_prod],
  exact sup_support_list_prod_le D0 Dm F,
end