Zulip Chat Archive

Stream: general

Topic: Avoiding repetition in calc mode


view this post on Zulip Eric Wieser (Nov 26 2020 at 22:16):

I just found out you can do this:

lemma ι_add_mul_swap (x y : M) : ι R x * ι R y + ι R y * ι R x = 0 :=
calc _ = ι R (x + y) * ι R (x + y) : by simp [mul_add, add_mul]
   ... = _ : ι_square_zero _

Which saves you from repeating both the LHS and RHS in the calc proof

view this post on Zulip Eric Wieser (Nov 26 2020 at 22:18):

Turns out you can avoid the repetition and even get things in the right order if you ignore the linter:

def ι_add_mul_swap (x y : M) :=  -- I am a def so that my type is inferred from my value
calc ι R x * ι R y + ι R y * ι R x = ι R (x + y) * ι R (x + y) : by simp [mul_add, add_mul]
                               ... = 0 : ι_square_zero _

Last updated: May 13 2021 at 22:15 UTC