linter.unusedVariables false positive when used in induction

[sven-manthe]

Prerequisites

• [X ] Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

In some cases, the linter.unusedVariables yields false positives for variables used only in inductions.

Context

This was discussed in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Possible.20linter.2EunusedVariables.20bug

Steps to Reproduce

example (P : Unit → Prop) (H : P () → True) (x : Unit) (h : P x) : True := by
  let h' := h
  cases x
  exact H h'

Expected behavior: No warning occurs.

Actual behavior: The message "unused variable h' [linter.unusedVariables]" is shown.

Versions

Lean (version 4.3.0-rc1, commit baa4b68, Release)
Manjaro Linux 23.0

[Kha]

Must be a general info tree issue

[Kha]

I think we're still missing a tactic version of #1396

[Seasawher]

I have encountered a similar false positive warning.

This is the MWE to reproduce the bug.

variable (α : Type)

def sample (n : Nat) : Nat :=
  match h : n with
  | 0 => 0
  | m + 1 => m + sample (m / 2)
  decreasing_by
    simp [h]
    simp_wf
    exact Nat.lt_of_le_of_lt (Nat.div_le_self _ _) (Nat.lt_succ_self _)

related : https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/False.20Positive.20Warning.3A.20.60linter.2EunusedVariables.60

[semorrison]

@Seasawher, I think this is an independent issue, that nothing is checking for usages in a decreasing_by clause. Could you open your example as a separate issue?

[Seasawher]

done #2920