Zulip Chat Archive

Stream: new members

Topic: choosing where we rewrite


view this post on Zulip Antoine Labelle (Nov 25 2020 at 22:47):

import data.real.basic

variables a b : 

example : abs a - abs b  abs (a - b) :=
begin
   rw [ sub_add_cancel (abs (a - b)) (-abs b), sub_neg_eq_add],
   apply (sub_le_sub_iff_right (abs b)).mpr,
   rw  sub_add_cancel a b,

end

The rw ← sub_add_cancel a b add a -b+b everywhere there is an a, but I just want to do the rewrite in the abs a on the left hand side. Is the a way to specify this?

view this post on Zulip Adam Topaz (Nov 25 2020 at 22:49):

Take a look at tactic#nth_rewrite

view this post on Zulip Adam Topaz (Nov 25 2020 at 22:49):

import data.real.basic

variables a b : 

example : abs a - abs b  abs (a - b) :=
begin
   rw [ sub_add_cancel (abs (a - b)) (-abs b), sub_neg_eq_add],
   apply (sub_le_sub_iff_right (abs b)).mpr,
   nth_rewrite 0 sub_add_cancel a b,
end

view this post on Zulip Antoine Labelle (Nov 25 2020 at 22:54):

Hum I get an unknown identifier 'nth_rewrite' error if I do the same. Do I need to import something?

view this post on Zulip Adam Topaz (Nov 25 2020 at 22:55):

Not sure why... I just copied and pasted the whole contents of the file.

view this post on Zulip Adam Topaz (Nov 25 2020 at 22:55):

Which compiles fine.

view this post on Zulip Adam Topaz (Nov 25 2020 at 22:56):

Are you using a recent version of mathlib?

view this post on Zulip Antoine Labelle (Nov 25 2020 at 22:57):

Yeah I downloaded it just today :)

view this post on Zulip Adam Topaz (Nov 25 2020 at 23:01):

It should work... your installation might be broken in some way.

view this post on Zulip Adam Topaz (Nov 25 2020 at 23:01):

I just tried that code with a fresh project with the most current mathlib, and it works just fine.

view this post on Zulip Adam Topaz (Nov 25 2020 at 23:03):

It even works in the web playground:
https://leanprover-community.github.io/lean-web-editor/#code=import%20data.real.basic%0A%0Avariables%20a%20b%20%3A%20%E2%84%9D%0A%0Aexample%20%3A%20abs%20a%20-%20abs%20b%20%E2%89%A4%20abs%20(a%20-%20b)%20%3A%3D%0Abegin%0A%20%20%20rw%20%5B%E2%86%90%20sub_add_cancel%20(abs%20(a%20-%20b))%20(-abs%20b)%2C%20sub_neg_eq_add%5D%2C%0A%20%20%20apply%20(sub_le_sub_iff_right%20(abs%20b)).mpr%2C%0A%20%20%20nth_rewrite%200%20%E2%86%90sub_add_cancel%20a%20b%2C%0Aend%0A

view this post on Zulip Antoine Labelle (Nov 25 2020 at 23:06):

Weird...

view this post on Zulip Floris van Doorn (Nov 25 2020 at 23:26):

Another way to do things like this is conv_lhs { rw ← sub_add_cancel a b }. See https://leanprover-community.github.io/extras/conv.html for more information about conv-mode.

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 23:33):

Yet another way is to work backwards rather than forwards. You're presumably trying to turn your goal into something where you can finish with abs_add (a - b) b. Why not just tell Lean that's how you want to finish with convert and then pick up the pieces afterwards?

import data.real.basic

variables a b : 

example : abs a - abs b  abs (a - b) :=
begin
   rw [ sub_add_cancel (abs (a - b)) (-abs b), sub_neg_eq_add],
   apply (sub_le_sub_iff_right (abs b)).mpr,
   -- ⊢ abs a ≤ abs (a - b) + abs b
   convert abs_add (a - b) b,
   -- ⊢ a = a - b + b
   simp,
end

But I would be more worried that you can't get a proof compiling which works for everyone else. Did you follow the instructions on the community website?

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 23:35):

If you're working in a Lean project (which you should be) then you can perhaps use something like leanproject upgrade-mathlib to upload the copy of mathlib for that project.

view this post on Zulip Antoine Labelle (Nov 26 2020 at 02:01):

Thanks for the tips, I didn't know about conv_lhs and convert. Also leanproject upgrade-mathlib worked, thanks!


Last updated: May 14 2021 at 13:24 UTC