`linter.unusedVariables` false positive when used in `decreasing_by`

[Seasawher]

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.

Context

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

Steps to Reproduce

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 _)

Expected behavior: No warning occurs.

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

Versions

Lean "4.3.0-rc2" OS: lean playground's OS version

[nomeata]

Thanks for the report!

NB: simp doesn't seem to actually need the h, maybe that’s part of it?

variable (α : Type)

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

works, as does

variable (α : Type)

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

[m4lvin]

I just ran into another example of this, and removing the variable here does break it.

Click for playground%20%3A%0A%20%20%20%20%CE%B1%20%E2%86%92%20Finset%20%CE%B1%0A%20%20%7C%20x%20%3D%3E%20%7Bx%7D%20%E2%88%AA%20(f%20x).attach.biUnion%20(fun%20%E2%9F%A8y%2C%20y_in%E2%9F%A9%20%3D%3E%20fTransReflSingle%20f%20h%20m%20isDec%20y)%20--%20unused%20variable%20%60y_in%60%20...%0Atermination_by%0A%20%20fTransReflSingle%20f%20h%20m%20isDec%20S%20%3D%3E%20m%20S%0Adecreasing_by%20simpwf%3B%20apply%20isDec%20x%20%20y_in%20---%20...%20but%20it%20is%20used%20here!%0A)

import Mathlib.Data.Finset.Basic

def fTransReflSingle {α : Type}
    (f : α → Finset α)
    (h : DecidableEq α)
    (m : α → ℕ)
    (isDec : ∀ (x : α), ∀ y ∈ (f x), m y < m x) :
    α → Finset α
  | x => {x} ∪ (f x).attach.biUnion (fun ⟨y, y_in⟩ => fTransReflSingle f h m isDec y) -- unused variable `y_in` ...
termination_by
  fTransReflSingle f h m isDec S => m S
decreasing_by simp_wf; apply isDec x _ y_in --- ... but it is used here!

[danielschemmel]

I ran into another example of this issue on stable (version 4.4.0, commit ca7d6dadb9e1, Release), which only uses exact (and sorry to "prove" the theorem it uses):

theorem halving_goes_to_zero (n: Nat): ¬(n = 0) -> n / 2 < n := by sorry

def pow (a : Nat) (b : Nat): Nat :=
  if b_is_not_zero: b = 0 then  -- "unused variable `b_is_not_zero` [linter.unusedVariables]"
    1
  else
    let a' := pow a (b / 2)
    if b % 2 == 0 then
      a' * a'
    else
      a' * a' * a
termination_by _ => b
decreasing_by exact (halving_goes_to_zero b) b_is_not_zero

As expected, removing the variable breaks compilation

[Kha]

@nomeata I can't reproduce any of these on master anymore, apparently some decreasing_by changes fixed them?

[m4lvin]

Hm, but slightly adjusting the example from @danielschemmel still gives the warning here with Lean nightly

theorem halving_goes_to_zero (n: Nat): ¬(n = 0) -> n / 2 < n := by sorry

def pow (a : Nat) (b : Nat): Nat :=
  if b_is_not_zero : b = 0 then  -- unused variable `b_is_not_zero`
    1
  else
    let a' := pow a (b / 2)
    if b % 2 == 0 then
      a' * a'
    else
      a' * a' * a
decreasing_by exact (halving_goes_to_zero b) b_is_not_zero

Is nightly different / much behind master?

[Kha]

My fault, I can see it now

[b-mehta]

I just ran into something I think is similar too:

variable {α : Type}

inductive Tree (α : Type)
| var : α → Tree α
| mul : Tree α → Tree α → Tree α

namespace Tree

inductive bar : Tree α → Prop
| right {x y : Tree α} : bar y → bar (mul x y)
| midCancel {x y z : Tree α} : bar (mul (mul x y) (mul y z))

theorem unusedVariable (x y : Tree α) (h : ¬ bar (mul x y)) :
    bar (mul (mul x y) (mul x y)) → x = y
  | .midCancel => rfl

end Tree

Apologies if this is a different bug, I'm happy to make it a separate report if so.

[nomeata]

This seems to be not about decreasing_by but the pattern match completenes checker, so probably worth its own report.