explicit sums

Stream: Is there code for X?

[Michael Stoll]

Is there a better way of proving the following?

import tactic
import data.zmod.basic

open_locale big_operators
open finset

example {R : Type*} [add_comm_monoid R] (f : (zmod 3) → R) : ∑ a, f a = f 0 + f 1 + f 2 :=
begin
  have hs : cons 0 ({1, 2} : finset (zmod 3)) dec_trivial = univ := dec_trivial,
  have hs' : cons 1 ({2} : finset (zmod 3)) dec_trivial = ({1, 2} : finset (zmod 3)) := dec_trivial,
  rw [← hs, sum_cons, ← hs', sum_cons, ← add_assoc, sum_singleton],
end

(bearing in mind that what I really want is the analogous statement for zmod 8...)

[Eric Rodriguez]

norm_num should do this, I think

[Eric Rodriguez]

hmm... seems not. I thought @Anne Baanen had made a tactic for this recently.

[Michael Stoll]

norm_num does basically nothing here. Perhaps because norm_num does not work well with zmod?

[Heather Macbeth]

For fin rather than zmod, you can do

example {R : Type*} [add_comm_monoid R] (f : fin 3 → R) : ∑ a, f a = f 0 + (f 1 + f 2) :=
by simp [fin.sum_univ_succ]

[Eric Rodriguez]

I figured it out: you need the import import algebra.big_operators.norm_num

[Eric Rodriguez]

but this still doesn't work for zmod, you need to change some stuff:

import tactic
import data.zmod.basic
import algebra.big_operators.norm_num

open_locale big_operators
open finset

example {R : Type*} [add_comm_monoid R] (f : (zmod 3) → R) : ∑ a, f a = f 0 + f 1 + f 2 :=
begin
  rw zmod at f,
  change ∑ (a : fin 3), _ = _,
  norm_num,
end

I guess this is fixable

[Eric Rodriguez]

(also for some reason norm_num doesn't fix the + 0 here)

[Eric Rodriguez]

(and if you don't try change, norm_num errors hard)

[Michael Stoll]

Hmm. After rw zmod at f, the tactic state has two fs:

f: zmod 3 → R
f: fin (2 + 1) → R

What to make of that?

[Eric Rodriguez]

it's what should be expected, but just don't do this it's a bad idea

[Eric Rodriguez]

like very bad idea

[Michael Stoll]

Why do you do it then in your code above?

[Eric Rodriguez]

the issue is that f is already in the expression so it can't just get rid of the f, so it has to make a copy

[Eric Rodriguez]

just to debug pretty much

[Michael Stoll]

Also, with

import tactic
import data.zmod.basic
import algebra.big_operators.norm_num

open_locale big_operators
open finset

example {R : Type*} [add_comm_monoid R] (f : (zmod 3) → R) : ∑ a, f a = f 0 + f 1 + f 2 :=
begin
  rw zmod at f,
  change ∑ (a : fin 3), _ = _,
  norm_num,
  rw [add_zero, ← add_assoc],
end

I get the "Goals accomplished" message, but also an error

type mismatch at application
  @tactic.norm_num.finset.eval_sum_of_list R
term
  R
has type
  Type u_1
but is expected to have type
  Type u_2

which I find rather confusing.

[Eric Rodriguez]

bug in the norm_num impl below:

import tactic
import data.zmod.basic
import algebra.big_operators.norm_num

open_locale big_operators
open finset

example {R : Type} [add_comm_monoid R] (f : (zmod 3) → R) : ∑ a, f a = f 0 + f 1 + f 2 :=
begin
  change ∑ (a : fin 3), _ = _,
  norm_num,
  rw [add_zero, add_assoc],
end

[Eric Rodriguez]

yeah, that's a sign of a buggy tactic. i'm not really sure what's up nor how to debug things

[Michael Stoll]

Heather Macbeth said:

For fin rather than zmod, you can do

example {R : Type*} [add_comm_monoid R] (f : fin 3 → R) : ∑ a, f a = f 0 + (f 1 + f 2) :=
by simp [fin.sum_univ_succ]

This doesn't seem to work when I replace 3 by 4:

example {R : Type*} [add_comm_monoid R] (f : (fin 4) → R) : ∑ a, f a = f 0 + f 1 + f 2 + f 3 :=
begin
  rw [add_assoc, add_assoc],
  simp [fin.sum_univ_succ],
end

leaves the goal at f 0 + (f 1 + (f 2 + f 2.succ)) = f 0 + (f 1 + (f 2 + f 3)). Adding a congr at the end finishes it, though.

[Michael Stoll]

Confusingly,

example {R : Type*} [add_comm_monoid R] (f : (zmod 8) → R) :
 ∑ a, f a = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7 :=
begin
  change ∑ (a : fin 8), _ = _,
  repeat {rw add_assoc},
  simp [fin.sum_univ_succ], -- does not replace the sum
  sorry
end

does not work, but using fin 8 in the statement instead of zmod 8 does.

[Michael Stoll]

The following works.

example {R : Type*} [add_comm_monoid R] (f : (zmod 8) → R) :
 ∑ a, f a = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7 :=
begin
  have sum8 : ∀ (f : (fin 8) → R), ∑ a, f a = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7 :=
  begin
    intro f',
    repeat {rw add_assoc},
    simp [fin.sum_univ_succ],
    congr,
  end,
  exact sum8 f,
end

[Michael Stoll]

But why it works in this form and not in the previous one, I do not understand.

[Mario Carneiro]

cc @Anne Baanen re: norm_num extension bug

[Michael Stoll]

But my proof (derived from @Heather Macbeth 's one) does not use norm_num.

[Mario Carneiro]

the norm_num bug may or may not be related to your issue, but it's a bug in any case

[Kevin Buzzard]

Why are you using zmod 3 and not fin 3, the "official" type with 3 elements?

[Alex J. Best]

I'm guessing f is some sort of character, so zmod makes more sense for those

[Michael Stoll]

Yes; in my use case, I want to expand a Gauss sum on Z/8Z into an explicit sum, so zmod n is the natural type.

[Anne Baanen]

Thanks for being guinea pigs for the tactic! :)

[Anne Baanen]

Michael Stoll said:

Hmm. After rw zmod at f, the tactic state has two fs:

f: zmod 3 → R
f: fin (2 + 1) → R

What to make of that?

I recall something ending up with fin (2+1) before, not entirely sure where, and it confused norm_num, but I fixed it by making sure the tactics I called would always give fin 3. The other solution would be to replace some usages of docs#expr.to_nat with something slightly smarter that understands +1.

[Anne Baanen]

Michael Stoll said:

Also, with

import tactic
import data.zmod.basic
import algebra.big_operators.norm_num

open_locale big_operators
open finset

example {R : Type*} [add_comm_monoid R] (f : (zmod 3) → R) : ∑ a, f a = f 0 + f 1 + f 2 :=
begin
  rw zmod at f,
  change ∑ (a : fin 3), _ = _,
  norm_num,
  rw [add_zero, ← add_assoc],
end

I get the "Goals accomplished" message, but also an error

type mismatch at application
  @tactic.norm_num.finset.eval_sum_of_list R
term
  R
has type
  Type u_1
but is expected to have type
  Type u_2

which I find rather confusing.

Oof, that's an embarassing kind of bug :P

[Anne Baanen]

I should have some time within the next days to fix both these issues.

[Eric Rodriguez]

was this ever fixed, btw?

[Anne Baanen]

I don't think so, at leat I never got around to it