feat: linters to try hammers at every step (#30808)

This PR adds three linters which respectively try running `simp_all`, `aesop`, and `grind` at each step in Mathlib. The intention is not to look at individual outputs and make replacements, but rather to use these as baselines for premise selection algorithm comparisons.

In leanprover/lean4#10920 I'm adding `grind +premises` (and I'd like to do the same with `simp_all` and `aesop`), and we can then measure how different premise selection algorithms compare at library scale.

Author: kim-em

Mathlib/Tactic/Core.lean

@@ -74,7 +74,7 @@ def MVarId.introsWithBinderIdents
     (g : MVarId) (ids : List (TSyntax ``binderIdent)) (maxIntros? : Option Nat := none) :
     MetaM (List (TSyntax ``binderIdent) × Array FVarId × MVarId) := do
   let type ← g.getType
-  let type ← instantiateMVars type
+  let type ← Lean.instantiateMVars type
   let n := getIntrosSize type
   let n := match maxIntros? with | none => n | some maxIntros => min n maxIntros
   if n == 0 then

Mathlib/Tactic/TacticAnalysis/Declarations.lean

@@ -265,6 +265,59 @@ def terminalToGrind : TacticAnalysis.Config where
       if oldHeartbeats * 2 < newHeartbeats then
         logWarningAt stx m!"'grind' is slower than the original: {oldHeartbeats} -> {newHeartbeats}"
 
+open Elab.Command in
+/-- Run a tactic at each proof step. -/
+def tryAtEachStep (tac : Syntax → MVarId → CommandElabM (TSyntax `tactic)) : TacticAnalysis.Config where
+  run seq := do
+    for (ctx, i) in seq do
+      if let [goal] := i.goalsBefore then
+        let tac ← tac i.stx goal
+        let goalsAfter ← try
+          ctx.runTacticCode i goal tac
+        catch _e =>
+          pure [goal]
+        if goalsAfter.isEmpty then
+          logInfoAt i.stx m!"`{i.stx}` can be replaced with `{tac}`"
+
+/-- Run `grind` at every step in proofs, reporting where it succeeds. -/
+register_option linter.tacticAnalysis.tryAtEachStepGrind : Bool := {
+  defValue := false
+}
+
+@[tacticAnalysis linter.tacticAnalysis.tryAtEachStepGrind,
+   inherit_doc linter.tacticAnalysis.tryAtEachStepGrind]
+def tryAtEachStepGrind := tryAtEachStep (fun _ _ => `(tactic| grind))
+
+/-- Run `simp_all` at every step in proofs, reporting where it succeeds. -/
+register_option linter.tacticAnalysis.tryAtEachStepSimpAll : Bool := {
+  defValue := false
+}
+
+@[tacticAnalysis linter.tacticAnalysis.tryAtEachStepSimpAll,
+   inherit_doc linter.tacticAnalysis.tryAtEachStepSimpAll]
+def tryAtEachStepSimpAll := tryAtEachStep (fun _ _ => `(tactic| simp_all))
+
+/-- Run `aesop` at every step in proofs, reporting where it succeeds. -/
+register_option linter.tacticAnalysis.tryAtEachStepAesop : Bool := {
+  defValue := false
+}
+
+@[tacticAnalysis linter.tacticAnalysis.tryAtEachStepAesop,
+   inherit_doc linter.tacticAnalysis.tryAtEachStepAesop]
+def tryAtEachStepAesop := tryAtEachStep
+  -- As `aesop` isn't imported here, we construct the tactic syntax manually.
+  fun _ _ => return ⟨TSyntax.raw <|
+    mkNode `Aesop.Frontend.Parser.aesopTactic #[mkAtom "aesop", mkNullNode]⟩
+
+/-- Run `grind +premises` at every step in proofs, reporting where it succeeds. -/
+register_option linter.tacticAnalysis.tryAtEachStepGrindPremises : Bool := {
+  defValue := false
+}
+
+@[tacticAnalysis linter.tacticAnalysis.tryAtEachStepGrindPremises,
+   inherit_doc linter.tacticAnalysis.tryAtEachStepGrindPremises]
+def tryAtEachStepGrindPremises := tryAtEachStep (fun _ _ => `(tactic| grind +premises))
+
 -- TODO: add compatibility with `rintro` and `intros`
 /-- Suggest merging two adjacent `intro` tactics which don't pattern match. -/
 register_option linter.tacticAnalysis.introMerge : Bool := {

MathlibTest/TacticAnalysis.lean

@@ -1,5 +1,6 @@
 import Mathlib.Tactic.TacticAnalysis.Declarations
 import Mathlib.Tactic.AdaptationNote
+import Lean.PremiseSelection
 
 section terminalReplacement
 
@@ -138,3 +139,53 @@ example : ∀ a b : Unit, a = b := by
   rfl
 
 end introMerge
+
+section tryAtEachStep
+
+section
+set_option linter.tacticAnalysis.tryAtEachStepGrind true
+
+/-- info: `rfl` can be replaced with `grind` -/
+#guard_msgs in
+example : 1 + 1 = 2 := by
+  rfl
+
+/--
+info: `skip` can be replaced with `grind`
+---
+info: `rfl` can be replaced with `grind`
+---
+warning: 'skip' tactic does nothing
+
+Note: This linter can be disabled with `set_option linter.unusedTactic false`
+-/
+#guard_msgs in
+example : 1 + 1 = 2 := by
+  skip
+  rfl
+
+end
+
+section
+
+def P (_ : Nat) := True
+theorem p : P 37 := trivial
+
+set_premise_selector fun _ _ => pure #[{ name := `p, score := 1.0 }]
+
+-- FIXME: remove this one `grind +premises` lands.
+macro_rules | `(tactic| grind +premises) => `(tactic| grind [p])
+
+example : P 37 := by
+  grind +premises
+
+set_option linter.tacticAnalysis.tryAtEachStepGrindPremises true
+
+/-- info: `trivial` can be replaced with `grind +premises✝` -/
+#guard_msgs in
+example : P 37 := by
+  trivial
+
+end
+
+end tryAtEachStep

MathlibTest/tryAtEachStep.lean

@@ -0,0 +1,9 @@
+import Mathlib.Tactic.Common
+import Mathlib.Tactic.TacticAnalysis.Declarations
+
+set_option linter.tacticAnalysis.tryAtEachStepAesop true
+
+/-- info: `rfl` can be replaced with `aesop` -/
+#guard_msgs in
+theorem foo : 2 + 2 = 4 := by
+  rfl

scripts/noshake.json

@@ -201,6 +201,7 @@
  ["Batteries.Tactic.Basic",
   "Mathlib.Mathport.Syntax",
   "Mathlib.Tactic.Linter",
+  "Mathlib.Tactic.Common",
   "Mathlib.Init"],
  "ignore":
  {"Mathlib.Util.Notation3": ["Lean.Elab.AuxDef", "Lean.Elab.BuiltinCommand"],