finish uses all hypotheses

Stream: general

[Floris van Doorn]

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

#lint

-- #explode foo

[Jeremy Avigad]

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]

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]

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

[Jeremy Avigad]

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

[Jannis Limperg]

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]

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]

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.