feat: unused tactic linter (#11308)

The `unusedTactic` linter emits a warning if a tactic does nothing.

Previous PRs (see below) removed all the "unused tactics" that the linter flagged.

Here is an overview of this PR:
* the linter is defined in `Mathlib/Tactic/Linter/UnusedTactic.lean`;
* the file `Mathlib/GroupTheory/Perm/Cycle/Concrete.lean` contains the "only" `set_option` to opt out of the linter, since it defines notation that uses `decide` that the notation itself does not use;
* 17 test files that have surgically opted out of the linter;
* noise to import the new file, place it low in the import hierarchy and update `noshake`.


PRs removing some unused tactics:
* #11333
* #11351
* #11365
* #11379

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/pointless.20tactic.20linter)

Mathlib.lean

@@ -3935,6 +3935,7 @@ import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.Linter.OldObtain
 import Mathlib.Tactic.Linter.Style
 import Mathlib.Tactic.Linter.TextBased
+import Mathlib.Tactic.Linter.UnusedTactic
 import Mathlib.Tactic.Measurability
 import Mathlib.Tactic.Measurability.Init
 import Mathlib.Tactic.MkIffOfInductiveProp

Mathlib/AlgebraicGeometry/Restrict.lean

@@ -346,8 +346,8 @@ theorem morphismRestrict_app {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Opens Y) (V :
   simp only [comp_coeBase, Opens.map_comp_obj, restrict_presheaf_obj,
     Hom.app_eq_appLE, comp_appLE, ofRestrict_appLE, Hom.appLE_map, eqToHom_op,
     restrict_presheaf_map, eqToHom_unop] at this
-  have e : ιOpens U ⁻¹ᵁ (ιOpens U ''ᵁ V) = V := by
-    exact Opens.ext (Set.preimage_image_eq _ Subtype.coe_injective)
+  have e : ιOpens U ⁻¹ᵁ (ιOpens U ''ᵁ V) = V :=
+    Opens.ext (Set.preimage_image_eq _ Subtype.coe_injective)
   have e' : (f ∣_ U) ⁻¹ᵁ V = (f ∣_ U) ⁻¹ᵁ ιOpens U ⁻¹ᵁ ιOpens U ''ᵁ V := by rw [e]
   rw [← (f ∣_ U).appLE_map' _ e', ← (f ∣_ U).map_appLE' _ e, Scheme.restrict_presheaf_map,
     Scheme.restrict_presheaf_map, this, Hom.appLE_map]

Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

@@ -195,8 +195,7 @@ theorem T_insert_le_T_lmarginal_singleton (hp₀ : 0 ≤ p) (s : Finset ι)
           ∏ j in s, (∫⋯∫⁻_{j}, (∫⋯∫⁻_{i}, f ∂μ) ∂μ) x ^ p := by
               -- identify the result with the RHS integrand
               congr! 2 with j hj
-              · push_cast
-                ring_nf
+              · ring_nf
               · congr! 1
                 rw [← lmarginal_union μ f hf]
                 · congr

Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

@@ -525,6 +525,8 @@ def isoCycle' : { f : Perm α // IsCycle f } ≃ { s : Cycle α // s.Nodup ∧ s
     right_inv := Fintype.leftInverse_bijInv _ }
 #align equiv.perm.iso_cycle' Equiv.Perm.isoCycle'
 
+-- mutes `'decide' tactic does nothing [linter.unusedTactic]`
+set_option linter.unusedTactic false in
 notation3 (prettyPrint := false) "c["(l", "* => foldr (h t => List.cons h t) List.nil)"]" =>
   Cycle.formPerm (Cycle.ofList l) (Iff.mpr Cycle.nodup_coe_iff (by decide))
 

Mathlib/SetTheory/Surreal/Multiplication.lean

@@ -133,7 +133,6 @@ lemma mulOption_lt_iff_P1 {i j k l} :
     (⟦mulOption x y i k⟧ : Game) < -⟦mulOption x (-y) j l⟧ ↔
     P1 (x.moveLeft i) x (x.moveLeft j) y (y.moveLeft k) (-(-y).moveLeft l) := by
   dsimp only [P1, mulOption, quot_sub, quot_add]
