finish vs tidy

Stream: general

[Stuart Presnell]

I was just trying to prove something involving a term n : ℕ+. I first tried hitting the problem with finish, which thought for a while and failed. Then I tried tidy?, which immediately found the solution cases n, refl. Why wouldn't finish be able to find this simple solution? Would it make sense to edit the finish tactic to add whatever cleverness tidy used in this case?

[Stuart Presnell]

For context (and in lieu of a #mwe), this was in proving factorization_equiv_apply in #11440.

[Yaël Dillies]

finish is being phased out, so the solution here is to not use it.

[Stuart Presnell]

Well, I suppose that's fair, and I wasn't intending to leave finish in the final version to PR into mathlib. But in the mean time it's still a useful tool to confirm that the thing I'm trying to prove is in fact true and that I haven't messed up somewhere. And presumably there will be a replacement for it in Lean 4 that will be based (at least to some extent) on whatever ends up being the most recent version of finish.

[Johan Commelin]

I don't know exactly what finish does, but it is in some sense much more specialized than tidy, I think.

[Alex J. Best]

Yes I think the role of finish and tidy is different enough that we shouldn't necessarily try to make them converge. Especially given that one of the main issues with these tactics is their runtine adding more work to finish seems like it might cause problems

[Yaël Dillies]

Stuart Presnell said:

And presumably there will be a replacement for it in Lean 4 that will be based (at least to some extent) on whatever ends up being the most recent version of finish.

That's the thing. It won't. But there will be indeed others that will replace it.

[Kyle Miller]

My limited understanding is that finish searches for a proof using @[ematch] lemmas -- it's supposed to be an SMT solver tactic.