Making `finset.sum` into an explicit sum

Stream: Is there code for X?

[Vasily Ilin]

How do I go between finset.sum to an explicit sum? I'd imagine it's just simp, using docs#finset.sum_cons three times. But simp doesn't do it.

import tactic
import linear_algebra.basis
import data.matrix.notation

variables (k : Type) (V : Type) [field k] [add_comm_group V] [module k V]

example (f : fin 4 → k) (v0 v1 v2 v3 : V) : finset.univ.sum (λ (i : fin 4), f i • ![v0, v1, v2, v3] i) = f 0 • v0 + f 1 • v1 + f 2 • v2 + f 3 • v3 := sorry

[Vasily Ilin]

Also, what tactic would do this?

import tactic
import data.complex.basic

variables (k : Type) (V : Type) [field k] [add_comm_group V] [module k V]

example (g : fin 4 → k) (v0 v1 v2 v3 : V) :
g 0 • v0 + (g 1 - g 0) • v1 + (g 2 - g 1) • v2 + (g 3 - g 2) • v3 =
g 0 • (v0 - v1) + g 1 • (v1 - v2) + g 2 • (v2 - v3) + g 3 • v3 := sorry

[Kevin Buzzard]

import tactic
import data.complex.basic

variables (k : Type) (V : Type) [field k] [add_comm_group V] [module k V]

example (g : fin 4 → k) (v0 v1 v2 v3 : V) :
g 0 • v0 + (g 1 - g 0) • v1 + (g 2 - g 1) • v2 + (g 3 - g 2) • v3 =
g 0 • (v0 - v1) + g 1 • (v1 - v2) + g 2 • (v2 - v3) + g 3 • v3 :=
begin
  simp only [smul_sub, sub_smul],
  abel,
end

The hint tactic suggests that you can't do this with one tactic.

[Kevin Buzzard]

import tactic
import linear_algebra.basis
import data.matrix.notation

variables (k : Type) (V : Type) [field k] [add_comm_group V] [module k V]

example (f : fin 4 → k) (v0 v1 v2 v3 : V) : finset.univ.sum (λ (i : fin 4), f i • ![v0, v1, v2, v3] i) = f 0 • v0 + f 1 • v1 + f 2 • v2 + f 3 • v3 :=
begin
  simp [finset.sum_fin_eq_sum_range, finset.sum_range_succ],
end

works. I knew about finset.sum_range_succ so could see that if I could translate into this I'd probably be done, and so I tried rw finset.sum_range and auto-complete found finset.sum_fin_eq_sum_range for me.

[Eric Wieser]

docs#fin.sum_univ_succ

[Eric Wieser]

We seem to get a question asking for that lemma every week or so!

[Vasily Ilin]

With the help above I was able to finish the proof. But it looks quite ugly and takes a few seconds to compile. I'm sure such as simple proposition can be proven easier. Can anyone give me advice on how to make this proof better?

import tactic -- imports all the Lean tactics
import linear_algebra.basis
import data.real.basic
import data.complex.basic
import data.complex.module
import data.matrix.notation

variables (k : Type) (V : Type) [field k] [add_comm_group V] [module k V]

example (v1 v2 v3 v4: V) (lin_indep : linear_independent k ![v1, v2, v3, v4]) : linear_independent k ![v1-v2, v2-v3, v3-v4, v4] :=
begin
  rw fintype.linear_independent_iff at *,
  intros g h,
  let f := ![g 0, g 1 - g 0, g 2 - g 1, g 3 - g 2],
  specialize lin_indep f,
  suffices  hf : ∀ (i : fin 4), f i = 0,
  have g0 : g 0 = 0,
    calc g 0 = f 0 : rfl
        ...  = 0 : hf 0,
  have g1 : g 1 = 0,
    calc g 1 = g 1 - g 0 + g 0 : by ring
      ... = f 1 + g 0 : by refl
      ... = 0 : by rw [hf 1, g0, zero_add],
  have g2 : g 2 = 0,
    calc g 2 = g 2 - g 1 + g 1 : by ring
      ... = f 2 + g 1 : by refl
      ... = 0 : by rw [hf 2, g1, zero_add],
  have g3 : g 3 = 0,
    calc g 3 = g 3 - g 2 + g 2 : by ring
      ... = f 3 + g 2 : by refl
      ... = 0 : by rw [hf 3, g2, zero_add],

  intro i,
  fin_cases i,
  exact g0,
  exact g1,
  exact g2,
  exact g3,

  apply lin_indep,
  calc finset.univ.sum (λ (i : fin 4), f i • ![v1, v2, v3, v4] i)
            = f 0 • v1 + f 1 • v2 + f 2 • v3 + f 3 • v4 : by
            begin
              simp only [fin.sum_univ_succ, add_assoc, matrix.cons_val_zero, matrix.cons_val_succ, fin.succ_zero_eq_one, fin.succ_one_eq_two, fintype.univ_of_subsingleton, fin.mk_eq_subtype_mk, fin.mk_zero, finset.sum_singleton, add_right_inj],
              refl,
            end
     ...    = g 0 • v1 + (g 1 - g 0) • v2 + (g 2 - g 1) • v3 + (g 3 - g 2) • v4 : rfl
     ...    = g 0 • (v1 - v2) + g 1 • (v2 - v3) + g 2 • (v3 - v4) + g 3 • v4 : by
            begin
              simp only [smul_sub, sub_smul],
              abel,
            end
     ...    = finset.univ.sum (λ (i : fin 4), g i • ![v1 - v2, v2 - v3, v3 - v4, v4] i) : by
            begin
              simp only [fin.sum_univ_succ, add_assoc, matrix.cons_val_zero, matrix.cons_val_succ, fin.succ_zero_eq_one, fin.succ_one_eq_two, fintype.univ_of_subsingleton, fin.mk_eq_subtype_mk, fin.mk_zero, finset.sum_singleton, add_right_inj],
              refl,
            end
     ...    = 0 : h,
