Zulip Chat Archive

Stream: new members

Topic: casting and adding in zmod


view this post on Zulip Rose Lopez (Jul 24 2020 at 22:17):

Hi! I am trying to simplify a goal:

 (x + y) = x + y

so I made a have statement

have add : (x : zmod n) + (y : zmod n) = ((x + y) : zmod n),

and the proof consisted of rfl

but afterwards, in the tactic state I see this,

add : x + y = x + y

and so my add statement is not helpful. Why is the goal state not recognizing that I casted then added in LHS and added then casted in RHS?

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:19):

If you're using mathlib and you have import tactic at the top of your file, then norm_cast might solve this goal for you.

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:21):

The answer to your cast question is that Lean casts x and y on the left hand side, and then it looks at the right hand side and says "OK so it says add x y and I read from left to right, and this is supposed to be an element of zmod n so add must be addition in zmod n, so the elements must be in zmod n, oh gosh they aren't, I'd better cast them.

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:22):

You have to change the right hand side to `((x + y : int) : zmod n) (or whatever the type of x and y actually are, to ensure the right kind of addition is done)


Last updated: May 13 2021 at 21:12 UTC