Zulip Chat Archive

Stream: new members

Topic: Unfold sum over zmod


view this post on Zulip Adrián Doña Mateo (Oct 26 2020 at 15:20):

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

view this post on Zulip Mario Carneiro (Oct 26 2020 at 15:21):

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

view this post on Zulip Mario Carneiro (Oct 26 2020 at 15:21):

the rfl proof should still work

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 15:23):

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

view this post on Zulip Kevin Buzzard (Oct 26 2020 at 15:23):

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

view this post on Zulip Mario Carneiro (Oct 26 2020 at 15:25):

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]

view this post on Zulip Yakov Pechersky (Oct 26 2020 at 15:32):

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

view this post on Zulip Mario Carneiro (Oct 26 2020 at 15:36):

they are actually defeq I think

view this post on Zulip Mario Carneiro (Oct 26 2020 at 15:38):

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]

view this post on Zulip Adrián Doña Mateo (Oct 26 2020 at 15:40):

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!

view this post on Zulip Johan Commelin (Oct 26 2020 at 15:44):

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


Last updated: May 13 2021 at 18:26 UTC