Zulip Chat Archive

Stream: general

Topic: splitting an explicit `finset.sum`


Jireh Loreaux (Oct 07 2022 at 15:23):

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 (Oct 07 2022 at 15:45):

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 (Oct 07 2022 at 16:18):

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 (Oct 07 2022 at 16:18):

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

Alex J. Best (Oct 07 2022 at 16:33):

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

Kyle Miller (Oct 07 2022 at 16:34):

It seems to already work:

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

Junyan Xu (Oct 07 2022 at 17:28):

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 (Oct 07 2022 at 18:08):

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 (Oct 07 2022 at 18:25):

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

Kyle Miller (Oct 07 2022 at 18:48):

@Alex J. Best I had

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

Kyle Miller (Oct 07 2022 at 19:25):

@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 (Oct 07 2022 at 21:59):

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 (Oct 08 2022 at 01:14):

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

Junyan Xu (Oct 08 2022 at 03:29):

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 (Oct 08 2022 at 06:10):

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 (Oct 08 2022 at 14:03):

#15738


Last updated: Dec 20 2023 at 11:08 UTC