end

[Wrenna Robson]

import linear_algebra.basis
import data.matrix.notation

open matrix
variables (R : Type) (V : Type) [ring R] [add_comm_group V] [module R V]

lemma better_form (v1 v2 v3 v4 : V) :
![v1 - v2, v2 - v3, v3 - v4, v4] = ![v1, v2, v3, v4] - fin.snoc (fin.tail (![v1, v2, v3, v4])) 0 :=
by simp [vec_head, vec_tail, fin.snoc, fin.tail]; refl

lemma snoc_tail_lin_indep (v : fin 4 → V) (lin_indep : linear_independent R v) :
linear_independent R (v - fin.snoc (fin.tail v) 0) :=
begin
  simp_rw fintype.linear_independent_iff at ⊢ lin_indep, intros g hg i,
  suffices hli :  finset.univ.sum (λ (i : fin 4),
                  (g - fin.cons 0 (fin.init g)) i • v i) = 0,
  { specialize lin_indep _ hli,
    have g0 : g 0 -   0 = 0 := lin_indep 0,               rw sub_zero at g0,
    have g1 : g 1 - g 0 = 0 := lin_indep 1, rw g0 at g1,  rw sub_zero at g1,
    have g2 : g 2 - g 1 = 0 := lin_indep 2, rw g1 at g2,  rw sub_zero at g2,
    have g3 : g 3 - g 2 = 0 := lin_indep 3, rw g2 at g3,  rw sub_zero at g3,
    fin_cases i; [exact g0, exact g1, exact g2, exact g3] },

  simp [fin.sum_univ_succ, smul_sub, sub_smul] at ⊢ hg,
  change  g 0 • v 0 + (g 1 • v 1 - g 0 • v 1 +
          (g 2 • v 2 - g 1 • v 2 + (g 3 • v 3 - g 2 • v 3))) = 0,
  change  g 0 • v 0 - g 0 • v 1 + (g 1 • v 1 -
          g 1 • v 2 + (g 2 • v 2 - g 2 • v 3 + (g 3 • v 3 - g 3 • 0))) = 0 at hg,
  rw [smul_zero, sub_zero] at hg, simp_rw [sub_eq_add_neg] at ⊢ hg,
  nth_rewrite 2 add_comm, nth_rewrite 4 add_comm, nth_rewrite 5 add_comm, simp_rw add_assoc at ⊢ hg,
  exact hg
end

example (v1 v2 v3 v4 : V) (lin_indep : linear_independent R ![v1, v2, v3, v4]) :
linear_independent R ![v1-v2, v2-v3, v3 - v4, v4] :=
by rw better_form ; exact snoc_tail_lin_indep _ _ _ lin_indep

[Wrenna Robson]

This is a bit better :)

[Wrenna Robson]

The problem is ultimately in how you state the lemma - how you express ![v1-v2, v2-v3, v3 - v4, v4] , basically.

[Wrenna Robson]

On some level this is a computational algebra task, which Lean has no natural facility in. That's the comm and assoc stuff at the end. Everything else is really just... making sure you're using sensible defintions.

[Wrenna Robson]

If you could express ![v1, v2, v3, v4] as the image under a suitable linear map of ![v1-v2, v2-v3, v3 - v4, v4] - bearing in mind that to use, say, linear_independent.map' you would have to define a map onV itself - this would be easier. But different expressions of ![v1-v2, v2-v3, v3 - v4, v4]produce different difficulties.

[Wrenna Robson]

In general, given an arbitrary linear combination of ![v1, v2, v3, v4] and proving linear independence from the linear independence of the v_i is going to be very close to showing that some matrix is non-singular...

[Wrenna Robson]

I note, by the way, that we don't seem to have something like vec_update or vec_rotate which makes this trickier to construct, as you can see.

[Eric Wieser]

vec_update is docs#function.update

[Eric Wieser]

vec_rotate is composition with docs#fin_rotate

[Wrenna Robson]

Aye. But we seem to have vec_cons despite having fin.cons also, unless I'm wrong?

[Eric Wieser]

I think the motivation is that the latter elaborates badly on non-dependent types. That may well be a concern for update too.

[Wrenna Robson]

Huh, makes sense.

[Anne Baanen]

Eric Wieser said:

I think the motivation is that the latter elaborates badly on non-dependent types. That may well be a concern for update too.

The issue was specifically that the ![1, 2, 3] notation elaborated badly and didn't get pretty-printed correctly (even with type ascriptions etc.)