rewrite sometimes substitute both sides of the equation

Stream: new members

[Trung Tran]

Good evening! I am new to Lean and I have a question about a phenomenon that is not well documented online.
I have noticed that some times, the rewrite command replaces multiple occurrence of the pattern found. In particular, in the Mathematics in Lean book, I found:

import algebra.ring
namespace my_ring
variables {R : Type*} [ring R]

theorem add_neg_cancel_right (a b : R) : (a + b) + -b = a :=
by rw [add_assoc, add_right_neg, add_comm, zero_add]

theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c :=
   calc
    a
      = (a + b) + -b : by rw [← add_neg_cancel_right]
  ... = (c + b) + -b : by rw [← h]
  ... =  c           : by rw [add_assoc, add_comm b, add_left_neg, add_comm, zero_add]
-- END

end my_ring

I want to replace 'a' by '(a + b) + -b' only on the left side, but Lean did both sides for me, which is not what I wanted... Could someone help me with this?

[Patrick Massot]

You're looking for #backticks

[Patrick Massot]

(I'm talking about your Zulip issue first)

[Trung Tran]

Patrick Massot said:

You're looking for #backticks

I got it! Thanks!

[Patrick Massot]

rw will replace every occurrence of a single pattern.

[Trung Tran]

Patrick Massot said:

rw will replace every occurrence of a single pattern.

I also observe that Lean replaces all patterns (some are very complex)

Is there a way to specify only the first or second pattern, or left/right side?

[Patrick Massot]

One possible answer is https://leanprover-community.github.io/extras/conv.html

[Patrick Massot]

There are simpler answers for simpler cases but that one is the most flexible one.

[Patrick Massot]

I don't understand your example, it seems to have independent issues.

[Trung Tran]

Patrick Massot said:

I don't understand your example, it seems to have independent issues.

Professor Massot, are you referring to the example code that I posted?

[Patrick Massot]

Yes. I think the issue is your rw [← add_neg_cancel_right] has no way to infer who is b.

[Trung Tran]

Patrick Massot said:

Yes. I think the issue is your rw [← add_neg_cancel_right] has no way to infer who is b.

I have updated again:

import algebra.ring
namespace my_ring
variables {R : Type*} [ring R]

theorem add_neg_cancel_right (a b : R) : (a + b) + -b = a :=
by rw [add_assoc, add_right_neg, add_comm, zero_add]

theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c :=
   calc
    a
      = (a + b) + -b : by rw [← add_neg_cancel_right a b]
  ... = (c + b) + -b : by rw [← h]
  ... =  c           : by rw [add_assoc, add_comm b, add_left_neg, add_comm, zero_add]
-- END

end my_ring

[Trung Tran]

If I change the code back to

rw [add_neg_cancel_right a b]

then it works very well, it just substituted my right hand side :)

[Patrick Massot]

Ok, here you see the announced behavior. Given rw [← add_neg_cancel_right a b] goes looking for the pattern a. It sees it twice (one on each side), hence it rewrites twice. You can fix this by using conv_lhs { rw [← add_neg_cancel_right a b] } to go only to the left-hand side.

[Trung Tran]

Thank you for your answer, Professor Massot! I will try that and also read the link that you sent!

[Patrick Massot]

or conv { to_lhs, rw ← add_neg_cancel_right a b } or many other variations.

[Mario Carneiro]

You are using bash syntax highlighting btw, you can just write ``` with no language specifier and it will default to "lean"

[Trung Tran]

Btw, is there an advantage to having lean syntax? Can we just run it on the server... I am just wondering

[Patrick Massot]

Yes you can.

[Patrick Massot]

Try to switch to lean syntax and you'll get a new icon on the upper-right corner of your code area.

[Patrick Massot]

Of course this will work only if the Lean snippet is autonomous.

[Trung Tran]

Thank you for telling me that. I will start posting self-contained codes from now on.

[Patrick Massot]

The important point is to post self-contained code in the first message of a thread, because it makes it much easier to help you, as explained in #mwe. The Lean javascript version is mostly a nice bonus.