Terminal tidy

Stream: general

[Yaël Dillies]

Is tidy considered a terminating tactic? https://github.com/leanprover-community/mathlib/pull/15389/files/9ebe54c697b0c1165a203db78e5eca94a8033ee6#diff-7a8472e52cb49fd874716f00c555dd1171780c533169748523156bc57388110f is the second time I hear that "tidy has nonterminal simps in it" recently and this makes no sense to me given that I see tidy as a terminating tactic.

[Mario Carneiro]

yes, nonterminal tidy is bad for the same reason as nonterminal simp

[Mario Carneiro]

in particular, it uses simp so using it nonterminally is also using simp nonterminally

[Mario Carneiro]

if you use tidy terminally then it doesn't matter whether simp is called in the middle of tactic execution

[Yaël Dillies]

Okay, that's what I thought too! cc @Bhavik Mehta

[Adam Topaz]

I think tidy is more or less just repeatedly applying intros, ext, dsimp (at *) and/or simp (at *) in some order.

[Bhavik Mehta]

Adam Topaz said:

I think tidy is more or less just repeatedly applying intros, ext, dsimp (at *) and/or simp (at *) in some order.

Yeah this is what I was worried about - a terminal tidy then can be doing simp, intros, simp, for instance, which means you're doing nonterminal simps

[Bhavik Mehta]

Mario Carneiro said:

if you use tidy terminally then it doesn't matter whether simp is called in the middle of tactic execution

Why doesn't this matter? Doesn't it cause the exact same issues as nonterminal simps - adding new lemmas to the simp list can cause a tidy which previously succeeded to now fail

[Yaël Dillies]

If you want to ban any tactic invokation that may fail in the future, you're going to have a rough time. Terminal simps are allowed because, even if they break, the goal before the invokation is "obvious" by design, hence the invokation won't be hard to fix.

[Yaël Dillies]

In that regard, terminal tidies are just the same, because solving a goal with tidy means that it was "obvious" to start with.

[Praneeth Kolichala]

Bhavik Mehta said:

Adam Topaz said:

I think tidy is more or less just repeatedly applying intros, ext, dsimp (at *) and/or simp (at *) in some order.

Yeah this is what I was worried about - a terminal tidy then can be doing simp, intros, simp, for instance, which means you're doing nonterminal simps

Moreover, unlike the situation of manually writing simp, intros, simp, if simp changes, tidy will likely be able to “fix itself” so the proofs are less brittle

[Mario Carneiro]

Right, this is the point. A tactic isn't a fixed sequence of steps, it can react to the changes in behavior and do something else

[Mario Carneiro]

the danger behind nonterminal simp is when you have something "rigid", that requires a specific goal, coming after something "fancy", with changing behavior

[Mario Carneiro]

"rigid" after "rigid" and "fancy" after "rigid" is no problem because there are not many proof changes, while "fancy" after "fancy" is okay because the second fancy tactic adapts to any changes in the first one

[Mario Carneiro]

the only problematic one is "rigid" after "fancy" since the rigid proof can't adapt to the change

[Bhavik Mehta]

So does this mean the points here about avoiding tidy in mathlib proofs are no longer applicable? https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60tidy.60.20in.20mathlib.20proofs

[Mario Carneiro]

I think that's a different issue: tidy is a slow tactic so replacing it with the generated proof is often an improvement

[Mario Carneiro]

but the generated proof is more brittle to changes

[Mario Carneiro]

well, it's not entirely unrelated: the fact that tidy is slow is correlated with the fact that it's also very adaptable to changes in the library

[Bhavik Mehta]

Perhaps I'm just overly cautious about this then, since I've spent a lot of time fixing broken tidy proofs!

[Mario Carneiro]

what do you mean by "broken tidy proof"? Is it a tidy invocation itself that no longer works, or a tidy-generated script that fails?

[Kevin Buzzard]

If I ever use tidy in a proof then the next thing I do is tidy? and then try to write a sensible proof given the output. There are of course secret tidy proofs in category theory, where people don't fill in terms when making a structure and . obviously kicks in, invokving tidy.

[Bhavik Mehta]

Mario Carneiro said:

what do you mean by "broken tidy proof"? Is it a tidy invocation itself that no longer works, or a tidy-generated script that fails?

A tidy invocation that no longer works