Zulip Chat Archive

Stream: new members

Topic: finsum/finprod


Alex Zhang (Jul 18 2021 at 16:52):

I am not very sophisticated at splitting sums or pick a single term out of a sum. Can anyone please give me convenient a way to proving the following eg?

import algebra.big_operators
import data.fintype.card
import data.finset.basic

open_locale big_operators

variables {I : Type*} [fintype I] [decidable_eq I]

def fn : I  I   := λ i j, ite (i = j) 0 1
lemma eg (j : I) :  (i : I), (fn i j) = fintype.card I - 1 :=
begin
  sorry
end

Eric Wieser (Jul 18 2021 at 16:53):

FYI, docs#finsum is different to docs#finset.sum

Anne Baanen (Jul 18 2021 at 17:00):

I think the best way to pick out a single term, for the moment is to rw ← with docs#finset.insert_erase and then rw with docs#finset.prod_insert. (We should really add a convenient shortcut.)

Anne Baanen (Jul 18 2021 at 17:04):

For your specific example, I would first rewrite with docs#finset.sum_ite and docs#finset.sum_const_zero, then show s.filter ((≠) i) = s.erase i with docs#finset.filter_ne. Finish with docs#finset.card_eq_sum_ones and docs#finset.card_erase_of_mem.

Anne Baanen (Jul 18 2021 at 17:07):

(Note that I didn't know about half of these lemmas, but guessed they existed based on their name!)

Kyle Miller (Jul 18 2021 at 18:13):

@Alex Zhang It seems like you potentially have the goal of proving

lemma eg' :  (i : I),  (j : I), fn i j = fintype.card I * (fintype.card I - 1)

In any case, I wanted to try proving this with docs#finset.induction_on (which is definitely not the best way), so here's a proof of it. I found many of the lemmas by guessing names, library_search for specific statements I wrote with have, squeeze_simp, and by consulting the documentation.

Alex Zhang (Jul 18 2021 at 18:54):

Cool proof!

Kyle Miller (Jul 18 2021 at 18:54):

This is definitely not the best proof :smile: Compare to this:

Kyle Miller (Jul 18 2021 at 18:56):

(The simp only line started out as simp [fn, finset.sum_ite, finset.filter_ne, finset.card_erase_of_mem, finset.card_univ] before squeeze_simp.)

Alex Zhang (Jul 18 2021 at 18:58):

Very nice! Do you have any convenient proof for the original eg without proving the more general one? @Kyle Miller

Alex Zhang (Jul 18 2021 at 19:00):

I have not happened to need the general one for my work, but definitely a wonderful backup!

Kyle Miller (Jul 18 2021 at 19:01):

@Alex Zhang Maybe try the simp [...] line I just mentioned and see how far it proves it.

Alex Zhang (Jul 18 2021 at 19:05):

It goes to the point where I first stuck (finset.filter (λ (x : I), ¬x = j) finset.univ).card = fintype.card I - 1.
I have known ways to get rid of such things, but they all seem kind of winding.

Kyle Miller (Jul 18 2021 at 19:06):

Make sure to take a look at what finset.filter_ne is doing and how it doesn't apply here.

Kyle Miller (Jul 18 2021 at 19:07):

This is what docs#finset.filter_ne' is for -- just add the ' to the end of the name of that lemma. refl will then prove the simplified result.

Yakov Pechersky (Jul 18 2021 at 19:16):

lemma eg (j : I) :  (i : I), (fn i j) = fintype.card I - 1 :=
begin
  have : 0 < fintype.card I := finset.card_pos.mpr j, by simp⟩,
  rw [fn, eq_comm, finset.sum_ite, nat.sub_eq_iff_eq_add this],
  simp [finset.filter_ne', finset.card_erase_of_mem, finset.card_univ, nat.succ_eq_add_one,
        nat.succ_pred_eq_of_pos this]
end

Kyle Miller (Jul 18 2021 at 19:18):

lemma eg (j : I) :  (i : I), fn i j = fintype.card I - 1 :=
by simpa [fn, finset.sum_ite, finset.filter_ne', finset.card_erase_of_mem, finset.card_univ]

Alex Zhang (Jul 18 2021 at 19:21):

short and nice!

Alex Zhang (Jul 18 2021 at 19:30):

@Kyle Miller Kyle, can you please explain why

lemma eg (j : I) :  (i : I), (fn i j) = fintype.card I - 1 :=
by {simp [fn, finset.sum_ite], simp [finset.filter_ne'],
  simpa [finset.card_erase_of_mem],}

the goal but not when changing the final simpa to simp?

Kyle Miller (Jul 18 2021 at 19:31):

simpa is meant to be the last step of a proof, and it does simp followed by trying to refl or to find a relevant assumption that closes the goal.

Kyle Miller (Jul 18 2021 at 19:31):

it's like rwa vs rw.

Alex Zhang (Jul 18 2021 at 19:32):

Oh! I forgot simpa uses refl.

Kyle Miller (Jul 18 2021 at 19:33):

I think it tries using assumption and then trivial. trivial knows how to refl.

Yakov Pechersky (Jul 18 2021 at 19:35):

Crucially, simpa can take a using h to try to close the goal with the hypothesis h. And it runs simp on both the goal and the hypothesis h, but no further than necessary.


Last updated: Dec 20 2023 at 11:08 UTC