Zulip Chat Archive

Stream: new members

Topic: casting and adding in zmod

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?

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.

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.

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: Dec 20 2023 at 11:08 UTC