Zulip Chat Archive

Stream: general

Topic: finish uses all hypotheses

Floris van Doorn (Dec 29 2020 at 08:30):

In the example posted in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Icc_ssubset_Icc the hypothesis hI₁ is "unused", except that finish seems to revert and intro back all hypotheses in the context, which makes hI₁ occur in the final proof term. Therefore #lint cannot catch the unused argument.
Is there a way to change finish so that it doesn't do this? (I didn't really investigate why finish does this.) Here is a minimized example:

import data.nat.basic

lemma foo {n : } (h : 5 < n) : 0  n :=
by finish


-- #explode foo

Jeremy Avigad (Jan 01 2021 at 20:23):

I don't think it is worth the effort. I wrote finish in 2016-2017 when Lean's metaprogramming language was still new. It was an experiment to see whether it would be sufficient to implement something like Isabelle's auto. I gave up when I determined that to do it right one would have to implement better low-level matching heuristics and primitives, and that it would have to be in C++ for performance. I was not up to that. I am pleased but slightly surprised that people still find finish useful sometimes, but I still think of it as a failed attempt at auto.

Is the problem specific to finish? IIRC, other tactics (like simp * at *, which finish uses) revert hypotheses and reintroduce them. But maybe finish does it too crudely where other tactics are more intelligent.

BTW, I think it would make a great project to do finish right in Lean 4. Isabelle's internal automated tools, auto, arith, and simp, are incredibly useful. Our simp and linarith are pretty good approximations to Isabelle's, but we have nothing like auto. In Lean 4, we should be able to get something even more performant and flexible.

Jannis Limperg (Jan 01 2021 at 21:10):

I'm just getting started on exactly this project. :) (Maybe with a prototype in Lean 3 first.) I'll be giving a talk with some extremely preliminary design ideas -- really more an invitation to discuss the design -- at Lean Together.

Kevin Buzzard (Jan 01 2021 at 21:19):

After that can you do omega and then groebner_basis? :-)

Jeremy Avigad (Jan 01 2021 at 21:24):

Jannis, I remember that you expressed interest in this before. I am happy to hear that it's still in scope!

Jannis Limperg (Jan 01 2021 at 21:25):

I've already successfully deflected Sander's requests for Gröbner bases. The problem with these tactics is that it would be really hard to dress them up as original research, so we'd need a BSc or MSc to do them.

Sebastien Gouezel (Jan 01 2021 at 21:37):

As for auto in Isabelle, if I understand correctly it is not described properly in any paper (or anywhere), so there is certainly something useful to be written on this!

Jannis Limperg (Jan 01 2021 at 21:47):

Yeah, I was told the same thing and haven't found any detailed docs so far. I suspect the type theory might get in the way as well, so I'm not worried about a lack of technical challenges.

Last updated: Dec 20 2023 at 11:08 UTC