Zulip Chat Archive

Stream: new members

Topic: rewrite sometimes substitute both sides of the equation


Trung Tran (Dec 28 2020 at 22:11):

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 (Dec 28 2020 at 22:12):

You're looking for #backticks

Patrick Massot (Dec 28 2020 at 22:12):

(I'm talking about your Zulip issue first)

Trung Tran (Dec 28 2020 at 22:13):

Patrick Massot said:

You're looking for #backticks

I got it! Thanks!

Patrick Massot (Dec 28 2020 at 22:14):

rw will replace every occurrence of a single pattern.

Trung Tran (Dec 28 2020 at 22:16):

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 (Dec 28 2020 at 22:17):

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

Patrick Massot (Dec 28 2020 at 22:17):

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

Patrick Massot (Dec 28 2020 at 22:18):

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

Trung Tran (Dec 28 2020 at 22:20):

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 (Dec 28 2020 at 22:21):

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

Trung Tran (Dec 28 2020 at 22:23):

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 (Dec 28 2020 at 22:24):

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 (Dec 28 2020 at 22:26):

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 (Dec 28 2020 at 22:27):

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

Patrick Massot (Dec 28 2020 at 22:28):

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

Mario Carneiro (Dec 28 2020 at 22:28):

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

Trung Tran (Dec 28 2020 at 22:32):

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

Patrick Massot (Dec 28 2020 at 22:33):

Yes you can.

Patrick Massot (Dec 28 2020 at 22:33):

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

Patrick Massot (Dec 28 2020 at 22:33):

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

Trung Tran (Dec 28 2020 at 22:38):

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

Patrick Massot (Dec 28 2020 at 22:40):

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.


Last updated: Dec 20 2023 at 11:08 UTC