Zulip Chat Archive

Stream: new members

Topic: tidy intercalation


view this post on Zulip 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 tidy).

view this post on Zulip Horatiu Cheval (Apr 03 2021 at 08:13):

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.

view this post on Zulip 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 thattidy does are not needed for the final argument.

view this post on Zulip 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