leanprover-community/batteries

False positive from the unusedHavesSuffices linter

kim-em opened this issue · 5 comments

kim-em commented 
import Std

/---/
def npowRec {M : Type} [Mul M] (one : M) : Nat → M → M
  | 0, _ => one
  | n + 1, a => a * npowRec one n a

/---/
@[nolint unusedArguments]
abbrev npowRec' {M : Type} [Mul M] (one : M) (_mul_one : ∀ m : M, m * one = m) (_one_mul : ∀ m : M, one * m = m) (k : Nat) (m : M) : M :=
  npowRec one k m

@[nolint unusedArguments]
theorem npowRec'_two_mul {M : Type} [Mul M] (one : M)
    (mul_one : ∀ m : M, m * one = m) (one_mul : ∀ m : M, one * m = m) (k : Nat) (m : M) :
    npowRec' one mul_one one_mul (2 * k) m = npowRec' one mul_one one_mul k (m * m) := sorry

/---/
@[nolint unusedArguments]
def npowBinRec {M : Type} [Mul M] (one : M) (_unused : one * one = one) (_unused' : one * one = one) (k : Nat) (m : M) : M :=
  go k one m
where
  /-- Auxiliary tail-recursive implementation for `npowBinRec`-/
  go : Nat → M → M → M
  | 0, y, _ => y
  | (k + 1), y, x =>
    let k' := (k + 1) >>> 1
    if k &&& 1 = 1 then
      have : k' < k + 1 := Nat.div_lt_self (Nat.zero_lt_succ _) (Nat.lt_succ_self _)
      go k' y (x * x)
    else
      have : k' < k + 1 := Nat.div_lt_self (Nat.zero_lt_succ _) (Nat.lt_succ_self _)
      go k' (y * x) (x * x)
  termination_by go k _ _ => k

theorem npowBinRec.go_spec {M : Type} [Mul M] (one : M) (mul_one : ∀ m : M, m * one = m) (one_mul : ∀ m : M, one * m = m) (k : Nat) (x y : M) :
    npowBinRec.go k y x = y * npowRec' one mul_one one_mul k x := by
  induction k using Nat.strongInductionOn generalizing x y with
  | ind k' ih =>
    cases k' with
    | zero => sorry
    | succ k' =>
      rw [go]
      sorry

#lint

Somehow when we rw [go], the unusedHavesSuffices linter can see the have statements from inside the go, and doesn't like them. This is from leanprover-community/mathlib4#8885

kmill commented

For anyone like me passing through, wondering what the linter is seeing, the issue is that once rw [go] applies, the body of the definition go is part of the proof term because the type is captured by the sorry term. Similarly, if you do dsimp first before sorry, while it does erase the offending let_fun statements, the let_funs are still captured in an id term that dsimp produces.

I might be inclined to say that this should be upgraded to a core issue. Maybe equation lemmas should erase unused let_funs?

digama0 commented

I might be inclined to say that this should be upgraded to a core issue. Maybe equation lemmas should erase unused let_funs?

Yes please! The problem is that the type of the equation lemma itself violates the linter, although it may or may not have actually been generated in the given file, and theorems that use the lemma will also end up violating the linter because the type of the equation lemma shows up in various places during rewriting.

semorrison commented

Upgrading to a core issue would require further minimizing the example. If anyone has the time and inclination to do so, that would be much appreciated. Either posting a smaller example here, or just directly opening a new issue on core would work!

llllvvuu commented

The unusedHavesSuffices linter was sometimes not going off due to leanprover/lean4#4375, which has now been fixed. Now we can see this issue more easily in nightly-testing:

import Batteries.Tactic.Lint.Misc
import Batteries.Tactic.Lint.Frontend

def Nat.log (b : Nat) : Nat → Nat
  | n =>
    if h : b ≤ n ∧ 1 < b then
      have : n / b < n := div_lt_self (by omega) (by omega)
      log b (n / b) + 1
    else 0

#print Nat.log
#print Nat.log.eq_1

theorem Nat.log_eq_zero_iff {b n : Nat} : log b n = log b n := by
  rw [log]

#lint only unusedHavesSuffices