Zulip Chat Archive

Stream: new members

Topic: Apply a rewrite on a precise term

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.

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.

Kevin Buzzard (Feb 08 2020 at 14:32):

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

Hamza Maimoune (Feb 08 2020 at 14:38):

Thank you both

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 :=
  rw [h] {occs := occurrences.pos [1, 3]},

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

Last updated: Dec 20 2023 at 11:08 UTC