Single rewrite with simp

Stream: lean4

[Tomas Skrivan]

Is there a way to restrict simp to perform at most one rewrite? Setting singlePass to true is really helpful, but it can actually perform multiple rewrites.

I'm in a scenario when a single pass is doing some rewrites but the whole pass takes me back to the original goal. I can make sense of what is happening from the trace but I would like to play with the goal after a single rewrite to figure out how to prevent the loop.

[Tomas Skrivan]

Also is there a tactic to run only beta reduction? There is delta, but no other like beta, zeta, eta, iota.

[Arthur Paulino]

This question is somewhat similar to one of my first questions here on Zulip:
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/behaviour.20of.20simp.20in.20Lean.20vs.20Coq/near/258537903

[Arthur Paulino]

I wanted to know if there was a way to have full control over simp

[Gabriel Ebner]

If you want to only rewrite some occurrences, then you could try the conv tactic which allows you to "zoom" in on subterms and only run simp there.

[Gabriel Ebner]

There is also rw, which restricts rewriting in another way. (It only rewrites once, not under binders, but it rewrites all occurrences of the same term.)

[Tomas Skrivan]

Yes I'm familiar with conv and rw but what I'm asking is more for debugging simp. I just want a single rewrite of simp. I can achieve this by running simp, looking at the trace, finding the name of the first rewrite and then manually doing the rewrite with rw. I find this tedious.

[Tomas Skrivan]

Ohh I can get beta, zeta, ... with simp (config := { ... }) only

[Mac]

(deleted)