[Merged by Bors] - feat(Tactic/Linter/UnusedTactic): also lint inside conv =>

Mathlib/CategoryTheory/Limits/Fubini.lean

@@ -591,7 +591,7 @@ theorem colimitFlipCompColimIsoColimitCompColim_ι_ι_hom (j) (k) :
       (colimitFlipCompColimIsoColimitCompColim F).hom =
         (colimit.ι _ k ≫ colimit.ι (F ⋙ colim) j : _ ⟶ colimit (F ⋙ colim)) := by
   dsimp [colimitFlipCompColimIsoColimitCompColim]
-  slice_lhs 1 3 => simp only
+  conv_lhs => slice 1 3
   simp [Equivalence.unit]
 
 set_option backward.defeqAttrib.useBackward true in
@@ -602,7 +602,7 @@ theorem colimitFlipCompColimIsoColimitCompColim_ι_ι_inv (k) (j) :
       (colimitFlipCompColimIsoColimitCompColim F).inv =
         (colimit.ι _ j ≫ colimit.ι (F.flip ⋙ colim) k : _ ⟶ colimit (F.flip ⋙ colim)) := by
   dsimp [colimitFlipCompColimIsoColimitCompColim]
-  slice_lhs 1 3 => simp only
+  conv_lhs => slice 1 3
   simp [Equivalence.counitInv]
 
 end
@@ -737,7 +737,7 @@ theorem colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_hom {j} {k} :
         (colimit.ι _ k ≫ colimit.ι (curry.obj G ⋙ colim) j :
           _ ⟶ colimit (curry.obj G ⋙ colim)) := by
   dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]
-  slice_lhs 1 3 => simp only
+  conv_lhs => slice 1 3
   simp
 
 set_option backward.defeqAttrib.useBackward true in
@@ -750,7 +750,7 @@ theorem colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv {j} {k} :
           colimit.ι (curry.obj _ ⋙ colim) k :
             _ ⟶ colimit (curry.obj (Prod.swap K J ⋙ G) ⋙ colim)) := by
   dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]
-  slice_lhs 1 3 => simp only
+  conv_lhs => slice 1 3
   rw [colimitIsoColimitCurryCompColim_ι_ι_inv, HasColimit.ι_isoOfEquivalence_inv]
   dsimp [Equivalence.counitInv]
   rw [CategoryTheory.Bifunctor.map_id]

Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean

@@ -355,7 +355,6 @@ def limitOfDiagramInitial {X : J} (tX : IsInitial X) (F : J ⥤ C) :
     IsLimit (coneOfDiagramInitial tX F) where
   lift s := s.π.app X
   uniq s m w := by
-    conv_lhs => dsimp
     simp_rw [← w X, coneOfDiagramInitial_π_app, tX.hom_ext (tX.to X) (𝟙 _)]
     simp
 

Mathlib/CategoryTheory/Monoidal/Hopf_.lean

@@ -238,7 +238,6 @@ theorem antipode_comul₂ (A : C) [HopfObj A] :
   slice_lhs 2 3 =>
     simp only [← whiskerLeft_comp]
     rw [ComonObj.counit_comul]
-    simp only [whiskerLeft_comp]
   slice_lhs 3 4 =>
     simp only [← whiskerLeft_comp]
     rw [BraidedCategory.braiding_naturality_left]
@@ -386,7 +385,6 @@ theorem mul_antipode₂ (A : C) [HopfObj A] :
   slice_lhs 6 7 =>
     simp only [← whiskerLeft_comp]
     rw [MonObj.one_mul]
-    simp only [whiskerLeft_comp]
   slice_lhs 3 4 =>
     simp only [← whiskerLeft_comp]
     rw [← BraidedCategory.braiding_naturality_left]
@@ -400,7 +398,6 @@ theorem mul_antipode₂ (A : C) [HopfObj A] :
   slice_lhs 6 7 =>
     simp only [← whiskerLeft_comp]
     rw [Iso.inv_hom_id]
