From 117f73fc8440e759fb04d741fae3c1bc4646a9fe Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sun, 22 Jun 2025 11:10:21 +0200 Subject: [PATCH] feat: linter.unusedSimpArgs (#8901) This PR adds a linter (`linter.unusedSimpArgs`) that complains when a simp argument (`simp [foo]`) is unused. It should do the right thing if the `simp` invocation is run multiple times, e.g. inside `all_goals`. It does not trigger when the `simp` call is inside a macro. The linter message contains a clickable hint to remove the simp argument. I chose to display a separate warning for each unused argument. This means that the user has to click multiple times to remove all of them (and wait for re-elaboration in between). But this just means multiple endorphine kicks, and the main benefit over a single warning that would have to span the whole argument list is that already the squigglies tell the users about unused arguments. This closes #4483. Making Init and Std clean wrt to this linter revealed close to 1000 unused simp args, a pleasant experience for anyone enjoying tidying things: #8905 --- src/Lean/Elab/Tactic/Simp.lean | 84 +++++- src/Lean/Linter.lean | 1 + src/Lean/Linter/UnusedSimpArgs.lean | 65 +++++ src/Lean/Meta/Tactic/Simp/Types.lean | 3 + tests/lean/1113.lean | 2 +- tests/lean/4452.lean | 1 + tests/lean/4452.lean.expected.out | 4 +- tests/lean/allFieldForConstants.lean | 4 +- tests/lean/linterUnusedVariables.lean | 1 + .../linterUnusedVariables.lean.expected.out | 68 ++--- tests/lean/run/1234.lean | 1 + tests/lean/run/1380.lean | 2 + tests/lean/run/6655.lean | 2 + tests/lean/run/binderNameHintSimp.lean | 2 + tests/lean/run/cdotAtSimpArg.lean | 4 +- tests/lean/run/eqnsAtSimp3.lean | 14 +- tests/lean/run/eqnsProjections.lean | 1 + tests/lean/run/simpHigherOrder.lean | 3 +- tests/lean/run/simpUnusedArgs.lean | 274 ++++++++++++++++++ tests/lean/trailingComma.lean | 3 +- tests/lean/trailingComma.lean.expected.out | 4 +- tests/lean/wfrecUnusedLet.lean | 1 - 22 files changed, 488 insertions(+), 56 deletions(-) create mode 100644 src/Lean/Linter/UnusedSimpArgs.lean create mode 100644 tests/lean/run/simpUnusedArgs.lean diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 54483fbb5c..1e9e580305 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -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 index 859e974ce2..30b21aef92 100644 --- 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 new file mode 100644 index 0000000000..fd5cc5943f --- /dev/null +++ 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 diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 042fd0055b..4d7f159ff9 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -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) : UsedSimps := if s.map.contains thmId then s diff --git a/tests/lean/1113.lean b/tests/lean/1113.lean index 44c6b8648c..2d90b3fe49 100644 --- 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 index b2c4986e4a..c3990b6dc4 100644 --- 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 index 8e50ea96d1..774e26a7ed 100644 --- 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 index 6d749b7b08..fff3ca5a37 100644 --- 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 index 1def2ca5f7..016d5b73cb 100644 --- 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 index 5a59655339..5a8b11f813 100644 --- 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 index b4bd842987..59736ea39a 100644 --- 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 index 6858b17d54..bb951fe299 100644 --- 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 index 366bcd3fac..e181d39912 100644 --- 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 index da75cc21b4..37d3020e88 100644 --- 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 index ca157f90be..d936cf3195 100644 --- 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 -/ diff --git a/tests/lean/run/eqnsAtSimp3.lean b/tests/lean/run/eqnsAtSimp3.lean index 49075cb456..e677a3d89e 100644 --- a/tests/lean/run/eqnsAtSimp3.lean +++ b/tests/lean/run/eqnsAtSimp3.lean @@ -12,7 +12,7 @@ h : y ≠ 5 -/ #guard_msgs in theorem ex1 (x : Nat) (y : Nat) (h : y ≠ 5) : ∃ z, f (x+1) y = 2 * z := by - simp [f, h] + simp [f] trace_state apply Exists.intro rfl @@ -31,7 +31,7 @@ h : y ≠ 5 -/ #guard_msgs in theorem ex2 (x : Nat) (y : Nat) (h : y ≠ 5) : ∃ z, g (x+1) y = 2 * z := by - simp [h] + simp trace_state apply Exists.intro rfl @@ -43,7 +43,7 @@ h : y = 5 → False -/ #guard_msgs in theorem ex3 (x : Nat) (y : Nat) (h : y = 5 → False) : ∃ z, f (x+1) y = 2 * z := by - simp [f, h] + simp [f] trace_state apply Exists.intro rfl @@ -51,7 +51,7 @@ theorem ex3 (x : Nat) (y : Nat) (h : y = 5 → False) : ∃ z, f (x+1) y = 2 * z @[simp] def f2 (x y z : Nat) : Nat := match x, y, z with | 0, 0, 0 => 1 - | 0, y, z => y + | 0, y, _ => y | x+1, 5, 6 => 2 * f2 x 0 1 | x+1, y, z => 2 * f2 x y z @@ -65,7 +65,7 @@ h : y = 5 → z = 6 → False -/ #guard_msgs in theorem ex4 (x y z : Nat) (h : y = 5 → z = 6 → False) : ∃ w, f2 (x+1) y z = 2 * w := by - simp [f2, h] + simp [f2] trace_state apply Exists.intro rfl @@ -83,7 +83,7 @@ theorem ex6 (x y z : Nat) (h2 : z ≠ 6) : ∃ w, f2 (x+1) y z = 2 * w := by @[simp] def f3 (x y z : Nat) : Nat := match x, y, z with | 0, 0, 0 => 1 - | 0, y, z => y + | 0, y, _ => y | x+1, 5, 6 => 4 * f3 x 0 1 | x+1, 6, 4 => 3 * f3 x 0 1 | x+1, y, z => 2 * f3 x y z @@ -96,6 +96,6 @@ theorem ex7 (x y z : Nat) (h2 : z ≠ 6) (h3 : y ≠ 6) : ∃ w, f3 (x+1) y z = rfl theorem ex8 (x y z : Nat) (h2 : y = 5 → z = 6 → False) (h3 : y = 6 → z = 4 → False) : ∃ w, f3 (x+1) y z = 2 * w := by - simp [f3, h2, h3] + simp [f3] apply Exists.intro rfl diff --git a/tests/lean/run/eqnsProjections.lean b/tests/lean/run/eqnsProjections.lean index 0493d07b7e..c45d61dc04 100644 --- a/tests/lean/run/eqnsProjections.lean +++ b/tests/lean/run/eqnsProjections.lean @@ -76,6 +76,7 @@ n : Nat ⊢ P n -/ #guard_msgs in +set_option linter.unusedSimpArgs false in example : P (S.proj ⟨n⟩) := by simp [S.proj]; fail -- NB: reduces the projectino end structure_concrete diff --git a/tests/lean/run/simpHigherOrder.lean b/tests/lean/run/simpHigherOrder.lean index 7ced4facac..f3f46b9bbb 100644 --- a/tests/lean/run/simpHigherOrder.lean +++ b/tests/lean/run/simpHigherOrder.lean @@ -33,6 +33,7 @@ l : List Nat ⊢ List.foldr (fun x a => a + x * x) 0 l = (List.map (fun x => x * x) l).sum -/ #guard_msgs in +set_option linter.unusedSimpArgs false in example (l : List Nat) : l.foldr (fun x a => a + x*x) 0 = List.sum (l.map (fun x => x * x)) := by simp [foldr_to_sum] @@ -61,5 +62,5 @@ theorem zipWith_ignores_right · simp [List.zipWith, h, ih] example (l₁ l₂ : List Nat) (hlen: l₁.length = l₂.length): - List.zipWith (fun x y => x*x) l₁ l₂ = l₁.map (fun x => x * x) := by + List.zipWith (fun x _ => x*x) l₁ l₂ = l₁.map (fun x => x * x) := by simp only [zipWith_ignores_right, hlen.symm, List.take_length] diff --git a/tests/lean/run/simpUnusedArgs.lean b/tests/lean/run/simpUnusedArgs.lean new file mode 100644 index 0000000000..8616d55858 --- /dev/null +++ b/tests/lean/run/simpUnusedArgs.lean @@ -0,0 +1,274 @@ +set_option linter.unusedVariables false + +set_option linter.unusedSimpArgs true + +def some_def := 1 +def some_rdef : Nat → Nat + | 0 => 42 + | n + 1 => some_rdef n + +/-- +warning: This simp argument is unused: + id_eq + +Hint: Omit it from the simp argument list. + simp ̵[̵i̵d̵_̵e̵q̵]̵ +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in +example : True := by simp [id_eq] + +/-- +warning: This simp argument is unused: + id_eq + +Hint: Omit it from the simp argument list. + simp [i̵d̵_̵e̵q̵,̵ ̵and_self] +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in +example : True ∧ True := by simp [id_eq, and_self] + + +#guard_msgs in example : id True := by simp [id_eq] + +/-- +warning: This simp argument is unused: + some_def + +Hint: Omit it from the simp argument list. + simp ̵[̵s̵o̵m̵e̵_̵d̵e̵f̵]̵ +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in example : True := by simp [some_def] + +#guard_msgs in example : 0 < some_def := by simp [some_def] + + +-- Duplicate are not warned about (yet) +#guard_msgs in example : 0 < some_def := by simp [some_def, some_def] + +-- The diffing algorithm can be somewhat confusing if a simp argument is repeated: + +/-- +warning: This simp argument is unused: + some_def.eq_def + +Hint: Omit it from the simp argument list. + simp [some_def, some_def.eq_def,̵ ̵s̵o̵m̵e̵_̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵] +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +--- +warning: This simp argument is unused: + some_def.eq_def + +Hint: Omit it from the simp argument list. + simp [some_def, some_def.eq_def,̵ ̵s̵o̵m̵e̵_̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵] +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in example : 0 < some_def := by simp [some_def, some_def.eq_def, some_def.eq_def] + +/-- +warning: This simp argument is unused: + (some_def.eq_def) + +Hint: Omit it from the simp argument list. + simp [some_def, (̵some_def.eq_def)̵,̵ ̵s̵o̵m̵e̵_̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵] +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +--- +warning: This simp argument is unused: + some_def.eq_def + +Hint: Omit it from the simp argument list. + simp [some_def, (some_def.eq_def),̵ ̵s̵o̵m̵e̵_̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵] +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in example : 0 < some_def := by simp [some_def, (some_def.eq_def), some_def.eq_def] + +#guard_msgs in example : 0 < some_def := by simp [some_def.eq_def] + +#guard_msgs in example : 0 < some_rdef 10 := by simp [some_rdef] + +/-- error: simp made no progress -/ +#guard_msgs in example : 0 < some_def := by simp [some_rdef] + +/-- +error: unsolved goals +⊢ 0 < some_def +--- +warning: This simp argument is unused: + some_rdef + +Hint: Omit it from the simp argument list. + simp -failIfUnchanged ̵[̵s̵o̵m̵e̵_̵r̵d̵e̵f̵]̵ +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in example : 0 < some_def := by simp -failIfUnchanged [some_rdef] + +#guard_msgs in example : 0 < some_rdef 10 := by simp -failIfUnchanged [some_rdef] + +#guard_msgs in example : 0 < some_rdef 10 := by simp -failIfUnchanged [some_rdef.eq_def] + +/-- +warning: This simp argument is unused: + some_rdef.eq_def + +Hint: Omit it from the simp argument list. + simp -failIfUnchanged [some_rdef,̵ ̵s̵o̵m̵e̵_̵r̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵] +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in example : 0 < some_rdef 10 := by simp -failIfUnchanged [some_rdef, some_rdef.eq_def] + +#guard_msgs in example : 0 < some_rdef 10 := by simp -failIfUnchanged [some_rdef, some_rdef.eq_1] + +#guard_msgs in example : 0 < some_rdef 10 := by simp -failIfUnchanged [some_rdef.eq_1, some_rdef.eq_2] + +-- This could complain about some_rdef.eq_2, but does not yet: + +#guard_msgs in example : 0 < some_rdef 0 := by simp -failIfUnchanged [some_rdef.eq_1, some_rdef.eq_2] + +/-- +error: unsolved goals +⊢ 0 < some_rdef 10 +-/ +#guard_msgs in example : 0 < some_rdef 10 := by simp -failIfUnchanged + + + +/-- +error: unsolved goals +a : Nat +h : a = 1 +⊢ 0 < a +-/ +#guard_msgs in example (a : Nat) (h : a = 1) : 0 < a := by simp -failIfUnchanged + +#guard_msgs in example (a : Nat) (h : a = 1) : 0 < a := by simp -failIfUnchanged [h] + +-- Local hyps + +/-- +warning: This simp argument is unused: + _h + +Hint: Omit it from the simp argument list. + simp -failIfUnchanged ̵[̵_̵h̵]̵ +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in example (a : Nat) (_h : a = 1) : True := by simp -failIfUnchanged [_h] + +#guard_msgs in example (a : Nat) (_h : a = 1) : True := by simp -failIfUnchanged [*] + + +-- Simprocs + +#guard_msgs in example : if true then True else False := by simp only [↓reduceIte] + +/-- +warning: This simp argument is unused: + ↓reduceIte + +Hint: Omit it from the simp argument list. + simp only [↓reduceI̵t̵e̵,̵ ̵↓̵r̵e̵d̵u̵c̵e̵DIte] +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in example : if _ : true then True else False := by simp only [↓reduceIte, ↓reduceDIte] + +-- Lets + +/-- +error: unsolved goals +x : Nat := 1 +⊢ 0 < x +-/ +#guard_msgs in example : let x := 1; x > 0 := by intro x; simp + +#guard_msgs in example : let x := 1; x > 0 := by intro x; simp [x] + +#guard_msgs in example : let x := 1; True ∨ x > 0:= by intro x; simp [x] + +/-- +warning: This simp argument is unused: + x + +Hint: Omit it from the simp argument list. + simp ̵[̵x̵]̵ +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in example : let x := 1; True ∨ x > 0:= by intro x; left; simp [x] + + +-- Now the tests for multiple branches + +/-- +warning: This simp argument is unused: + h3 + +Hint: Omit it from the simp argument list. + simp [h1, h2,̵ ̵h̵3̵] +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in +example (h1 : P) (h2 : Q) (h3 : R) : P ∧ (Q ∨ R) := by + constructor <;> ((try left); simp [h1, h2, h3]) + +/-- +warning: This simp argument is unused: + h2 + +Hint: Omit it from the simp argument list. + simp [h1,̵ ̵h̵2̵] +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +--- +warning: This simp argument is unused: + h1 + +Hint: Omit it from the simp argument list. + simp [h1̵,̵ ̵h̵2] +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in +example (h1 : P) (h2 : Q) : P ∧ Q := by + constructor + · simp [h1, h2] + · simp [h1, h2] + +-- Inside a macro? + +macro "mySimp" h:term : tactic => `(tactic| simp [$h:term, id_eq]) +macro tk:"mySimp'" h:term : tactic => `(tactic| simp%$tk [$h:term, id_eq]) + +/-- +warning: This simp argument is unused: + h + +Hint: Omit it from the simp argument list. + simp ̵[̵h̵]̵ +note: this linter can be disabled with `set_option linter.unusedSimpArgs false` +-/ +#guard_msgs in +example {P : Prop} (h : P) : True ∧ True := by constructor <;> simp [h] + +example {P : Prop} (h : P) : True ∧ True := by constructor <;> mySimp h + +example {P : Prop} (h : P) : True ∧ True := by constructor <;> mySimp' h + + +-- Check option setting + +section +set_option linter.unusedSimpArgs true + +#guard_msgs in +set_option linter.unusedSimpArgs false in +example : True := by + simp [not_false_eq_true] +end + +section +set_option linter.unusedSimpArgs true + +#guard_msgs in +example : True := by + set_option linter.unusedSimpArgs false in + simp [not_false_eq_true] +end diff --git a/tests/lean/trailingComma.lean b/tests/lean/trailingComma.lean index 380b244eed..b29f59b969 100644 --- a/tests/lean/trailingComma.lean +++ b/tests/lean/trailingComma.lean @@ -1,5 +1,4 @@ -import Lean -open Lean +set_option linter.unusedSimpArgs false #eval [1,2,3,] #eval (2,3,) diff --git a/tests/lean/trailingComma.lean.expected.out b/tests/lean/trailingComma.lean.expected.out index 99655e8904..e549798e7d 100644 --- a/tests/lean/trailingComma.lean.expected.out +++ b/tests/lean/trailingComma.lean.expected.out @@ -1,4 +1,4 @@ [1, 2, 3] (2, 3) -trailingComma.lean:6:13-6:14: error: unexpected token ','; expected ']' -trailingComma.lean:7:11-7:12: error: unexpected token ','; expected ')' +trailingComma.lean:5:13-5:14: error: unexpected token ','; expected ']' +trailingComma.lean:6:11-6:12: error: unexpected token ','; expected ')' diff --git a/tests/lean/wfrecUnusedLet.lean b/tests/lean/wfrecUnusedLet.lean index 0108141e46..ec42eca57b 100644 --- a/tests/lean/wfrecUnusedLet.lean +++ b/tests/lean/wfrecUnusedLet.lean @@ -5,7 +5,6 @@ def f (n : Nat) : Nat := let y := 42 2 * f (n-1) decreasing_by - simp [measure, id, invImage, InvImage, Nat.lt_wfRel, WellFoundedRelation.rel] apply Nat.pred_lt h #print f