rewriting have in goal

Stream: lean4

[Pavel Klimov]

Is there a way to rewrite specific have in goal without manually writing meta code?

Here is small example.

example (a : Nat): have v := 2 * (a * 5); v = a * 10 := by
  rw [← Nat.mul_comm]
  trace_state
  rw [Nat.mul_assoc]

This works well if I rewrite globally. But is there a way to rewrite specific have / let inside a goal?

[Jakub Nowak]

You can try selecting specific let/have with the conv mode.

[Jakub Nowak]

Like this for example. Though, I didn't find a way to select have by its variable name

example (a : Nat) : have v := 2 * (a * 5); have v2 := a * 10; v = v2 + 1 := by
  conv in 2 * (a * 5) =>
    rewrite [← Nat.mul_comm, Nat.mul_assoc]
    simp only [Nat.reduceMul]

[Pavel Klimov]

Thanks for a reply. But in my case the have expression is way too long and I don't want to copy-paste it in the code.

[Kevin Buzzard]

Do you know about conv? in Mathlib? Then you can select terms by shift-click.

[Aaron Liu]

this is one of the fun ones because there's no way to fill in an enter [...] string that navigates into the value of a let or have

[Jakub Nowak]

Kevin Buzzard said:

Do you know about conv? in Mathlib? Then you can select terms by shift-click.

I didn't. But it looks like it doesn't work "Rpc error: InternalError: conv mode does not yet support entering let values"

[Aaron Liu]

and this is just a limitation of enter [...]

[Jakub Nowak]

Pavel Klimov said:

Thanks for a reply. But in my case the have expression is way too long and I don't want to copy-paste it in the code.

You don't have to copy-paste in entire expression. You can try to make an unambiguous pattern:

example (a : Nat) : have v := 2 * (a * 5); have v2 := a * 10; v = v2 + 1 := by
  conv in _ * (_ * _) =>
    rewrite [← Nat.mul_comm, Nat.mul_assoc]
    simp only [Nat.reduceMul]

or

example (a : Nat) : have v := 2 * (a * 5); have v2 := a * 10; v = v2 + 1 := by
  conv in 2 * _ =>
    rewrite [← Nat.mul_comm, Nat.mul_assoc]
    simp only [Nat.reduceMul]