Zulip Chat Archive

Stream: new members

Topic: Apply a rewrite on a precise term


view this post on Zulip Hamza Maimoune (Feb 08 2020 at 14:22):

Hello everyone,

I would like to ask you if there is a way to apply a rewrite tactic on a particular term. For example, if I want to replace only the second term of an expression.

Thank you.

view this post on Zulip Ryan Lahfa (Feb 08 2020 at 14:30):

You can perform something like:

conv_rhs {
  rw [what you want]
}

It'll rewrite the right hand only.
Inside of a conv block, you can use congr in order to split parts of your equation, like if you have A * B, congr will give you two goals A then B, you can use skip to through some you don't want.

view this post on Zulip Kevin Buzzard (Feb 08 2020 at 14:32):

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md might help

view this post on Zulip Hamza Maimoune (Feb 08 2020 at 14:38):

Thank you both

view this post on Zulip Patrick Massot (Feb 08 2020 at 20:30):

@Hamza MAIMOUNE , please also try:

example (a b : ) (h : a = b): a + a + a + a + a = 0 :=
begin
  rw [h] {occs := occurrences.pos [1, 3]},
  sorry,
end

The syntax is awfully verbose but it can still be quicker than a complicated conv navigation.


Last updated: May 13 2021 at 22:15 UTC