-    simp only [whiskerLeft_comp]
   simp only [whiskerLeft_id, Category.id_comp]
   slice_lhs 5 6 =>
     rw [whiskerLeft_rightUnitor, Category.assoc, ← rightUnitor_naturality]
@@ -414,7 +411,6 @@ theorem mul_antipode₂ (A : C) [HopfObj A] :
   slice_lhs 2 3 =>
     rw [← whisker_exchange]
   slice_lhs 1 2 =>
-    dsimp
     rw [← tensorHom_def]
   slice_lhs 2 3 =>
     rw [rightUnitor_naturality]

Mathlib/Tactic/Linter/UnusedTactic.lean

@@ -36,8 +36,6 @@ 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, ...`.
@@ -82,12 +80,14 @@ abbrev M := StateRefT (Std.HashMap Lean.Syntax.Range Syntax) IO
   Lean.Parser.Tactic.tacticTry_
   -- the following `SyntaxNodeKind`s play a role in silencing `test`s
   Lean.Parser.Tactic.guardHyp
+  Lean.Parser.Tactic.guardHypConv
   Lean.Parser.Tactic.guardTarget
+  Lean.Parser.Tactic.guardTargetConv
   Lean.Parser.Tactic.failIfSuccess
 
 /--
 A list of blocklisted syntax kinds, which are expected to have subterms that contain
-unevaluated tactics.
+unused tactics.
 -/
 initialize ignoreTacticKindsRef : IO.Ref NameHashSet ←
   IO.mkRef <| .ofArray #[
@@ -99,7 +99,6 @@ initialize ignoreTacticKindsRef : IO.Ref NameHashSet ←
     ``Lean.Parser.Command.notation,
     ``Lean.Parser.Command.mixfix,
     ``Lean.Parser.Tactic.discharger,
-    ``Lean.Parser.Tactic.Conv.conv,
     ``Lean.Parser.Command.registerTryTactic,
     `Batteries.Tactic.seq_focus,
     `Mathlib.Tactic.Hint.registerHintStx,
@@ -108,6 +107,7 @@ initialize ignoreTacticKindsRef : IO.Ref NameHashSet ←
     `Aesop.Frontend.Parser.addRules,
     `Aesop.Frontend.Parser.aesopTactic,
     `Aesop.Frontend.Parser.aesopTactic?,
+    ``Mathlib.Linter.UnusedTactic.«command#show_kind_»,
     -- the following `SyntaxNodeKind`s play a role in silencing `test`s
     ``Lean.Parser.Tactic.failIfSuccess,
     `Mathlib.Tactic.successIfFailWithMsg,
@@ -116,8 +116,6 @@ initialize ignoreTacticKindsRef : IO.Ref NameHashSet ←
 
 /-- 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 ||
   k matches .str _ "quot" ||
   ignoreTacticKinds.contains k
 
@@ -128,12 +126,12 @@ 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
+@[specialize] partial def getTactics (ignoreTacticKinds : NameHashSet)
+    (isTacKind : SyntaxNodeKind → Bool) (stx : Syntax) : M Unit := do
   if let .node _ k args := stx then
     if !isIgnoreTacticKind ignoreTacticKinds k then
-      args.forM getTactics
+      args.forM (getTactics ignoreTacticKinds isTacKind)
     if isTacKind k then
       if let some r := stx.getRange? true then
         modify fun m => m.insert r stx
@@ -175,7 +173,6 @@ def unusedTacticLinter : Linter where run := withSetOptionIn fun stx => do
     return
   if (← get).messages.hasErrors then
     return
-  if stx.isOfKind ``Mathlib.Linter.UnusedTactic.«command#show_kind_» then return
   let env ← getEnv
   let cats := (Parser.parserExtension.getState env).categories
   -- These lookups may fail when the linter is run in a fresh, empty environment
@@ -196,7 +193,7 @@ def unusedTacticLinter : Linter where run := withSetOptionIn fun stx => 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"
+    Linter.logLint linter.unusedTactic stx m!"Unused tactic linter: `{stx}` does nothing"
     last := r
 
 initialize addLinter unusedTacticLinter

Mathlib/Tactic/Linter/UnusedTacticExtension.lean

@@ -58,17 +58,19 @@ public initialize allowedRef : IO.Ref (Std.HashSet SyntaxNodeKind) ←
     `by,
     `null,
     `«]»,
