leanprover · nomeata · Jun 22, 2025 · Jun 16, 2025 · Jun 16, 2025 · Jun 16, 2025
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Simp
 import Lean.Meta.Tactic.Replace
+import Lean.Meta.Hint
 import Lean.Elab.BuiltinNotation
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.ElabTerm
@@ -504,6 +505,79 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
 def traceSimpCall (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Unit := do
   logInfoAt stx[0] m!"Try this: {← mkSimpOnly stx usedSimps}"
 
+
+register_builtin_option linter.unusedSimpArgs : Bool := {
+  defValue := true,
+  descr := "enable the linter that warns when explicit `simp` arguments are unused.\n\
+    \n\
+    The linter suggests removing the unused arguments. This hint may not be correct in the case \
+    that `simp [← thm]` is given, when `thm` has the `@[simp]` attribute, and it is relevant that \
+    `thm` it disabled (which is a side-effect of specifying `← thm`). In that case, replace \
+    it with `simp [- thm]`.\n\
+    \n\
+    When one `simp` invocation is run multiple times (e.g. `all_goals simp [thm]`), it warns \
+    about simp arguments that are unused in all invocations. For this reason, the linter \
+    does not warn about uses of `simp` inside a macro, as there it is usually not possible to see \
+    all invocations."
+}
+
+structure UnusedSimpArgsInfo where
+  mask : Array Bool
+deriving TypeName
+
+def pushUnusedSimpArgsInfo [Monad m] [MonadInfoTree m] (simpStx : Syntax) (mask : Array Bool) : m Unit := do
+  pushInfoLeaf <| .ofCustomInfo {
+    stx := simpStx
+    value := .mk { mask := mask : UnusedSimpArgsInfo } }
+
+/--
+Checks the simp arguments for unused ones, and stores a bitmask of unused ones in the info tree,
+to be picked up by the linter.
+(This indirection is necessary because the same `simp` syntax may be executed multiple times,
+and different simp arguments may be used in each step.)
+-/
+def warnUnusedSimpArgs (simpArgs : Array (Syntax × ElabSimpArgResult)) (usedSimps : Simp.UsedSimps) : MetaM Unit := do
+  if simpArgs.isEmpty then return
+  let mut mask : Array Bool := #[]
+  for h : i in [:simpArgs.size] do
+    let (ref, arg) := simpArgs[i]
+    let used ←
+      match arg with
+      | .addEntries entries =>
+        entries.anyM fun
+          | .thm thm => return usedSimps.contains (← usedThmIdOfSimpTheorem thm)
+          | .toUnfold declName => return usedSimps.contains (.decl declName)
+          | .toUnfoldThms _declName thms => return thms.any (usedSimps.contains <| .decl ·)
+      | .addSimproc declName post =>
+        pure <| usedSimps.contains (.decl declName post)
+      | .addLetToUnfold fvarId =>
+        pure <| usedSimps.contains (.fvar fvarId)
+      | .erase _
+      | .eraseSimproc _
+      | .ext _ _ _
+      | .star
+      | .none
+      => pure true -- not supported yet
+    mask := mask.push used
+  pushUnusedSimpArgsInfo (← getRef) mask
+where
+  /--
+  For equational theorems, usedTheorems record the declaration name. So if the user
+  specified `foo.eq_1`, we get `foo` in `usedTheores`, but we still want to mark
+  `foo.eq_1` as used.
+  (cf. `recordSimpTheorem`)
+  This may lead to unused, explicitly given `foo.eq_1` to not be warned about. Ok for now,
+  eventually `recordSimpTheorem` could record the actual theorem, and the logic for
+  treating `foo.eq_1` as `foo` be moved to `SimpTrace.lean`
+  -/
+  usedThmIdOfSimpTheorem (thm : SimpTheorem) : MetaM Origin := do
+    let thmId := thm.origin
+    if let .decl declName post false := thmId then
+      if let some declName ← isEqnThm? declName then
+        return (Origin.decl declName post false)
+    return thmId
+
+
 /--
 `simpLocation ctx discharge? varIdToLemmaId loc`
 runs the simplifier at locations specified by `loc`,
@@ -545,21 +619,27 @@ def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
   (location)?
 -/
 @[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do withSimpDiagnostics do
-  let { ctx, simprocs, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
+  let { ctx, simprocs, dischargeWrapper, simpArgs } ← mkSimpContext stx (eraseLocal := false)
   let stats ← dischargeWrapper.with fun discharge? =>
     simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
   if tactic.simp.trace.get (← getOptions) then
     traceSimpCall stx stats.usedTheorems
+  else if linter.unusedSimpArgs.get (← getOptions) then
+    withRef stx do
+      warnUnusedSimpArgs simpArgs stats.usedTheorems
   return stats.diag
 
 @[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do withSimpDiagnostics do
-  let { ctx, simprocs, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
+  let { ctx, simprocs, dischargeWrapper := _, simpArgs } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
   let (result?, stats) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
   match result? with
   | none => replaceMainGoal []
   | some mvarId => replaceMainGoal [mvarId]
   if tactic.simp.trace.get (← getOptions) then
     traceSimpCall stx stats.usedTheorems
+  else if linter.unusedSimpArgs.get (← getOptions) then
+    withRef stx do
+      warnUnusedSimpArgs simpArgs stats.usedTheorems
   return stats.diag
 
 def dsimpLocation (ctx : Simp.Context) (simprocs : Simp.SimprocsArray) (loc : Location) : TacticM Unit := do

diff --git a/src/Lean/Linter.lean b/src/Lean/Linter.lean
@@ -13,3 +13,4 @@ import Lean.Linter.MissingDocs
 import Lean.Linter.Omit
 import Lean.Linter.List
 import Lean.Linter.Sets
+import Lean.Linter.UnusedSimpArgs
diff --git a/src/Lean/Linter/UnusedSimpArgs.lean b/src/Lean/Linter/UnusedSimpArgs.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+prelude
+import Lean.Elab.Command
+import Lean.Elab.Tactic.Simp
+import Lean.Linter.Util
+
+namespace Lean.Linter
+
+open Lean Elab Command
+open Lean.Linter (logLint)
+
+private def warnUnused (stx : Syntax) (i : Nat) : CoreM Unit := do
+  let stx : TSyntax `tactic := ⟨stx⟩
+  let simpArgs := Tactic.getSimpParams stx
+  unless i < simpArgs.size do
+    throwError "Index {i} out of bounds for simp arguments of {stx}"
+  let argStx := simpArgs[i]!
+  let msg := m!"This simp argument is unused:{indentD argStx}"
+  let mut otherArgs : Array Syntax := #[]
+  for h : j in [:simpArgs.size] do if j != i then
+    otherArgs := otherArgs.push simpArgs[j]
+  let stx' := Tactic.setSimpParams stx otherArgs
+  let suggestion : Meta.Hint.Suggestion := stx'
+  let suggestion := { suggestion with span? := stx }
+  let hint ← MessageData.hint "Omit it from the simp argument list." #[ suggestion ]
+  logLint Tactic.linter.unusedSimpArgs argStx (msg ++ hint)
+
+def unusedSimpArgs : Linter where
+  run cmdStx := do
+    if !Tactic.linter.unusedSimpArgs.get (← getOptions) then return
+    let some cmdStxRange := cmdStx.getRange?  | return
+
+    let infoTrees := (← get).infoState.trees.toArray
+    let masksMap : IO.Ref (Std.HashMap String.Range (Syntax × Array Bool)) ← IO.mkRef {}
+
+    for tree in infoTrees do
+      tree.visitM' (postNode := fun ci info _ => do
+        match info with
+        | .ofCustomInfo ci =>
+          if let some {mask} := ci.value.get? Tactic.UnusedSimpArgsInfo then
+            -- Only look at info with a range. This also happens to prevent the linter from
+            -- reporting about unused simp arguments inside macro, which we do not want to do
+            -- (we likely cannot see all uses of the macro, so the warning would be incomplete)
+            let some range := info.range? | return
+            let maskAcc ←
+              if let some (_, maskAcc) := (← masksMap.get)[range]? then
+                unless mask.size = maskAcc.size do
+                  throwErrorAt info.stx "Simp argument mask size mismatch}: {maskAcc.size} vs. {mask.size}"
+                pure <| Array.zipWith (· || ·) mask maskAcc
+              else
+                pure mask
+            masksMap.modify fun m => m.insert range (ci.stx, maskAcc)
+        | _ => pure ())
+
+    -- Sort the outputs by position
+    for (_range, tacticStx, mask) in (← masksMap.get).toArray.qsort (·.1.start < ·.1.start) do
+      for i in [:mask.size] do
+        unless mask[i]! do
+          liftCoreM <| warnUnused tacticStx i
+
+builtin_initialize addLinter unusedSimpArgs
@@ -204,6 +204,9 @@ structure UsedSimps where
   size : Nat := 0
   deriving Inhabited
 
+def UsedSimps.contains (s : UsedSimps) (thmId : Origin) : Bool :=
+  s.map.contains thmId
+
 def UsedSimps.insert (s : UsedSimps) (thmId : Origin) : UsedSimp
F438
s :=
   if s.map.contains thmId then
     s

diff --git a/tests/lean/1113.lean b/tests/lean/1113.lean
@@ -10,7 +10,7 @@ theorem t3 {f: Fin (n+1)}:
   foo f = 0 := by
   dsimp only [←Nat.succ_eq_add_one' n] at f -- use `dsimp` to ensure we don't copy `f`
   trace_state
-  simp only [←Nat.succ_eq_add_one' n, foo]
+  simp only [foo]
 
 example {n: Nat} {f: Fin (n+1)}:
   foo f = 0 := by

diff --git a/tests/lean/4452.lean b/tests/lean/4452.lean
@@ -11,6 +11,7 @@ example (h : 1 = b) : a = b := by
   exact h
 
 set_option linter.all true
+set_option linter.unusedSimpArgs false
 
 example (h : 1 = b) : a = b := by
   simp[

diff --git a/tests/lean/4452.lean.expected.out b/tests/lean/4452.lean.expected.out
@@ -1,2 +1,2 @@
-4452.lean:17:4-17:6: warning: `hi` has been deprecated: Don't use `hi`.
-4452.lean:28:4-28:7: warning: `hi'` has been deprecated: Don't use `hi'`, either.
+4452.lean:18:4-18:6: warning: `hi` has been deprecated: Don't use `hi`.
+4452.lean:29:4-29:7: warning: `hi'` has been deprecated: Don't use `hi'`, either.
diff --git a/tests/lean/allFieldForConstants.lean b/tests/lean/allFieldForConstants.lean
@@ -93,9 +93,9 @@ theorem foldl_init (s : Nat) (xs : List String) :  (xs.foldl (init := s) fun sum
 
 theorem listStringLen_append (xs ys : List String) : listStringLen (xs ++ ys) = listStringLen xs + listStringLen ys := by
   simp [listStringLen]
-  induction xs with
+  cases xs with
   | nil => simp
-  | cons x xs ih => simp +arith [foldl_init x.length, foldl_init (_ + _), ih]
+  | cons x xs => simp +arith [foldl_init x.length, foldl_init (_ + _)]
 
 mutual
   theorem listStringLen_flat (f : Foo) : listStringLen (flat f) = textLength f := by

diff --git a/tests/lean/linterUnusedVariables.lean b/tests/lean/linterUnusedVariables.lean
@@ -2,6 +2,7 @@ import Lean
 
 set_option linter.missingDocs false
 set_option linter.all true
+set_option linter.unusedSimpArgs false
 
 def explicitlyUsedVariable (x : Nat) : Nat :=
   x

diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out
@@ -1,71 +1,71 @@
-linterUnusedVariables.lean:16:21-16:22: warning: unused variable `x`
+linterUnusedVariables.lean:17:21-17:22: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:17:6-17:7: warning: unused variable `y`
+linterUnusedVariables.lean:18:6-18:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:22:8-22:9: warning: unused variable `x`
+linterUnusedVariables.lean:23:8-23:9: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:38:5-38:6: warning: unused variable `x`
+linterUnusedVariables.lean:39:5-39:6: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:43:5-43:6: warning: unused variable `x`
+linterUnusedVariables.lean:44:5-44:6: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:46:7-46:8: warning: unused variable `x`
+linterUnusedVariables.lean:47:7-47:8: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:49:8-49:9: warning: unused variable `x`
+linterUnusedVariables.lean:50:8-50:9: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:53:9-53:10: warning: unused variable `z`
+linterUnusedVariables.lean:54:9-54:10: warning: unused variable `z`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:55:11-55:12: warning: unused variable `z`
+linterUnusedVariables.lean:56:11-56:12: warning: unused variable `z`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:60:14-60:15: warning: unused variable `y`
+linterUnusedVariables.lean:61:14-61:15: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:66:20-66:21: warning: unused variable `y`
+linterUnusedVariables.lean:67:20-67:21: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:71:34-71:38: warning: unused variable `inst`
+linterUnusedVariables.lean:72:34-72:38: warning: unused variable `inst`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:112:25-112:26: warning: unused variable `x`
+linterUnusedVariables.lean:113:25-113:26: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:113:6-113:7: warning: unused variable `y`
+linterUnusedVariables.lean:114:6-114:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:119:6-119:7: warning: unused variable `a`
+linterUnusedVariables.lean:120:6-120:7: warning: unused variable `a`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:129:26-129:27: warning: unused variable `z`
+linterUnusedVariables.lean:130:26-130:27: warning: unused variable `z`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:138:9-138:10: warning: unused variable `h`
+linterUnusedVariables.lean:139:9-139:10: warning: unused variable `h`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:152:8-152:9: warning: unused variable `y`
+linterUnusedVariables.lean:153:8-153:9: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:155:20-155:21: warning: unused variable `β`
+linterUnusedVariables.lean:156:20-156:21: warning: unused variable `β`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:156:7-156:8: warning: unused variable `x`
+linterUnusedVariables.lean:157:7-157:8: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:166:6-166:7: warning: unused variable `s`
+linterUnusedVariables.lean:167:6-167:7: warning: unused variable `s`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:190:6-190:7: warning: unused variable `y`
+linterUnusedVariables.lean:191:6-191:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:200:19-200:20: warning: unused variable `x`
+linterUnusedVariables.lean:201:19-201:20: warning: unused variable `x`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:204:6-204:7: warning: unused variable `y`
+linterUnusedVariables.lean:205:6-205:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:209:6-209:7: warning: unused variable `y`
+linterUnusedVariables.lean:210:6-210:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:214:6-214:7: warning: unused variable `y`
+linterUnusedVariables.lean:215:6-215:7: warning: unused variable `y`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:225:32-225:33: warning: unused variable `b`
+linterUnusedVariables.lean:226:32-226:33: warning: unused variable `b`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
-linterUnusedVariables.lean:243:27-243:28: error: don't know how to synthesize placeholder
+linterUnusedVariables.lean:244:27-244:28: error: don't know how to synthesize placeholder
 context:
 a : Nat
 ⊢ Nat
-linterUnusedVariables.lean:244:0-244:7: warning: declaration uses 'sorry'
 linterUnusedVariables.lean:245:0-245:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:246:29-247:7: error: unexpected token 'theorem'; expected '{' or tactic
-linterUnusedVariables.lean:246:27-246:29: error: unsolved goals
+linterUnusedVariables.lean:246:0-246:7: warning: declaration uses 'sorry'
+linterUnusedVariables.lean:247:29-248:7: error: unexpected token 'theorem'; expected '{' or tactic
+linterUnusedVariables.lean:247:27-247:29: error: unsolved goals
 a : Nat
 ⊢ Nat
-linterUnusedVariables.lean:247:33-247:40: error: unsolved goals
+linterUnusedVariables.lean:248:33-248:40: error: unsolved goals
 a : Nat
 ⊢ Nat
-linterUnusedVariables.lean:247:0-247:40: error: type of theorem 'async' is not a proposition
+linterUnusedVariables.lean:248:0-248:40: error: type of theorem 'async' is not a proposition
   Nat → Nat
-linterUnusedVariables.lean:282:41-282:43: warning: unused variable `ha`
+linterUnusedVariables.lean:283:41-283:43: warning: unused variable `ha`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
diff --git a/tests/lean/run/1234.lean b/tests/lean/run/1234.lean
@@ -3,6 +3,7 @@ theorem lt_of_succ_lt          (_: a + 1 < b): a < b := sorry
 theorem succ_pred_eq_of_pos        (_: 0 < v): v - 1 + 1 = v := sorry
 
 set_option trace.Meta.Tactic.simp true
+set_option linter.unusedSimpArgs false
 --set_option trace.Debug.Meta.Tactic.simp true
 
 set_option Elab.async false -- for stable message ordering in #guard_msgs

diff --git a/tests/lean/run/1380.lean b/tests/lean/run/1380.lean
@@ -1,3 +1,5 @@
+set_option linter.unusedSimpArgs false
+
 variable (n v₁ v₂) (hv₁: v₁ < n + 1) (hv₂: v₂ < n + 1)
 
 theorem foo (_: ¬ Fin.mk v₂ hv₂ = Fin.mk v₁ hv₁ ): True := trivial

diff --git a/tests/lean/run/6655.lean b/tests/lean/run/6655.lean
@@ -11,6 +11,8 @@ it would over-report local variables. This comes down to two kinds of issues:
 This file tests that it resets the tracking and filters the list.
 -/
 
+set_option linter.unusedSimpArgs false
+
 /-!
 Example from #6655. This used to suggest `simp only [e, d]`.
 -/

diff --git a/tests/lean/run/binderNameHintSimp.lean b/tests/lean/run/binderNameHintSimp.lean
@@ -1,3 +1,5 @@
+set_option linter.unusedSimpArgs false
+
 /-!
 Checks that `simp` removes the `binderNameHint` in the pre-phase, and does not spend time looking
 at its arguments.

diff --git a/tests/lean/run/cdotAtSimpArg.lean b/tests/lean/run/cdotAtSimpArg.lean
@@ -15,7 +15,7 @@ example (h : y = 0) : x + y = x := by
   simp [(.+.)] -- Expands `HAdd.hAdd
   trace_state
   simp [Add.add]
-  simp [h, Nat.add]
+  simp [h]
   done
 
 /--
@@ -28,7 +28,7 @@ example (h : y = 0) : x + y = x := by
   simp [.+.]
   trace_state
   simp [Add.add]
-  simp [h, Nat.add]
+  simp [h]
   done
 
 /-! Test `binop%` variant `rightact%` as well -/
-Original file line number
+Diff line change
@@ Expand Up / @@ -11,6 +11,7 @@ example (h : 1 = b) : a = b := by @@
       exact h
     set_option linter.all true
+    set_option linter.unusedSimpArgs false
     example (h : 1 = b) : a = b := by
       simp[
@@ Expand Down @@