unused have linter

Stream: mathlib4

[Bolton Bailey]

Mathlib has an unused argument linter, but do we have an unused have linter, i.e. a linter that fires if a have statement is made in a tactic proof but then the conclusion of that have is never used elsewhere in the proof?

[Bolton Bailey]

I mainly have in mind using such a linter for LLM-outputted proofs, which tend to be relatively verbose, and where something like this is more of a concern.

[David Loeffler]

Isn't that what Batteries.Tactic.Lint.unusedHavesSuffices does?

[Bolton Bailey]

Looks like it, thanks!

[Ruben Van de Velde]

But does it work?

[Yaël Dillies]

What would be a nice continuation of this linter is an "unused by_cases" linter which detects proofs of the form

by_cases hP : P
. foo -- doesn't use `P`
. bar

which could be turned into

foo

[Yaël Dillies]

And also (this comes up a lot with alphaproof) proofs of the form

by_cases hP : P
. foo
. bar -- derives a contradiction

which could be turned into

have hP : P := by
  by_contra hP
  bar
foo

[Bolton Bailey]

Ruben Van de Velde said:

But does it work?

Well, it looks like it isn't actively triggering on mathlib by showing warnings the way that the nonterminal simp linter does.

[Kyle Miller]

Ruben Van de Velde said:

But does it work?

No, it currently doesn't do anything. https://github.com/leanprover-community/batteries/blob/bc7b7f567dacc39ae904b6f12f6aa7f90e48e45f/Batteries/Tactic/Lint/Misc.lean#L238

Last discussion: #mathlib4 > Unused `have`s @ 💬

The problem is basically that the Batteries linter operates on the final elaborated expression. It doesn't distinguish between user-written haves and the have expression, and it leads to too many false positives.

[Ruben Van de Velde]

That was my impression, thanks for confirming :)