Unfold sum over zmod

Stream: new members

[Adrián Doña Mateo]

Is there a way to unfold a sum over a finite type into an explicit sum? In particular, I would like to prove something like the following:

import data.zmod.basic
import data.real.basic

open_locale big_operators

example (f : zmod 3 → ℝ) : ∑ x, f x = f 0 + f 1 + f 2 := sorry

I have noticed that if instead of ℝ I write ℕ this is easy. But I can't do the same with ℝ because it is not computable.

example (f : zmod 3 → ℕ) : ∑ x, f x = f 0 + (f 1 + f 2) := rfl

[Mario Carneiro]

I don't think it should matter if the codomain is real here

[Mario Carneiro]

the rfl proof should still work

[Kevin Buzzard]

example (f : zmod 3 → ℝ) : ∑ x, f x = f 0 + (f 1 + (f 2 + 0)) := rfl

[Kevin Buzzard]

n+0=n is rfl for nat but not for real

[Mario Carneiro]

so an alternative proof for the original version would be

example (f : zmod 3 → ℝ) : ∑ x, f x = f 0 + f 1 + f 2 :=
show f 0 + (f 1 + (f 2 + 0)) = _, by simp [add_assoc]

[Yakov Pechersky]

Is there a zmod to fin equiv? This works:

import data.zmod.basic
import data.real.basic

open_locale big_operators

example (f : fin 3 → ℝ) : ∑ x, f x = f 0 + f 1 + f 2 :=
begin
  simpa [fin.sum_univ_succ, add_assoc]
end

[Mario Carneiro]

they are actually defeq I think

[Mario Carneiro]

example : ∀ (f : zmod 3 → ℝ), ∑ x, f x = f 0 + f 1 + f 2 :=
show ∀ (f : fin 3 → ℝ), ∑ x, f x = f 0 + f 1 + f 2,
by intro f; simpa [fin.sum_univ_succ, add_assoc]

[Adrián Doña Mateo]

Mario Carneiro said:

so an alternative proof for the original version would be

example (f : zmod 3 → ℝ) : ∑ x, f x = f 0 + f 1 + f 2 :=
show f 0 + (f 1 + (f 2 + 0)) = _, by simp [add_assoc]

I see, thanks!

[Johan Commelin]

Pedantic remark: zmod 0 is not defeq to fin 0 :sweat_smile: