tidy intercalation

Stream: new members

[Horatiu Cheval]

I have some complicated proof I want to solve by tidy. It almost does it, only after some progress it gets stuck and I use a specialize to advance the goal, after which tidy finishes the proof. So I do something like this:

tidy,
specialize h x,
tidy,

which works fine but looks like an antipattern. Can I merge them into one, or somehow remain only with a terminal tidy? (note that the specialize does not work before the first tidy).

[Horatiu Cheval]

I read tidy supports additional tactics, so I tried local attribute [tidy] tactic.interactive.specialize but nothing changed, though I'm not sure that's the right way of doing it.

[Damiano Testa]

My strategy would be to expand the first tidy with the output of tidy?, tidy up the result so that you get to the stage where specialize, tidy finishes the proof.

In my experience, a lot of the steps thattidy does are not needed for the final argument.

[Damiano Testa]

I would probably also repeat this process after the second tidy and leave a tidy-free proof, but is not required, I think.