Unused variable linter not triggering

Stream: mathlib4

[Daniel Weber]

In docs#SimpleGraph.Walk.getVert_tail, after #16352, the assumption hnp is unused. Why didn't the unused variable linter trigger?

[Kim Morrison]

Hmmmm, that does look suspicious. Did you check that it really can be removed?

[Kim Morrison]

If so, if there's any chance you could try minimising it a bit it would be good to have a bug report.

[Daniel Weber]

Kim Morrison said:

Hmmmm, that does look suspicious. Did you check that it really can be removed?

Yes, it's in #16382

[Daniel Weber]

Kim Morrison said:

If so, if there's any chance you could try minimising it a bit it would be good to have a bug report.

Alright, I'll try

[Daniel Weber]

Here's a Mathlib-free version, I'll try to minimize it:

section Relation

variable {α : Sort u} {β : Sort v} (r : β → β → Prop)

local infix:50 " ≺ " => r

/-- A relation is symmetric if `x ≺ y` implies `y ≺ x`. -/
def Symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x

/-- Irreflexive means "not reflexive". -/
def Irreflexive := ∀ x, ¬ x ≺ x

end Relation

structure SimpleGraph (V : Type u) where
  /-- The adjacency relation of a simple graph. -/
  Adj : V → V → Prop
  symm : Symmetric Adj
  loopless : Irreflexive Adj

universe u v w

variable {V : Type u} {V' : Type v} {V'' : Type w}
variable (G : SimpleGraph V)

namespace SimpleGraph

inductive Walk : V → V → Type u
  | nil {u : V} : Walk u u
  | cons {u v w : V} (h : G.Adj u v) (p : Walk v w) : Walk u w
  deriving DecidableEq

namespace Walk

variable {G}

inductive Nil : {v w : V} → G.Walk v w → Prop
  | nil {u : V} : Nil (nil : G.Walk u u)

def getVert {u v : V} : G.Walk u v → Nat → V
  | nil, _ => u
  | cons _ q, 0 => u
  | cons _ q, n + 1 => q.getVert n

protected def copy {u v u' v'} (p : G.Walk u v) (hu : u = u') (hv : v = v') : G.Walk u' v' :=
  hu ▸ hv ▸ p

@[simp]
theorem getVert_zero {u v} (w : G.Walk u v) : w.getVert 0 = u := by cases w <;> rfl

/-- The walk obtained by removing the first `n` darts of a walk. -/
def drop {u v : V} (p : G.Walk u v) (n : Nat) : G.Walk (p.getVert n) v :=
  match p, n with
  | .nil, _ => .nil
  | p, 0 => p.copy (getVert_zero p).symm rfl
  | .cons _ q, (n + 1) => q.drop n

/-- The walk obtained by removing the first dart of a walk. A nil walk stays nil. -/
def tail (p : G.Walk u v) : G.Walk (p.getVert 1) v := p.drop 1

@[simp]
theorem getVert_cons_succ {u v w n} (p : G.Walk v w) (h : G.Adj u v) :
    (p.cons h).getVert (n + 1) = p.getVert n := rfl

theorem tail_cons_eq (h : G.Adj u v) (p : G.Walk v w) :
    (p.cons h).tail = p.copy (getVert_zero p).symm rfl := sorry

theorem getVert_cons {u v w n} (p : G.Walk v w) (h : G.Adj u v) (hn : n ≠ 0) :
    (p.cons h).getVert n = p.getVert (n - 1) := sorry

theorem getVert_copy  {u v w x : V} (p : G.Walk u v) (i : Nat) (h : u = w) (h' : v = x) :
    (p.copy h h').getVert i = p.getVert i := sorry


@[simp] theorem getVert_tail {u v n} (p : G.Walk u v) (hnp: ¬ p.Nil) (test : Nat) :
    p.tail.getVert n = p.getVert (n + 1) := by
  match p with
  | .nil => rfl
  | .cons h q =>
    simp only [getVert_cons_succ, tail_cons_eq, getVert_cons]
    exact getVert_copy q n (getVert_zero q).symm rfl

end Walk
end SimpleGraph

[Kim Morrison]

@Daniel Weber, thanks, even that would be good to report as an issue on the lean4 repository.