unusedHavesSuffices false positive

Stream: mathlib4

[Sky Wilshaw]

I think the unusedHavesSuffices linter is giving me a false positive on this theorem:

@[simp]
theorem xgcd_zero_left {s t r' s' t' : R} : xgcdAux 0 s t r' s' t' = (r', s', t') := by
  unfold xgcdAux
  exact if_pos rfl

It gives unnecessary have this : EuclideanDomain.r (r' % r) r, and in the definition xgcdAux there's the line have : r' % r ≺ r := mod_lt _ hr (where locally ≺ means EuclideanDomain.r) which is needed for the termination check with well-founded recursion. What's the best fix? Maybe this is a bug with the linter, or maybe I'm missing something obvious.

[Sky Wilshaw]

Replacing the have : with have _ : stops the linter complaining, but is this the best solution?

[Kevin Buzzard]

What happens if you just delete the unfold line?

[Sky Wilshaw]

The exact line doesn't work in that case:

type mismatch
  if_pos rfl
has type
  (if ?m.20158 = ?m.20158 then ?m.20160 else ?m.20161) = ?m.20160 : Prop
but is expected to have type
  xgcdAux 0 s t r' s' t' = (r', s', t') : Prop

[Sky Wilshaw]

I think this happens because xgcdAux is defined through well-founded recursion and the equation compiler.

[Mario Carneiro]

do you have a MWE?

[Sky Wilshaw]

I've minified it a little.

import Mathlib.Tactic.Basic

variable (r : Nat → Nat → Prop) (hr : WellFounded r) (hz : ∀ x, r 0 x)

def foo (hr : WellFounded r) : Nat → Nat
  | a => if true then
      0
    else
      have := hz a;
      foo hr 0
  termination_by' ⟨_, hr⟩

theorem foo_id : foo r hz hr 0 = 0 := by
  unfold foo
  rfl

#lint

Unfortunately there are still a few moving parts, I'm not sure what precisely causes it.