choosing where we rewrite

Stream: new members

[Antoine Labelle]

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?

[Adam Topaz]

Take a look at tactic#nth_rewrite

[Adam Topaz]

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

[Antoine Labelle]

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

[Adam Topaz]

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

[Adam Topaz]

Which compiles fine.

[Adam Topaz]

Are you using a recent version of mathlib?

[Antoine Labelle]

Yeah I downloaded it just today :)

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Antoine Labelle]

Weird...

[Floris van Doorn]

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.

[Kevin Buzzard]

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?

[Kevin Buzzard]

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.

[Antoine Labelle]

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