finset.to_list sum

Stream: Is there code for X?

[Joseph Hua]

Hi, is there code for

import data.finset

lemma help {A B : Type*}
  [decidable_eq A] [add_comm_monoid B] (s : finset A)
  (f : A → B)
  :
  finset.sum s f = (list.map f s.to_list).sum
  :=
begin
  apply finset.induction_on s,
  {simp},
  {
    intros a s has hind,
    rw [finset.sum_insert has, hind],
    sorry -- f a + (list.map f s.to_list).sum = (list.map f (insert a s).to_list).sum
  },
end

[Kevin Buzzard]

My instinct is to show that (insert a s).to_list bijects with a :: s.to_list in the sense of list.perm and then to show that list.map reflects equiv.perm and list.sum sends equivalent lists to equal sums.

[Kevin Buzzard]

Do we have any of that?

[Yaël Dillies]

Of course. That's basically how finset.sum is defined in the first place.

[Kevin Buzzard]

Right! I just don't know my way around

[Kevin Buzzard]

OK we've reduced it to a :: s.to_list ~ (insert a s).to_list

[Yaël Dillies]

Okay, that sounds actually hard to prove

[Johan Commelin]

Hmmz, it seems that finset.sum uses a list.foldr under the hood. Whereas list.sum is using a foldl. That's surprising.

[Johan Commelin]

delta finset.sum multiset.sum list.sum multiset.foldr
    multiset.map finset.to_list
-- quot.lift_on (quot.lift_on s.val
--  (λ (l : list A), ↑(list.map f l)) _) (λ (l : list B), list.foldr has_add.add 0 l) _ =
-- list.foldl has_add.add 0 (list.map f s.val.to_list)

[Kevin Buzzard]

import data.finset

lemma help {A B : Type*}
  [decidable_eq A] [add_comm_monoid B] (s : finset A)
  (f : A → B)
  :
  finset.sum s f = (list.map f s.to_list).sum
  :=
begin
  apply finset.induction_on s,
  {simp},
  {
    intros a s has hind,
    rw [finset.sum_insert has, hind],
    rw ← list.sum_cons,
    apply list.perm.sum_eq,
    rw ← list.map_cons,
    apply list.perm.map,
    -- a :: s.to_list ~ (insert a s).to_list
    sorry,
  },
end

[Yaël Dillies]

Oh actually this is fine because we're talking about finsets, not multisets.

[Kevin Buzzard]

(deleted)

[Yaël Dillies]

Extensionality is enough.

[Kevin Buzzard]

Aah!

[Yaël Dillies]

But I don't know how to prove the corresponding statement with docs#multiset.to_list

[Kevin Buzzard]

lol list.perm.mem_iff isn't an iff

[Kevin Buzzard]

oh because it's not true because of repeats :-/

[Ruben Van de Velde]

lemma help {A B : Type*}
  [decidable_eq A] [add_comm_monoid B] (s : finset A)
  (f : A → B)
  :
  finset.sum s f = (list.map f s.to_list).sum
  :=
begin
  apply finset.induction_on s,
  {simp},
  { intros a s has hind,
    rw [finset.sum_insert has, hind],
    rw ← list.sum_cons,
    apply list.perm.sum_eq,
    rw ← list.map_cons,
    apply list.perm.map,
    rw list.perm_ext,
    { intros x,
      simp only [list.mem_cons_iff, iff_self, finset.mem_to_list, finset.mem_insert] },
    { simp [has, finset.nodup_to_list s] },
    { apply finset.nodup_to_list } },
end

[Johan Commelin]

docs#multiset.sum_to_list exists

[Joseph Hua]

should this be called finset.sum_to_list? or maybe finset.to_list_sum? whats the convension on the ordering

[Anne Baanen]

I'd copy the multiset version and call it finset.sum_to_list. In general we put the "outermost" operator first, in this case sum.

[Yaël Dillies]

Given the multiset precedent, finset.sum_to_list. Please make finset.insert_to_list as separate lemma

[Anne Baanen]

Even better would be to call it finset.prod_to_list (and prove it for Π of course!): we have a magical translation from products to sums called @[to_additive].

[Kevin Buzzard]

Can someone give Joseph push access to non-master branches of mathlib? His github userid is Jlh18

[Johan Commelin]

lemma help {A B : Type*} [decidable_eq A] [add_comm_monoid B]
  (s : finset A) (f : A → B) :
  finset.sum s f = (list.map f s.to_list).sum :=
begin
  delta finset.sum,
  rw [← multiset.coe_sum, ← multiset.coe_map, finset.coe_to_list],
end

[Ruben Van de Velde]

Do we want

lemma finset.sum_def {A B : Type*} [add_comm_monoid B] (s : finset A) (f : A → B) :
  finset.sum s f = (s.1.map f).sum :=
rfl

?

[Johan Commelin]

@Joseph Hua https://github.com/leanprover-community/mathlib/invitations

[Joseph Hua]

thank you!

[Johan Commelin]

Golfed:

by { rw [← multiset.coe_sum, ← multiset.coe_map, finset.coe_to_list], refl, }

[Anne Baanen]

Ruben Van de Velde said:

Do we want

lemma finset.sum_def {A B : Type*} [add_comm_monoid B] (s : finset A) (f : A → B) :
  finset.sum s f = (s.1.map f).sum :=
rfl

?

I'd see this as a simp lemma in the opposite direction named something like sum_to_multiset. (More precisely, as@[to_additive] prod_to_multiset.)

[Eric Wieser]

We don't need finset.sum_def, because we already have it as an equation lemma for finset.sum; rw finset.sum does the same thing as that lemma.

[Eric Wieser]

Johan Commelin said:

Hmmz, it seems that finset.sum uses a list.foldr under the hood. Whereas list.sum is using a foldl. That's surprising.

There's an open issue about changing list.sum to go in the other direction, which definitionally is more convenient but computationally is slower.

[Eric Wieser]

The Zulip thread is here, I can't find the github issue any more

[Ruben Van de Velde]

#10842 is ready to land if someone wants to tell bors