feat: a non-terminal simp linter

Mathlib.lean

@@ -3593,6 +3593,7 @@ import Mathlib.Tactic.Monotonicity.Attr
 import Mathlib.Tactic.Monotonicity.Basic
 import Mathlib.Tactic.Monotonicity.Lemmas
 import Mathlib.Tactic.MoveAdd
+import Mathlib.Tactic.NonTerminalSimp
 import Mathlib.Tactic.NoncommRing
 import Mathlib.Tactic.Nontriviality
 import Mathlib.Tactic.Nontriviality.Core

Mathlib/Tactic.lean

@@ -110,6 +110,7 @@ import Mathlib.Tactic.Monotonicity.Attr
 import Mathlib.Tactic.Monotonicity.Basic
 import Mathlib.Tactic.Monotonicity.Lemmas
 import Mathlib.Tactic.MoveAdd
+import Mathlib.Tactic.NonTerminalSimp
 import Mathlib.Tactic.NoncommRing
 import Mathlib.Tactic.Nontriviality
 import Mathlib.Tactic.Nontriviality.Core

Mathlib/Tactic/Basic.lean

@@ -8,6 +8,7 @@ import Std
 import Mathlib.Tactic.PPWithUniv
 import Mathlib.Tactic.ExtendDoc
 import Mathlib.Tactic.Lemma
+import Mathlib.Tactic.NonTerminalSimp
 import Mathlib.Tactic.TypeStar
 
 set_option autoImplicit true

Mathlib/Tactic/NonTerminalSimp.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2024 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+import Lean.Elab.Command
+import Lean.Linter.Util
+import Std.Data.Array.Basic
+
+/-!
+#  The non-terminal `simp` linter
+
+The non-terminal `simp` linter makes sure that `simp` is not used as a finishing tactic.
+If you want to use `simp [...]` followed by other tactics, then replace `simp [...]` by
+* a `suffices \"expr after simp\" by simpa` line;
+* the output of `simp? [...]`, so that the final code contains `simp only [...]`;
+* something else that does not involve `simp`!
+
+The linter equates "non-terminal" with "does not strictly decrease the number of goals".
+
+##  Implementation detail
+
+The code in this linter is just a very small modification of the code for the
+`unreachableTactic` linter.
+-/
+
+open Lean Elab
+
+namespace Mathlib.Linter
+
+/-- The non-terminal `simp` linter makes sure that `simp` is not used as a finishing tactic. -/
+register_option linter.nonTerminalSimp : Bool := {
+  defValue := true
+  descr := "enable the 'non-terminal `simp`' linter"
+}
+
+namespace nonTerminalSimp
+
+/-- `onlyOrNotSimp stx` if `stx` is syntax for `simp` *without* `only`, then returns `false` else
+returs `true`. -/
+def onlyOrNotSimp : Syntax → Bool
+  | .node _info `Lean.Parser.Tactic.simp #[_, _, _, only?, _, _] => only?[0].getAtomVal == "only"
+  | _ => true
+
+/-- The monad for collecting `simp`s that are not `simp only`. -/
+abbrev M := StateRefT (HashMap String.Range Syntax) IO
+
+mutual
+/-- Search for `simp`s that
+* are not `simp only` and
+* do not close a goal.
+
+Add such `simp`s to the state. -/
+partial def addNonSimpOnlysList (trees : PersistentArray InfoTree) : M Unit :=
+  trees.forM addNonSimpOnlys
+
+@[inherit_doc addNonSimpOnlysList]
+partial def addNonSimpOnlys : InfoTree → M Unit
+  | .node i c => do
+    if let .ofTacticInfo i := i then
+      let non_terminal_simp? := (! onlyOrNotSimp i.stx) &&
+                                (! i.goalsAfter.length < i.goalsBefore.length)
+      match i.stx.getRange? true, non_terminal_simp? with
+        | some r, true => modify (·.insert r i.stx)
+        | _, _ => pure ()
+    addNonSimpOnlysList c
+  | .context _ t => addNonSimpOnlys t
+  | .hole _ => pure ()
+
+end
+
+/-- Gets the value of the `linter.nonTerminalSimp` option. -/
+def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.nonTerminalSimp o
+
+/-- The main entry point to the unreachable tactic linter. -/
+def nonTerminalSimpLinter : Linter where run := withSetOptionIn fun _stx => do
+  unless getLinterHash (← getOptions) && (← getInfoState).enabled do
+    return
+  if (← get).messages.hasErrors then
+    return
+  let (_, map) ← (addNonSimpOnlysList (← getInfoTrees)).run {}
+  let simps := map.toArray
+  let key (r : String.Range) := (r.start.byteIdx, (-r.stop.byteIdx : Int))
+  let mut last : String.Range := ⟨0, 0⟩
+  for (r, stx) in let _ := @lexOrd; let _ := @ltOfOrd.{0}; simps.qsort (key ·.1 < key ·.1) do
+    if last.start ≤ r.start && r.stop ≤ last.stop then continue
+    Linter.logLint linter.nonTerminalSimp stx
+      "non-terminal simp: consider replacing it with\n\
+        * `suffices \"expr after simp\" by simpa`\n\
+        * the output of `simp?`\n"
+    last := r
+
+initialize addLinter nonTerminalSimpLinter

scripts/noshake.json

@@ -280,7 +280,7 @@
   ["Mathlib.CategoryTheory.Functor.Basic"],
   "Mathlib.Tactic.CategoryTheory.Coherence":
   ["Mathlib.Tactic.CategoryTheory.MonoidalComp"],
-  "Mathlib.Tactic.Basic": ["Std"],
+  "Mathlib.Tactic.Basic": ["Mathlib.Tactic.NonTerminalSimp", "Std"],
   "Mathlib.Tactic.Attr.Register": ["Lean.Meta.Tactic.Simp.SimpTheorems"],
   "Mathlib.Tactic.ArithMult": ["Mathlib.Tactic.ArithMult.Init"],
   "Mathlib.RingTheory.Subsemiring.Order":
@@ -299,9 +299,9 @@
   "Mathlib.Logic.Equiv.Defs": ["Mathlib.Init.Data.Bool.Lemmas"],
   "Mathlib.LinearAlgebra.Matrix.Transvection": ["Mathlib.Data.Matrix.DMatrix"],
   "Mathlib.LinearAlgebra.AffineSpace.Basic": ["Mathlib.Algebra.AddTorsor"],
-  "Mathlib.Lean.Expr.Basic": ["Std.Logic"],
-  "Mathlib.Lean.Expr.ExtraRecognizers": ["Mathlib.Data.Set.Defs"],
   "Mathlib.Lean.Meta": ["Std.Logic"],
+  "Mathlib.Lean.Expr.ExtraRecognizers": ["Mathlib.Data.Set.Defs"],
+  "Mathlib.Lean.Expr.Basic": ["Std.Logic"],
   "Mathlib.Init.Data.Nat.GCD": ["Std.Data.Nat.Gcd"],
   "Mathlib.Init.Data.Int.Basic": ["Std.Data.Int.Order"],
   "Mathlib.Init.Core": ["Std.Classes.Dvd"],
@@ -331,4 +331,4 @@
   "Mathlib.Algebra.Category.Ring.Basic":
   ["Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso"],
   "Mathlib.Algebra.Algebra.Subalgebra.Order":
-  ["Mathlib.Algebra.Module.Submodule.Order"]}}
+  ["Mathlib.Algebra.Module.Submodule.Order"]}}