Unused `have`s

Stream: mathlib4

[Michael Rothgang]

There are a few unused haves in mathlib, such as the one #28924 is removing. I thought we have the unusedHave linter for this: did something change so it's no longer catching these? (Is this a regression?)

[Ruben Van de Velde]

Yeah, I've noticed the same in PNT+

[Kyle Miller]

Someone needs to review/rewrite the unusedHave linter.

There was a change to Lean where have was encoded as an Expr.letE term instead of using the letFun function, and also Lean aggressively turns lets into haves automatically. This caused a lot of false positives, so unusedHave is mostly disabled now. https://github.com/leanprover-community/batteries/blob/6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d/Batteries/Tactic/Lint/Misc.lean#L231

One kind of false positive was from do notation expansion, which puts unused lets places, which get turned to haves.

The linter is expression-based, which seems really low-level to me. I'm also not sure why it flags only haves. Why not unused lets too?

Something I wonder is, shouldn't the unused variable linter catch these?

If not, then I wonder whether it would be better if this linter used some InfoTree-based approach, since then it could find which expressions were from user-authored haves.

[Kyle Miller]

Possibly there are some heuristics it could use to continue as an expression-based linter. I'm not sure.

[Damiano Testa]

I also found that giving a name to the variable introduced by have gives it a better chance of being picked up by the unusedHave linter, though it is not fail-safe.

[Kyle Miller]

@Damiano Testa Maybe that worked before June — I should have said "disabled" not "mostly disabled".

Given how the code used to work, I'm guessing the Name.isInternal check potentially excluded anonymous haves?

[Damiano Testa]

Ah, my impression could have originated from an older version of mathlib and I had not picked up that this was obsolete.

[Jannis Limperg]

The unused variable linter can catch unused haves, but it needs to be told to look at tactics: set_option linter.unusedVariables.analyzeTactics true. This option used to be on by default (or rather, it didn't exist), but was turned off by default because it can apparently lead to bad performance in corner cases.

A detail I didn't appreciate before I got into this game: a have can be both used and unnecessary, e.g. when a have-introduced hypothesis is used by linarith, but it would also work without that hypothesis. So if you want perfect linting for unused haves, there seems to be no better way than deleting the have and checking whether the proof still compiles.

[Damiano Testa]

The issue with have being used and unnecessary is similar to one of the reasons why the inclusion mechanism for variables changed for theorem: several tactics "touch" all local declarations, making them appear to be "used", when really they were unnecessary.