Stream: new members
Topic: tidy intercalation
Horatiu Cheval (Apr 03 2021 at 08:10):
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
Horatiu Cheval (Apr 03 2021 at 08:13):
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 (Apr 03 2021 at 11:07):
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 that
tidy does are not needed for the final argument.
Damiano Testa (Apr 03 2021 at 11:08):
I would probably also repeat this process after the second
tidy and leave a
tidy-free proof, but is not required, I think.
Last updated: May 12 2021 at 04:19 UTC