Possible linter.unusedVariables bug

Stream: new members

[Sven Manthe]

I got a wrong positive of linter.unusedVariables; a reduced working example is

import Mathlib
theorem sor {α: Prop} (a: ℕ): α := sorry
structure Game (A: Type*) where
  T: Set (List A)
def Game.residual (G: Game A) {x: List A} (_: x ∈ G.T): Game A where
  T := G.T
noncomputable def sew {G: Game A}
  (_: {a: A} → (h: [a] ∈ G.T) → List (G.residual h).T):
  ℕ := 0
theorem eqPre (G: Game A): ∀_: List A, False := by
  intro x
  let f {a: A} (h: [a] ∈ (G.residual (sor 0)).T):
  List ((Game.residual (Game.residual G (_ : x ∈ G.T)) h).T) := []
  let str := sew f --this line causes "unused variable 'str'", although str is used
  induction' x
  { exact sor str }
  exact sor 0

[Sven Manthe]

Should I maybe post this somewhere else?

[Kevin Buzzard]

Here is fine, let's see if I can drum up some more eyes on your question by observing that changing the line to have str := sew f makes the warning go away even though it's data.

Note that your definition sor is marked as a theorem by you, but its conclusion is not a true-false statement, it's data. If you put #lint at the bottom of your code you'll see this issue is flagged. I suspect that sorrying data (which is what you're doing here) is causing the linter to be confused. If you actually fill in a definition of sor does the problem go away?

[Kevin Buzzard]

If I try to unsorry your data then I get type mismatch errors. I am going to go with "sorrying data confuses the linter" as a response to your question, but perhaps others can be more precise. But don't sorry data anyway :-)

[Sven Manthe]

Oh, I used this universal sorry function only to reduce this to a minimal working example, but I have a much more complicated sorry-free example

[Sven Manthe]

I'll try to produce a minimal working example without sorrying data

[Sven Manthe]

Okay, this was easily fixed and not the issue (see the edit)

[Kevin Buzzard]

I think the linter is complaining that you never use the value of str, just its type. Quite whether it should be complaining is a question for someone else, but again if you change let to have then the code still compiles and the linter stops complaining.

[Sven Manthe]

I don't think this is the case in my nonreduced example (there, changing "let" to "have" leads to a failure of the proof). Although this is probably not really helpful, I'll add the file here, however without the imported ones:

import BorelDet.build_strategies

open Classical
variable {A: Type*} [TopologicalSpace A] [DiscreteTopology A]
variable {T: DTree A} {G: Game A} {p: Player}

def winningPos (G: Game A) (x: List A): Prop :=
  ∃(h: x ∈ G.T)(s: Strategy (G.residual h).T Player.zero), s.winning
theorem winningPos_Iff_exQS (x: List A): winningPos (G:=G) x ↔
  ∃(h: x ∈ G.T)(s: QuasiStrategy (G.residual h).T Player.zero), s.winning := by
  apply exists_congr; intro _; exact existsWinning_Iff_exQuasiWinning

def waitingPre (G: Game A) (p: Player): PreStrategy G.T p where
  toFun {x} _ _ := {a | x++[a] ∈ G.T ∧ ¬winningPos G (x++[a]) }
  valid _ _ _ ha := ha.left
def waitingQuasi (G: Game A) (p: Player) := (waitingPre G p).extQ G.hT

@[simp] theorem QuasiStrategy.castWinning {G G': Game A} (h: G=G') (s: QuasiStrategy G.T p):
  (cast (by rw[h]) s: QuasiStrategy G'.T p).winning ↔ s.winning := by subst h; rfl
theorem waitingQuasi.eqPre {G: Game A} {p: Player}
  (h: ¬∃s: Strategy G.T p.swap, s.winning):
  (waitingQuasi G p).subtree = (waitingPre G p).subtree := by
  apply (waitingPre G p).preIsQuasi; intro x hp hs
  by_contra hc; simp[waitingPre] at hc; push_neg at hc
  have tpeq {a: A} (h: [a] ∈ (G.residual hs.fst).T):
    G.residual h = (G.residual hs.fst).residual h := by simp
  let f {a: A} (h: [a] ∈ (G.residual hs.fst).T) := cast (by rw[tpeq h])
    ((winningPos_Iff_exQS _).mp (hc a h)).snd.choose
  let _str := QuasiStrategy.sew f; have wstr := QuasiStrategy.sew.winning f (fun a h ↦ by --TODO rename back after linter bug is fixed
    dsimp; rw[QuasiStrategy.castWinning (tpeq _)]; apply ((winningPos_Iff_exQS _).mp (hc a h)).snd.choose_spec)
  induction' x using List.reverseRecOn with x b
  { apply h; apply existsWinning_Iff_exQuasiWinning.mpr
    simp at hp; subst hp; use _str }
  induction' x using List.reverseRecOn with x c
  { apply h; apply existsWinning_Iff_exQuasiWinning.mpr
    simp at hp; subst hp; use _str.firstMove;
    rw[QuasiStrategy.firstMove.isWinning]; exact wstr }
  { simp only[position.change, Player.swap_swap] at hp
    have hs' := hs.snd (y:=x) (a:=c) (List.prefix_append _ _) hp; apply hs'.right
    use hs'.left; apply existsWinning_Iff_exQuasiWinning.mpr
    let str': QuasiStrategy ((G.residual (G.T.isTree hs.fst)).residual hs.fst).T Player.one
      := cast (by simp) _str
    use str'.firstMove; rw[QuasiStrategy.firstMove.isWinning]; dsimp
    rw[QuasiStrategy.castWinning (by simp)]; exact wstr }

theorem waitingPre.winsClosed (h: IsClosed G.payoff): (waitingPre G Player.zero).winning := by
  intro a ha; dsimp[Player.payoff]; rw[←(closure_eq_iff_isClosed.mpr h)]
  apply (mem_closure_iff_nhds_basis (isBasis_basic_open a)).mpr

  intro x h
  have ⟨y, b, hsu⟩: ∃y b, a ↾ (2 * (x.length / 2) + 1) = y++[b] := by
    apply ne_nil_has_last; intro h; replace h := congr_arg List.length h; simp at h
  have hpy: position y Player.zero := by
    apply (position.change (a:=b) (p:=Player.one)).mp; rw[←hsu]; simp[position, Nat.even_add_one]
  specialize ha (a ↾ (2 * (x.length / 2) + 1)) (extend_sub _ _)
  rw[hsu] at ha; have ⟨hT, nwin⟩ := (waitingPre G Player.zero).subtree_is_compat hpy ha

  by_contra hfa; simp_rw[not_exists, not_and'] at hfa
  apply nwin; use hT; apply existsWinning_Iff_exQuasiWinning.mpr; use Game.voidStrategy _ Player.zero
  intro a' ha'; specialize hfa (y++[b]++a') (by
    rw[basic_open_iff_restr, basic_open_iff_restr.mp h, ←hsu]
    have hx: x.length ≤ 2 * (x.length / 2) + 1 := by by_cases h: Even x.length <;> simp[h]
    simp[append_restrict (a ↾ (2 * (x.length / 2) + 1)) a' (n:=x.length) (by simp[hx]), hx])
  dsimp[Player.payoff, Game.residual]
  simp only[position, iff_true] at hpy; simp[Nat.even_add_one, hpy]
  simp at ha'; exact ⟨ha', hfa⟩

theorem gale_stewart_prec (h: IsClosed G.payoff) (h': ¬∃s: Strategy G.T Player.one, s.winning):
  (waitingQuasi G Player.zero).winning := by
  dsimp[PreStrategy.winning]; rw[waitingQuasi.eqPre h']; exact waitingPre.winsClosed h
theorem gale_stewart (h: IsClosed G.payoff): determined G := by
  by_cases h': ∃s: Strategy G.T Player.one, s.winning
  exact ⟨Player.one, h'⟩
  exact determined_Iff_quasiDetermined.mpr ⟨Player.zero, _, gale_stewart_prec h h'⟩

[Kevin Buzzard]

yeah there's definitely something beyond my pay grade going on.

[Sven Manthe]

Okay, then I guess I'll wait for a linter expert. Anyways, thank you

[Kevin Buzzard]

A bunch of experts have the new members stream muted because it's mostly beginner questions. Your question is definitely not a beginner question so you could ask again in #std4 , which (I believe) is the repo where the relevant linter is defined.

[Sven Manthe]

For future readers: Reposted as https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/linter.2EunusedVariables.20bug/near/401839285

[Mario Carneiro]

It's not in #std4, it's in core. But also, quoting myself from a similar issue:

In general, issues with unusedVariables linter are usually not actually linter issues but rather the most obvious sign that there is a bug in elaboration and/or the info tree generation, which generate the correct term but with the wrong auxiliary info.

In this case, it's almost certainly a bug in let / have / general elaboration, or induction'

[Mario Carneiro]

minimized:

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

[Scott Morrison]

@Sven Manthe, might you be able to open bug report on the Lean repository, using Mario's minimisation?

[Sven Manthe]

Done (https://github.com/leanprover/lean4/issues/2873)