termination_by? over generalizes the decreasing term

[hargoniX]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following (not quite correct theorem) causes an annoyance with termination_by?:

def copy (curr : Nat) (input : Array Nat) (output : Array Nat) : Array Nat :=
  if hcurr:curr < input.size then
    copy (curr + 1) input (output.push (input[curr]'hcurr))
  else
    output
termination_by input.size - curr

theorem foo (curr : Nat) (input : Array Nat) (output : Array Nat)
    : ∀ (idx : Nat) (hidx1 : idx < curr),
        (copy curr input output)[idx]'sorry
          =
        output[idx]'sorry := by
  intro idx hidx
  unfold copy
  split
  . rw [foo]
    . rw [Array.get_push_lt]
    . omega
  . rfl
termination_by?

Here termination_by? suggests:

Try this: termination_by idx => input.size - curr

Which, while correct, does contain the unused variable idx and will get flagged by the unused
variable linter. It would be great if it only did this for variables that are actually used in
the decreasing term.

Context

This was discovered as part of my work on LeanSAT where lots of theorems of this form (that are actually correct due to additional constraints on the indices) produced slightly "wrong" termination_by? terms.

Expected behavior: Suggest input.size - curr

Actual behavior: Suggest idx => input.size - curr

Versions

"4.8.0-rc1"

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

Thanks! I think when termination_by? was added, the unused variable linter wouldn’t work for termination_by…

Probably just a matter of using the delaborator for binders correctly.