Unused linter with `by_cases`

Stream: lean4

[Yury G. Kudryashov]

Here is an #mwe:

import Mathlib

lemma bycases_unused (n : ℕ) : n = 1 → 1 + 2 = 3 := by
  by_cases hn : n = 1
  · rw [hn]; intro; rfl
  · intro; rfl

#lint

reports no errors. AFAIR, we had a linter in mathlib3 that checked for this kind of "unused". Is it hard to reimplement in Lean 4?

[Yury G. Kudryashov]

I tried both with by_cases (generates if .. then .. else ..) and cases eq_or_ne n 0 (generates Or.casesOn)

[Yury G. Kudryashov]

I recently found an unneeded by_cases in a longer proof in Mathlib, this :up: is a minimized version.

[Mario Carneiro]

(PSA: please don't use import Mathlib in MWEs)

[Yury G. Kudryashov]

1. That's not what #mwe says.
2. I used import Mathlib intentionally to be sure that I run all Mathlib linters.

[Mario Carneiro]

"mathlib linters" aren't defined in mathlib anymore, they are in Std now

[Mario Carneiro]

in particular the one you are talking about here is in std

[Mario Carneiro]

the reason for the issue is that you did the case split before the intro, so it's not just an unused variable

[Mario Carneiro]

with

theorem bycases_unused (n : ℕ) : n = 1 → 1 + 2 = 3 := by
  intro h
  by_cases hn : n = 1
  · rw [hn] at h
  · rfl

the linter does trigger

[Mario Carneiro]

I would expect the lean 3 linter to have the same behavior here

[Yury G. Kudryashov]

The actual proof was more like

lemma comm2 (m : Nat) : 2 * m = m * 2 := by
  by_cases hm : m = 0
  · rw [hm]; rfl
  · apply Nat.mul_comm

[Yury G. Kudryashov]

I'll test mathlib linter now.

[Mario Carneiro]

that doesn't have an unused variable

[Yury G. Kudryashov]

Indeed, Lean 3 doesn't catch it too. Can we catch this (may be, not on the fly, if it takes time)?

[Mario Carneiro]

sure but what are you looking for

[Yury G. Kudryashov]

One of the branches of by_cases ignores the assumption, thus we can drop the by_cases.

[Yury G. Kudryashov]

And similarly for cases (though this can be more tricky)

[Yury G. Kudryashov]

A related request: report unused have := something, not only have h := something.

[Yury G. Kudryashov]

I'm cleaning up some have _ := now.

[Eric Rodriguez]

If this is turned into an em with rcases (not cases, that's got a bug open) the linter will trigger. Not that I think we should get rid of by_cases

[Yury G. Kudryashov]

Indeed, rcases eq_or_ne m 0 with rfl | hm triggers the linter.

[Yury G. Kudryashov]

Or do you mean something else?

[Eric Rodriguez]

Yes, I do mean that!