Use of Tactics

Stream: new members

[Alex Zhang]

Suppose I have some goal like a+a+b <= d+c+a and I would like to change the second "a" on the LHS to "a+0", how can I make this change?

[Hanting Zhang]

nth_rewrite 2 [add_zero a]

[Hanting Zhang]

docs#nth_rewrite Nevermind that doesn't work. nth_rewrite essentially allows you to rw with more precision

[Scott Morrison]

Or use conv mode, which lets you select subexpressions to work on.

[Scott Morrison]

Maybe tactic#nth_rewrite?

[Alex Zhang]

@Hanting Zhang It seems not to work for me as add_zero is from a+0 to a, but what I want is to rewrite in the other direction.

[Scott Morrison]

Use the left arrow to rewrite backwards.

[Alex Zhang]

Do you mean`nth_rewrite←'? This gives me the error message: (small) natural number expected... :hurt:

[Adam Topaz]

nth_rewrite 2 [← add_zero a]

[Adam Topaz]

In general when you're rewriting adding a left arrow in front of the name of the lemma uses that particular lemma in reverse.

[Alex Zhang]

Thanks to all of you!