simp_rw: New favorite tactic?

Stream: new members

[Dan Abramov]

I'm finding myself using simp_rw often instead or rw or simp (only).

Feels like a perfect tactic:

• More powerful than rw and can reach deeper
• Doesn't introduce magic or hang, each rewrite is chosen explicitly
• Errors if the rewrite doesn't clearly apply
• Don't need to worry about it being non-terminal

Should it be promoted more? It seems really nice.

[Aaron Liu]

simp_rw will rewrite all occurrences of the pattern, so you have less control with what gets rewritten

[Aaron Liu]

It also won't leave assumptions in the thing you're rewriting by as side goals

[Shreyas Srinivas]

I would like to see simp_rw upstreamed. Unfortunately this involves pushing code across the mighty FROwall. There are so many times in iris when I am doing this intro _ ; rw ...; revert pattern.

[Henrik Böving]

Dan Abramov said:

I'm finding myself using simp_rw often instead or rw or simp (only).

Feels like a perfect tactic:

• More powerful than rw and can reach deeper
• Doesn't introduce magic or hang, each rewrite is chosen explicitly
• Errors if the rewrite doesn't clearly apply
• Don't need to worry about it being non-terminal

Should it be promoted more? It seems really nice.

The FRO is working on a more powerful rewrite tactic that can handle these kinds of situations: https://lean-lang.org/fro/roadmap/1900-1-1-the-lean-fro-year-3-roadmap/#4.-proof-automation

[Shreyas Srinivas]

How long will that take? I am working on iris now

[Kyle Miller]

Dan Abramov said:

• Doesn't introduce magic or hang, each rewrite is chosen explicitly

Are you describing simp_rw with this one? That sounds like rw to me. The simp_rw tactic gives you no way to explicitly choose what you want to rewrite, nor how many times it should iterate its rewriting, and it can get stuck doing infinite loops.

Similarly, with "Errors if the rewrite doesn't clearly apply", you only get a "no progress" error. It's no better than rw.

Maybe you're comparing simp_rw and simp, not simp_rw and rw.

By the way, conv => enter [...position string...]; rw [thm] is a good way to rewrite where you want. @Shreyas Srinivas There's no need for intro; rw; revert because of this.

[Aaron Liu]

I do sometimes do revert h; rw [eq]; intro h

[Kyle Miller]

That's very different @Aaron Liu. That's to deal with dependencies among hypotheses; intro/rw/revert on the other hand is to rewrite within the body of a pi/let/lambda.