How to `generalize` in specific locations in the goal

Stream: lean4

[Gustavo Goretkin]

I have a goal:

transduce_helper StateMachineType.Moore i o moore moore.s0 is =
  transduce_helper StateMachineType.Mealey i o
    { state_space := moore.state_space, s0 := moore.s0, transition := moore.transition,
      output := fun x x_1 => moore.output x }
    moore.s0 is

I want to generalize moore.s0 = s on 2 of the 3 occurrences. I want to leave s0 := moore.s0 alone.

The way I'm doing it now is

  generalize H : moore.s0 = s
  conv =>
    rhs
    rw [← H]
    congr
    . rw [H]
    . skip
  clear H

Is there a more straightforward way?

[Gustavo Goretkin]

The full context is here: https://gist.github.com/goretkin/623625fbeefe930a135d1390c81f70ce

[Kyle Miller]

Maybe you can use the rw (occs := [1,2]) [...] syntax? That rewrites just occurrences 1 and 2 for example.

The generalize syntax doesn't give any access to occs

[Gustavo Goretkin]

Thanks, I will try that! How do I split up what generalize H : foo = bar int o two pieces so that I have an H I can give to rw (occs := .pos [1, 2]) [H] (or i might be missing the bigger picture)

[Robin Arnez]

You can use the set! tactic: set! bar := foo with H and then rewrite or conv or whatever

[Robin Arnez]

Actually that might not work quite how you'd like...

[Robin Arnez]

I'm assuming you want to generalize because of induction?

[Robin Arnez]

Then perhaps it is simpler to avoid generalization and use let rec instead

[Gustavo Goretkin]

I ended up doing

  generalize H : moore.s0 = s
  rewrite (config := {occs := .pos [2]}) [← H]
  clear H
  revert s

which is nicer than what I had before.

[Gustavo Goretkin]

I don't see the set! tactic

[Kyle Miller]

A hack is you could do generalize H : moore.s0 = s at h where h is some hypothesis that doesn't contain moore.s0. That will prevent moore.s0 from being replaced in the goal. I'm not recommending this though.

There's also doing something like let s := moore.s0, then using change to replace certain occurrences, and then clear_value s. It's not that great of an experience.

Are you on an old Lean? You should be able to write

rewrite (occs := [2]) [← H]

these days.

[Kyle Miller]

Robin's suggestion of set! is a mathlib tactic. It's in Mathlib.Tactic.Set. The ! causes set to not rewrite.