finsum/finprod

Stream: new members

[Alex Zhang]

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]

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

[Anne Baanen]

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]

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]

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

[Kyle Miller]

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

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 fn.symm (i j : I) : fn i j = fn j i :=
by simp [fn, eq_comm]

lemma eg'' (s : finset I) : ∑ i in s, ∑ j in s, fn i j = s.card * (s.card - 1) :=
begin
  refine s.induction_on _ (λ x s' hx h, _),
  { simp, },
  { change ∑ i in s', finset.sum s' (fn i) = _ at h,
    simp_rw [finset.sum_insert hx, finset.sum_add_distrib, h],
    rw [←finset.sum_attach],
    have key1 : fn x x = 0 := by simp [fn],
    have key2 : ∀ (x' : s'), fn x (x' : I) = 1,
    { rintro ⟨x', hx'⟩,
      simp only [fn, ite_eq_right_iff, nat.zero_ne_one, subtype.coe_mk],
      rintro rfl,
      exact hx hx', },
    simp only [key1, key2, nat.cast_id, finset.sum_const, zero_add, finset.card_attach, nat.smul_one_eq_coe],
    rw [←finset.sum_attach],
    simp only [fn.symm, key2, nat.cast_id, finset.sum_const, finset.card_attach, nat.smul_one_eq_coe],
    simp only [finset.card_insert_of_not_mem hx, nat.add_succ_sub_one, add_zero],
    rw [right_distrib, one_mul, add_comm _ (finset.card s')],
    rw [add_right_inj, add_comm, ←nat.mul_succ],
    by_cases hh : s'.card = 0,
    { simp only [hh, zero_mul], },
    { congr,
      rw nat.succ_eq_add_one,
      apply nat.sub_add_cancel,
      have : 0 < finset.card s', exact pos_iff_ne_zero.mpr hh,
      exact nat.succ_le_iff.mpr this, } },
end

lemma eg' : ∑ (i : I), ∑ (j : I), fn i j = fintype.card I * (fintype.card I - 1) :=
by rw [eg'', finset.card_univ]

[Alex Zhang]

Cool proof!

[Kyle Miller]

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

lemma eg''' : ∑ (i : I), ∑ (j : I), fn i j = fintype.card I * (fintype.card I - 1) :=
begin
  simp only [fn, finset.sum_ite, finset.filter_ne, finset.card_erase_of_mem, finset.card_univ,
    finset.mem_univ, nat.cast_id, mul_eq_mul_left_iff, finset.sum_const,
    nsmul_eq_mul, zero_add, finset.sum_const_zero, nat.smul_one_eq_coe],
  left,
  refl,
end

[Kyle Miller]

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

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

[Alex Zhang]

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

[Kyle Miller]

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

[Alex Zhang]

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]

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

[Kyle Miller]

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]

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]

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]

short and nice!

[Alex Zhang]

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

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]

it's like rwa vs rw.

[Alex Zhang]

Oh! I forgot simpa uses refl.

[Kyle Miller]

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

[Yakov Pechersky]

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.