Rewrite once

Stream: Is there code for X?

[Ben]

Is there a way to rewrite a pattern once. Say I have d : 0 = 0 + 0 if I rw that on goal 0 = 0 I end up with new goal 0 + 0 = 0 + 0. Is there a way to apply it to only get 0 + 0 = 0?

[Ben]

Even better a rewrite if I can choose what side of the equality to apply it to

[Kevin Buzzard]

Check out the following tactics: tactic#conv_lhs , tactic#conv_rhs and tactic#nth_rewrite . In short there are several ways to do it :-)

[Kevin Buzzard]

Did I dream the first two tactics? I can't find them in the docs

[Yaël Dillies]

They are part of tactic#conv. So it's docs#tactic.conv.conv_lhs. Also worth mentioning tactic#nth_rewrite_lhs, tactic#nth_rewrite_rhs.

[Kyle Miller]

rw has some configuration options too. One is for specifying which occurrences should be rewritten.

example (d : 0 = 0 + 0) : 0 = 0 ↔ sorry :=
begin
  rw [d] { occs := occurrences.pos [1]},
  -- ⊢ 0 + 0 = 0 ↔ sorry
end

(I put the iff sorry in there to prevent rw from closing the 0 = 0 goal automatically with refl!)

[Kyle Miller]

docs#occurrences gives some explanation. The default is occurrences.all

[Scott Morrison]

There is a pretty weird bug/feature in occurrences: if the rule you're rewriting by has variables, they will get "stuck" when traversing the expression, and so it will not find later rewrites with different values of the variables.

Thus:

lemma foo {f : ℕ → ℕ} (d : ∀ i, f i = i) : f 2 ≠ f 3 := begin
  rw [d] { occs := occurrences.pos [2] },
end

fails. This is why nth_rewrite exists, essentially.

[Scott Morrison]

I haven't got around to checking how this behaves in Lean 4, however.

[Ben]

Wow that is cool, didn't know you could provide arguments to tactics like that! nth_rewrite is also perfect + more readable, but good to know it is possible outside of mathlib

[Kyle Miller]

Just to explain this bug/feature (based on my understanding), the occurrences.pos/occurrences.neg is configuring which positions are being rewritten with respect to the positions it would have rewritten without that configuration option. That lemma foo example fails because rw [d] would have only rewritten the f 2 ==> 2.

[Kyle Miller]

This is because rw works by (1) finding something it can rewrite to specialize all the variables in the rewrite lemma then (2) looks for all occurrences, then (3) rewrites all the occurrences (configured by occs) simultaneously using a single eq.rec.

[Scott Morrison]

Maybe I should have called it a feature/bug rather than a bug/feature. Kyle's description makes is sound much more reasonable, but this behaviour can be annoying when you're trying to do a "weird" rewrite.

[Kyle Miller]

This is a good gotcha for occs. I have to admit I've never used it, only nth_rewrite or conv mode!

[Kyle Miller]

It seems like rw should have an extra configuration for how it finds the thing to rewrite in the first place...