Zulip Chat Archive

Stream: general

Topic: finish vs tidy


Stuart Presnell (Feb 03 2022 at 13:57):

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 (Feb 03 2022 at 13:57):

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

Yaël Dillies (Feb 03 2022 at 13:58):

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

Stuart Presnell (Feb 03 2022 at 14:19):

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 (Feb 03 2022 at 14:22):

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

Alex J. Best (Feb 03 2022 at 14:40):

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 (Feb 03 2022 at 14:40):

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 (Feb 03 2022 at 18:08):

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


Last updated: Dec 20 2023 at 11:08 UTC