-  congr
   simp_rw [neg_sub', neg_add, quot_mul_neg, neg_neg]
 
 lemma mulOption_lt_mul_iff_P3 {i j} :

Mathlib/Tactic.lean

@@ -119,6 +119,7 @@ import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.Linter.OldObtain
 import Mathlib.Tactic.Linter.Style
 import Mathlib.Tactic.Linter.TextBased
+import Mathlib.Tactic.Linter.UnusedTactic
 import Mathlib.Tactic.Measurability
 import Mathlib.Tactic.Measurability.Init
 import Mathlib.Tactic.MkIffOfInductiveProp

Mathlib/Tactic/Linter.lean

@@ -11,3 +11,4 @@ import Mathlib.Tactic.Linter.GlobalAttributeIn
 import Mathlib.Tactic.Linter.HashCommandLinter
 import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.Linter.Style
+import Mathlib.Tactic.Linter.UnusedTactic

Mathlib/Tactic/Linter/UnusedTactic.lean

@@ -0,0 +1,213 @@
+/-
+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 Batteries.Data.List.Basic
+import Batteries.Tactic.Unreachable
+
+/-!
+#  The unused tactic linter
+
+The unused linter makes sure that every tactic call actually changes *something*.
+
+The inner workings of the linter are as follows.
+
+The linter inspects the goals before and after each tactic execution.
+If they are not identical, the linter is happy.
+If they are identical, then the linter checks if the tactic is whitelisted.
+Possible reason for whitelisting are
+* tactics that emit messages, such as `have?`, `extract_goal`, or `says`;
+* tactics that are in place to assert something, such as `guard`;
+* tactics that allow to work on a specific goal, such as `on_goal`;
+* "flow control" tactics, such as `success_if_fail` and related.
+
+The only tactic that has a bespoke criterion is `swap_var`: the reason is that the only change that
+`swap_var` has is to relabel the usernames of local declarations.
+Thus, to check that `swap_var` was used, so we inspect the names of all the local declarations
+before and after and see if there is some change.
+
+###  Notable exclusions
+
+* `conv` is completely ignored by the linter.
+
+* The linter does not enter a "sequence tactic": upon finding `tac <;> [tac1, tac2, ...]`
+  the linter assumes that the tactic is doing something and does not recurse into each
+  `tac1, tac2, ...`.
+  This is just for lack of an implementation: it may not be hard to do this.
+
+* The tactic does not check the discharger for `linear_combination`,
+  but checks `linear_combination` itself.
+  The main reason is that `skip` is a common discharger tactic and the linter would
+  then always fail whenever the user explicitly chose to pass `skip` as a discharger tactic.
+
+###  TODO
+* The linter seems to be silenced by `set_option ... in`: maybe it should enter `in`s?
+
+##  Implementation notes
+
+Yet another linter copied from the `unreachableTactic` linter!
+-/
+
+open Lean Elab
+
+namespace Mathlib.Linter
+
+/-- The unused tactic linter makes sure that every tactic call actually changes *something*. -/
+register_option linter.unusedTactic : Bool := {
+  defValue := true
+  descr := "enable the unused tactic linter"
+}
+
+namespace UnusedTactic
+
+/-- The monad for collecting the ranges of the syntaxes that do not modify any goal. -/
+abbrev M := StateRefT (HashMap String.Range Syntax) IO
+
+/-- `Parser`s allowed to not change the tactic state. -/
+def allowed : HashSet SyntaxNodeKind:= HashSet.empty
+  |>.insert `Mathlib.Tactic.Says.says
+  |>.insert `Batteries.Tactic.«tacticOn_goal-_=>_»
+  -- attempt to speed up, by ignoring more tactics
+  |>.insert `by
+  |>.insert `null
+  |>.insert `«]»
+  |>.insert ``Lean.Parser.Term.byTactic
+  |>.insert ``Lean.Parser.Tactic.tacticSeq
+  |>.insert ``Lean.Parser.Tactic.tacticSeq1Indented
+  |>.insert ``Lean.Parser.Tactic.tacticTry_
+
+  -- the following `SyntaxNodeKind`s play a role in silencing `test`s
+  |>.insert ``Lean.Parser.Tactic.guardHyp
+  |>.insert ``Lean.Parser.Tactic.guardTarget
+  |>.insert ``Lean.Parser.Tactic.failIfSuccess
+  |>.insert `Mathlib.Tactic.successIfFailWithMsg
+  |>.insert `Mathlib.Tactic.failIfNoProgress
+  |>.insert `Mathlib.Tactic.ExtractGoal.extractGoal
+  |>.insert `Mathlib.Tactic.Propose.propose'
+  |>.insert `Lean.Parser.Tactic.traceState
+  |>.insert `Mathlib.Tactic.tacticMatch_target_
+  |>.insert `change?
+  |>.insert `«tactic#adaptation_note_»
+
+/--
+A list of blacklisted syntax kinds, which are expected to have subterms that contain
+unevaluated tactics.
+-/
+initialize ignoreTacticKindsRef : IO.Ref NameHashSet ←
+  IO.mkRef <| HashSet.empty
+    |>.insert `Mathlib.Tactic.Says.says
+    |>.insert ``Parser.Term.binderTactic
+    |>.insert ``Lean.Parser.Term.dynamicQuot
+    |>.insert ``Lean.Parser.Tactic.quotSeq
+    |>.insert ``Lean.Parser.Tactic.tacticStop_
+    |>.insert ``Lean.Parser.Command.notation
+    |>.insert ``Lean.Parser.Command.mixfix
+    |>.insert ``Lean.Parser.Tactic.discharger
+    |>.insert ``Lean.Parser.Tactic.Conv.conv
+    |>.insert `Batteries.Tactic.seq_focus
+    |>.insert `Mathlib.Tactic.Hint.registerHintStx
+    |>.insert `Mathlib.Tactic.LinearCombination.linearCombination
+    -- the following `SyntaxNodeKind`s play a role in silencing `test`s
+    |>.insert ``Lean.Parser.Tactic.failIfSuccess
+    |>.insert `Mathlib.Tactic.successIfFailWithMsg
+    |>.insert `Mathlib.Tactic.failIfNoProgress
+
+/-- Is this a syntax kind that contains intentionally unused tactic subterms? -/
+def isIgnoreTacticKind (ignoreTacticKinds : NameHashSet) (k : SyntaxNodeKind) : Bool :=
+  k.components.contains `Conv ||
+  "slice".isPrefixOf k.toString ||
+  match k with
+  | .str _ "quot" => true
+  | _ => ignoreTacticKinds.contains k
+
+/--
+Adds a new syntax kind whose children will be ignored by the `unusedTactic` linter.
+This should be called from an `initialize` block.
+-/
+def addIgnoreTacticKind (kind : SyntaxNodeKind) : IO Unit :=
+  ignoreTacticKindsRef.modify (·.insert kind)
+
+variable (ignoreTacticKinds : NameHashSet) (isTacKind : SyntaxNodeKind → Bool) in
+/-- Accumulates the set of tactic syntaxes that should be evaluated at least once. -/
+@[specialize] partial def getTactics (stx : Syntax) : M Unit := do
+  if let .node _ k args := stx then
+    if !isIgnoreTacticKind ignoreTacticKinds k then
+      args.forM getTactics
+    if isTacKind k then
+      if let some r := stx.getRange? true then
+        modify fun m => m.insert r stx
+
+/-- `getNames mctx` extracts the names of all the local declarations implied by the
+`MetavarContext` `mctx`. -/
+def getNames (mctx : MetavarContext) : List Name :=
+  let lcts := mctx.decls.toList.map (MetavarDecl.lctx ∘ Prod.snd)
+  let locDecls := (lcts.map (PersistentArray.toList ∘ LocalContext.decls)).join.reduceOption
+  locDecls.map LocalDecl.userName
+
+mutual
+/-- Search for tactic executions in the info tree and remove the syntax of the tactics that
+changed something. -/
+partial def eraseUsedTacticsList (trees : PersistentArray InfoTree) : M Unit :=
+  trees.forM eraseUsedTactics
+
+/-- Search for tactic executions in the info tree and remove the syntax of the tactics that
+changed something. -/
+partial def eraseUsedTactics : InfoTree → M Unit
+  | .node i c => do
+    if let .ofTacticInfo i := i then
+      let stx := i.stx
+      let kind := stx.getKind
+      if let some r := stx.getRange? true then
+        if allowed.contains kind
+        -- if the tactic is allowed to not change the goals
+        then modify (·.erase r)
+        else
+        -- if the goals have changed
+        if i.goalsAfter != i.goalsBefore
+        then modify (·.erase r)
+        -- bespoke check for `swap_var`: the only change that it does is
+        -- in the usernames of local declarations, so we check the names before and after
+        else
+        if (kind == `Mathlib.Tactic.«tacticSwap_var__,,») &&
+                (getNames i.mctxBefore != getNames i.mctxAfter)
+        then modify (·.erase r)
+    eraseUsedTacticsList c
+  | .context _ t => eraseUsedTactics t
+  | .hole _ => pure ()
+
+end
+
+/-- Gets the value of the `linter.unusedTactic` option. -/
+def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.unusedTactic o
+
+/-- The main entry point to the unused tactic linter. -/
+def unusedTacticLinter : Linter where run := withSetOptionIn fun stx => do
+  unless getLinterHash (← getOptions) && (← getInfoState).enabled do
+    return
+  if (← get).messages.hasErrors then
+    return
+  let cats := (Parser.parserExtension.getState (← getEnv)).categories
+  -- These lookups may fail when the linter is run in a fresh, empty environment
+  let some tactics := Parser.ParserCategory.kinds <$> cats.find? `tactic
+    | return
+  let some convs := Parser.ParserCategory.kinds <$> cats.find? `conv
+    | return
+  let trees ← getInfoTrees
+  let go : M Unit := do
+    getTactics (← ignoreTacticKindsRef.get) (fun k => tactics.contains k || convs.contains k) stx
+    eraseUsedTacticsList trees
+  let (_, map) ← go.run {}
+  let unused := 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}; unused.qsort (key ·.1 < key ·.1) do
+    if stx.getKind ∈ [``Batteries.Tactic.unreachable, ``Batteries.Tactic.unreachableConv] then
+      continue
+    if last.start ≤ r.start && r.stop ≤ last.stop then continue
+    Linter.logLint linter.unusedTactic stx m!"'{stx}' tactic does nothing"
+    last := r
+
+initialize addLinter unusedTacticLinter

scripts/noshake.json

@@ -224,6 +224,7 @@
   ["Mathlib.Algebra.Group.Basic", "Mathlib.Init.Order.LinearOrder"],
   "Mathlib.Tactic.Measurability":
   ["Mathlib.Algebra.Group.Defs", "Mathlib.Tactic.Measurability.Init"],
+  "Mathlib.Tactic.Linter.UnusedTactic": ["Batteries.Tactic.Unreachable"],
   "Mathlib.Tactic.Lemma": ["Lean.Parser.Command"],
   "Mathlib.Tactic.IrreducibleDef": ["Mathlib.Data.Subtype"],
   "Mathlib.Tactic.ITauto": ["Mathlib.Init.Logic"],

test/Group.lean

@@ -49,6 +49,7 @@ example (n : ℤ) (a b : G) : a^n*b^n*a^n*a^n*a^(-n)*a^(-n)*b^(-n)*a^(-n) = 1 :=
 
 example (x y : G) : (x⁻¹ * (x * y) * y⁻¹)⁻¹ = 1 := by group
 
+set_option linter.unusedTactic false in
 example (x : G) (h : x = 1) : x = 1 := by
   group
   exact h

test/RewriteSearch/Polynomial.lean

@@ -39,6 +39,9 @@ open
   Finsupp
   Polynomial
 
+-- mutes various `'done' tactic does nothing [linter.unusedTactic]`
+set_option linter.unusedTactic false
+
 -- Polynomial.degree_of_subsingleton.{u}
 #guard_msgs(drop info) in
 example {R : Type u} [Semiring R] {p : Polynomial R} [Subsingleton R] :

test/UnusedTactic.lean

@@ -0,0 +1,24 @@
+import Mathlib.Tactic.Linter.UnusedTactic
+import Mathlib.Tactic.AdaptationNote
+
+def why2 : True → True := (by refine ·)
+
+example : True := by
+  #adaptation_note /--hi-/
+  exact .intro
+
+-- both `;` and `<;>` are unseen by the linter
+example : True ∧ True := by
+  constructor <;> trivial;
+
+set_option linter.unusedTactic false
+/--
+warning: 'congr' tactic does nothing
+note: this linter can be disabled with `set_option linter.unusedTactic false`
+-/
+#guard_msgs in
+set_option linter.unusedTactic true in
+-- the linter notices that `congr` is unused
+example : True := by
+  congr
+  constructor

test/Zify.lean

@@ -20,7 +20,6 @@ example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) : c < a + 3*b := by
 -- set_option pp.coercions false
 example (a b c x y z : ℕ) (h : ¬ x*y*z < 0) (h2 : (c : ℤ) < a + 3 * b) : a + 3*b > c := by
   zify at h ⊢
-  push_cast at h
   guard_hyp h :~ ¬↑x * ↑y * ↑z < (0 : ℤ) -- TODO: canonize instances?
   guard_target =~ ↑c < (↑a : ℤ) + 3 * ↑b
   exact h2

test/congr.lean

@@ -88,6 +88,7 @@ example (s t : Set α) (f : Subtype s → α) (g : Subtype t → α) :
   · guard_target = HEq f g
     exact test_sorry
 
+set_option linter.unusedTactic false in
 /- `ι = κ` is not plausible -/
 example (f : ι → α) (g : κ → α) :
     Set.image f Set.univ = Set.image g Set.univ := by
@@ -119,6 +120,7 @@ example (p q r : Prop) : p ∧ q ↔ p ∧ r := by
   guard_target = q ↔ r
   exact test_sorry
 
+set_option linter.unusedTactic false in
 /- Congruence here is not OK by default since `α = β` is not generally plausible. -/
 example (α β) [inst1 : Add α] [inst2 : Add β] (x : α) (y : β) : HEq (x + x) (y + y) := by
   congr!
@@ -257,6 +259,7 @@ example (x y z : Nat) (h : x = z) (hy : y = 2) : 1 + x + y = g z + 2 := by
   funext
   simp [g, Nat.add_comm]
 
+set_option linter.unusedTactic false in
 example (Fintype : Type → Type)
     (α β : Type) (inst : Fintype α) (inst' : Fintype β) : HEq inst inst' := by
   congr!
@@ -290,6 +293,7 @@ example (x y x' : Nat) (hx : id x = id x') : x + y = x' + y := by
   congr! (config := { closePost := false })
   exact hx
 
+set_option linter.unusedTactic false in
 example : { f : Nat → Nat // f = id } :=
   ⟨?_, by
     -- prevents `rfl` from solving for `?m` in `?m = id`:

test/linarith.lean

@@ -671,6 +671,7 @@ example (a b c d e : ℚ)
     e = 3 := by
   linarith (config := { oracle := .fourierMotzkin })
 
+set_option linter.unusedTactic false in
 -- TODO: still broken with Fourier-Motzkin
 /--
 error: linarith failed to find a contradiction

test/norm_num.lean

@@ -549,6 +549,7 @@ section norm_num_erase
 
 example : 3 ^ 3 + 4 = 31 := by norm_num1
 
+set_option linter.unusedTactic false in
 attribute [-norm_num] Mathlib.Meta.NormNum.evalPow in
 example : 3 ^ 3 + 4 = 31 := by
   norm_num1
@@ -663,6 +664,7 @@ example : (- ((- (((66 - 86) - 36) / 94) - 3) / - - (77 / (56 - - - 79))) + 87)
 
 example : 2 ^ 13 - 1 = Int.ofNat 8191 := by norm_num1
 
+set_option linter.unusedTactic false in
 -- Since https://github.com/leanprover/lean4/pull/4177
 -- `simp` will continue even if given invalid theorem names (but generates an error)
 -- and this felicitously applies to `norm_num` too.

test/peel.lean

@@ -85,6 +85,7 @@ example (x y : ℝ) (h : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x + n = y + ε) :
   guard_target =ₐ x - ε = y - n
   linarith
 
+set_option linter.unusedTactic false in
 example (x y : ℝ) (h : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x + n = y + ε) :
     ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, x - ε = y - n := by
   peel h