-    `Lean.Parser.Tactic.show,
+    ``Lean.Parser.Tactic.show,
     -- the following `SyntaxNodeKind`s play a role in silencing `test`s
     `Mathlib.Tactic.successIfFailWithMsg,
     `Mathlib.Tactic.failIfNoProgress,
     `Mathlib.Tactic.ExtractGoal.extractGoal,
-    `Lean.Parser.Tactic.traceState,
+    ``Lean.Parser.Tactic.traceState,
+    ``Lean.Parser.Tactic.Conv.convTrace_state,
     `Mathlib.Tactic.tacticMatch_target_,
     `change?,
     `«tactic#adaptation_note_»,
     `tacticSleep_heartbeats_,
-    `Mathlib.Tactic.«tacticRename_bvar_→__»
+    `Mathlib.Tactic.«tacticRename_bvar_→__»,
+    ``Lean.Parser.Tactic.Conv.skip
   ]
 
 /--

MathlibTest/Linter/UnusedTactic.lean

@@ -11,7 +11,7 @@ example : 0 + 1 = 1 := by
   rfl
 
 /--
-warning: 'change 1 = 1' tactic does nothing
+warning: Unused tactic linter: `change 1 = 1` does nothing
 
 Note: This linter can be disabled with `set_option linter.unusedTactic false`
 -/
@@ -33,11 +33,11 @@ example : True ∧ True := by
 
 set_option linter.unusedTactic true
 /--
-warning: 'congr' tactic does nothing
+warning: Unused tactic linter: `congr` does nothing
 
 Note: This linter can be disabled with `set_option linter.unusedTactic false`
 ---
-warning: 'done' tactic does nothing
+warning: Unused tactic linter: `done` does nothing
 
 Note: This linter can be disabled with `set_option linter.unusedTactic false`
 -/
@@ -48,6 +48,35 @@ example : True := by
   constructor
   done
 
+/--
+warning: Unused tactic linter: `show False` does nothing
+
+Note: This linter can be disabled with `set_option linter.unusedTactic false`
+-/
+#guard_msgs in
+example : True := by
+  show True -- `show` does not warn.
+  guard_target = True -- `guard_target` also does not warn
+  trivial <;> show False -- But, if it doesn't run at all, `show` does warn.
+
+/--
+warning: Unused tactic linter: `simp` does nothing
+
+Note: This linter can be disabled with `set_option linter.unusedTactic false`
+-/
+#guard_msgs in
+example : True := by
+  conv =>
+    skip -- `skip` in `conv` mode does not warn.
+    guard_target = True -- `guard_target` also does not warn
+    simp -- other tactics in `conv` mode do warn
+  trivial
+
+example (a b : Nat) (h : a + 1 ≤ b + 1) : max a b ≤ b := by
+  -- The linter does not look inside of dischargers, no matter whether it's actually used or not.
+  have : True := by simp (disch := grind)
+  simp (disch := grind) [Nat.max_eq_right]
+
 section allowing_more_unused_tactics
 
 /-- info: The `SyntaxNodeKind` is 'Lean.Parser.Tactic.refine'. -/

MathlibTest/TacticAnalysis.lean

@@ -363,7 +363,7 @@ info: `skip` (+1 later steps) can be replaced with `grind`
 ---
 info: `rfl` can be replaced with `grind`
 ---
-warning: 'skip' tactic does nothing
+warning: Unused tactic linter: `skip` does nothing
 
 Note: This linter can be disabled with `set_option linter.unusedTactic false`
 -/