splitting an explicit `finset.sum`

Stream: general

[Jireh Loreaux]

How does one get Lean to prove this automatically? I was expecting some sort of incantation involving fin_cases and dec_trivial would work, but I couldn't manage it.

lemma foo : finset.univ.sum (![4, 5] : fin 2 → ℝ) = 4 + 5 := sorry

[Junyan Xu]

import algebra.big_operators.fin
import data.real.basic

-- the defeq works this way
example : finset.univ.sum (![4, 5] : fin 2 → ℝ) = 4 + 5 := by { change 4 + (5 + 0 : ℝ) = _, simp }

-- mathlib also has lemma for it
example : finset.univ.sum (![4, 5] : fin 2 → ℝ) = 4 + 5 := fin.sum_univ_two _

[Jireh Loreaux]

Aha, but we just ran into part of my #xy. What if I had, say, 20 terms? It would be nice to have some tactic that could handle this without an ugly change.

[Yaël Dillies]

Just simp_rw with docs#fin.sum_univ_succ and docs#fin.sum_univ_zero

[Alex J. Best]

After #16518 is merged (tomorrow?) norm_num will evaluate both sides of this

[Kyle Miller]

It seems to already work:

example : finset.univ.sum (![4, 5] : fin 2 → ℝ) = 4 + 5 := by norm_num

[Junyan Xu]

I also came up with a general way of proving such equalities as a comment in the PR where the fin.sum_univ_x lemmas were added:

example : finset.univ.sum (![4, 5] : fin 2 → ℝ) = 4 + 5 :=
(multiset.fold_eq_foldl _ _ _).trans $ by { conv_rhs { rw ← zero_add (4 : ℝ) }, refl }

but it's not good for rewriting the LHS to RHS.

[Alex J. Best]

Kyle Miller said:

It seems to already work:

example : finset.univ.sum (![4, 5] : fin 2 → ℝ) = 4 + 5 := by norm_num

with what imports? I tried on some random lean window I had open and it didn't, perhaps my mathlib is too old!

[Eric Rodriguez]

there is a norm_num extension for finset.sum but it's half-broken with weird unierse isuses

[Kyle Miller]

@Alex J. Best I had

import algebra.big_operators.fin
import data.real.basic

[Kyle Miller]

@Alex J. Best Turns out by simp works too with those imports, and norm_num is likely working just because it does simp

[Junyan Xu]

It turns out docs#fin.sum_univ_two is a simp lemma but docs#fin.sum_univ_three is not, so

example : finset.univ.sum (![4, 5, 6] : fin 3 → ℝ) = 4 + 5 + 6 := by simp

fails.

[Eric Wieser]

I have a PR about generating this kind of lemma at elaboration time, which handles the n=20 case

[Junyan Xu]

Eric Wieser said:

I have a PR about generating this kind of lemma at elaboration time, which handles the n=20 case

#16518 or another one? #16518 has been delegated.

[Patrick Johnson]

Term mode proof for any number of elements (faster than simp or norm_num):

import data.real.basic
import algebra.big_operators.fin

variables {α : Type*} [add_comm_monoid α]

def f : Π {n : ℕ} (v : fin n → α), α
| 0 _ := 0
| 1 v := v 0
| (n+2) v := f (λ (k : fin (n + 1)), v k) + v (n + 1)

lemma auto {n : ℕ} {v : fin n → α} : finset.univ.sum v = f v := sorry

example : finset.univ.sum (![4, 5] : fin 2 → ℝ) = 4 + 5 := auto

[Eric Wieser]

#15738