From f78aa30bd9ac97bdf66759f3cf7d34bf90980ece Mon Sep 17 00:00:00 2001 From: L Date: Wed, 12 Jun 2024 06:57:05 +0000 Subject: [PATCH] chore: address unusedHavesSuffices warning (#13754) This linter was silently not doing anything until https://github.com/leanprover/lean4/pull/4410 was fixed, and now it is working so a backlog of warnings needed to be addressed. Some were addressed here: https://github.com/leanprover-community/mathlib4/pull/13680. The warnings in this PRs are false positives (https://github.com/leanprover-community/batteries/issues/428?), but a workaround is put in place. Co-authored-by: L Lllvvuu --- Mathlib/Data/Nat/Log.lean | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/Mathlib/Data/Nat/Log.lean b/Mathlib/Data/Nat/Log.lean index dbe5c2b8191e0..baf6136efc728 100644 --- a/Mathlib/Data/Nat/Log.lean +++ b/Mathlib/Data/Nat/Log.lean @@ -30,11 +30,12 @@ namespace Nat such that `b^k ≤ n`, so if `b^k = n`, it returns exactly `k`. -/ --@[pp_nodot] porting note: unknown attribute def log (b : ℕ) : ℕ → ℕ - | n => - if h : b ≤ n ∧ 1 < b then - have : n / b < n := div_lt_self ((Nat.zero_lt_one.trans h.2).trans_le h.1) h.2 - log b (n / b) + 1 - else 0 + | n => if h : b ≤ n ∧ 1 < b then log b (n / b) + 1 else 0 +decreasing_by + -- putting this in the def triggers the `unusedHavesSuffices` linter: + -- https://github.com/leanprover-community/batteries/issues/428 + have : n / b < n := div_lt_self ((Nat.zero_lt_one.trans h.2).trans_le h.1) h.2 + decreasing_trivial #align nat.log Nat.log @[simp] @@ -238,11 +239,13 @@ theorem add_pred_div_lt {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : (n + b - 1) / `k : ℕ` such that `n ≤ b^k`, so if `b^k = n`, it returns exactly `k`. -/ --@[pp_nodot] def clog (b : ℕ) : ℕ → ℕ - | n => - if h : 1 < b ∧ 1 < n then - have : (n + b - 1) / b < n := add_pred_div_lt h.1 h.2 - clog b ((n + b - 1) / b) + 1 - else 0 + | n => if h : 1 < b ∧ 1 < n then clog b ((n + b - 1) / b) + 1 else 0 +decreasing_by + -- putting this in the def triggers the `unusedHavesSuffices` linter: + -- https://github.com/leanprover-community/batteries/issues/428 + have : (n + b - 1) / b < n := add_pred_div_lt h.1 h.2 + decreasing_trivial + #align nat.clog Nat.clog theorem clog_of_left_le_one {b : ℕ} (hb : b ≤ 1) (n : ℕ) : clog b n = 0 := by