[Merged by Bors] - feat: the multiGoal linter

Mathlib.lean

@@ -4397,6 +4397,7 @@ import Mathlib.Tactic.Linter.HaveLetLinter
 import Mathlib.Tactic.Linter.Header
 import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.Linter.MinImports
+import Mathlib.Tactic.Linter.Multigoal
 import Mathlib.Tactic.Linter.OldObtain
 import Mathlib.Tactic.Linter.PPRoundtrip
 import Mathlib.Tactic.Linter.RefineLinter

Mathlib/Analysis/Analytic/Within.lean

@@ -113,6 +113,7 @@ result for `AnalyticOn`, as this requires a bit more work to show that local ext
 be stitched together.
 -/
 
+set_option linter.style.multiGoal false in
 /-- `f` has power series `p` at `x` iff some local extension of `f` has that series -/
 lemma hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall [CompleteSpace F] {f : E → F}
     {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ℝ≥0∞} :

Mathlib/Init.lean

@@ -4,6 +4,7 @@ import Mathlib.Tactic.Linter.GlobalAttributeIn
 import Mathlib.Tactic.Linter.Header
 -- This file imports Batteries.Tactic.Lint, where the `env_linter` attribute is defined.
 import Mathlib.Tactic.Linter.Lint
+import Mathlib.Tactic.Linter.Multigoal
 import Mathlib.Tactic.Linter.OldObtain
 import Mathlib.Tactic.Linter.RefineLinter
 import Mathlib.Tactic.Linter.UnusedTactic

Mathlib/LinearAlgebra/Eigenspace/Basic.lean

@@ -376,7 +376,7 @@ lemma isNilpotent_restrict_unifEigenspace_top [IsNoetherian R M] (f : End R M) (
       mapsTo_unifEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ _) :
     IsNilpotent ((f - μ • 1).restrict h) := by
   apply isNilpotent_restrict_of_le
-  swap; apply isNilpotent_restrict_unifEigenspace_nat f μ (maxUnifEigenspaceIndex f μ)
+  on_goal 2 => apply isNilpotent_restrict_unifEigenspace_nat f μ (maxUnifEigenspaceIndex f μ)
   rw [unifEigenspace_top_eq_maxUnifEigenspaceIndex]
 
 /-- The submodule `eigenspace f μ` for a linear map `f` and a scalar `μ` consists of all vectors `x`

Mathlib/Tactic.lean

@@ -144,6 +144,7 @@ import Mathlib.Tactic.Linter.HaveLetLinter
 import Mathlib.Tactic.Linter.Header
 import Mathlib.Tactic.Linter.Lint
 import Mathlib.Tactic.Linter.MinImports
+import Mathlib.Tactic.Linter.Multigoal
 import Mathlib.Tactic.Linter.OldObtain
 import Mathlib.Tactic.Linter.PPRoundtrip
 import Mathlib.Tactic.Linter.RefineLinter

Mathlib/Tactic/Linter/Multigoal.lean

@@ -0,0 +1,165 @@
+/-
+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
+
+/-!
+#  The "multiGoal" linter
+
+The "multiGoal" linter emits a warning where there is more than a single goal in scope.
+There is an exception: a tactic that closes *all* remaining goals is allowed.
+
+There are a few tactics, such as `skip`, `swap` or the `try` combinator, that are intended to work
+specifically in such a situation.
+Otherwise, the mathlib style guide ask that goals be be focused until there is only one active goal
+at a time.
+If this focusing does not happen, the linter emits a warning.
+Typically, the focusing is achieved by the `cdot`: `·`, but, e.g., `focus` or `on_goal x`
+also serve a similar purpose.
+
+TODO:
+* Should the linter flag unnecessary scoping as well?
+  For instance, should
+  ```lean
+  example : True := by
+    · · exact .intro
+  ```
+  raise a warning?
+* Custom support for "accumulating side-goals", so that once they are all in scope
+  they can be solved in bulk via `all_goals` or a similar tactic.
+* In development, `on_goal` has been partly used as a way of silencing the linter
+  precisely to allow the accumulation referred to in the previous item.
+  Maybe revisit usages of `on_goal` and also nested `induction` and `cases`.
+-/
+
+open Lean Elab
+
+namespace Mathlib.Linter
+
+/-- The "multiGoal" linter emits a warning when there are multiple active goals. -/
+register_option linter.style.multiGoal : Bool := {
+  defValue := false
+  descr := "enable the multiGoal linter"
+}
+
+namespace Style.multiGoal
+
+/-- The `SyntaxNodeKind`s in `exclusions` correspond to tactics that the linter allows,
+even though there are multiple active goals.
+Reasons for admitting a kind in `exclusions` include
+* the tactic focuses on one goal, e.g. `·`, `focus`, `on_goal i =>`, ...;
+* the tactic is reordering the goals, e.g. `swap`, `rotate_left`, ...;
+* the tactic is structuring a proof, e.g. `skip`, `<;>`, ...;
+* the tactic is creating new goals, e.g. `constructor`, `cases`, `induction`, ....
+
+There is some overlap in scope between `ignoreBranch` and `exclusions`.
+
+Tactic combinators like `repeat` or `try` are a mix of both.
+-/
+abbrev exclusions : Std.HashSet SyntaxNodeKind := .ofList [
+    -- structuring a proof
+    ``Lean.Parser.Term.cdot,
+    ``cdot,
+    ``cdotTk,
+    ``Lean.Parser.Tactic.tacticSeqBracketed,
+    `«;»,
+    `«<;>»,
+    ``Lean.Parser.Tactic.«tactic_<;>_»,
+    `«{»,
+    `«]»,
+    `null,
+    `then,
+    `else,
+    ``Lean.Parser.Tactic.«tacticNext_=>_»,
+    ``Lean.Parser.Tactic.tacticSeq1Indented,
+    ``Lean.Parser.Tactic.tacticSeq,
+    -- re-ordering goals
+    `Batteries.Tactic.tacticSwap,
+    ``Lean.Parser.Tactic.rotateLeft,
+    ``Lean.Parser.Tactic.rotateRight,
+    ``Lean.Parser.Tactic.skip,
+    `Batteries.Tactic.«tacticOn_goal-_=>_»,
+    `Mathlib.Tactic.«tacticSwap_var__,,»,
+    -- tactic combinators
+    ``Lean.Parser.Tactic.tacticRepeat_,
+    ``Lean.Parser.Tactic.tacticTry_,
+    -- creating new goals
+    ``Lean.Parser.Tactic.paren,
+    ``Lean.Parser.Tactic.case,
+    ``Lean.Parser.Tactic.constructor,
+    `Mathlib.Tactic.tacticAssumption',
+    ``Lean.Parser.Tactic.induction,
+    ``Lean.Parser.Tactic.cases,
+    ``Lean.Parser.Tactic.intros,
+    ``Lean.Parser.Tactic.injections,
+    ``Lean.Parser.Tactic.substVars,
+    `Batteries.Tactic.«tacticPick_goal-_»,
+    ``Lean.Parser.Tactic.case',
+    `«tactic#adaptation_note_»,
+    `tacticSleep_heartbeats_
+  ]
+
+/-- The `SyntaxNodeKind`s in `ignoreBranch` correspond to tactics that disable the linter from
+their first application until the corresponding proof branch is closed.
+Reasons for ignoring these tactics include
+* the linter gets confused by the proof management, e.g. `conv`;
+* the tactics are *intended* to act on multiple goals, e.g. `repeat`, `any_goals`, `all_goals`, ...
+
+There is some overlap in scope between `exclusions` and `ignoreBranch`.
+-/
+abbrev ignoreBranch : Std.HashSet SyntaxNodeKind := .ofList [
+    ``Lean.Parser.Tactic.Conv.conv,
+    `Mathlib.Tactic.Conv.convLHS,
+    `Mathlib.Tactic.Conv.convRHS,
+    ``Lean.Parser.Tactic.first,
+    ``Lean.Parser.Tactic.repeat',
+    ``Lean.Parser.Tactic.tacticIterate____,
+    ``Lean.Parser.Tactic.anyGoals,
+    ``Lean.Parser.Tactic.allGoals,
+    ``Lean.Parser.Tactic.focus
+  ]
+
+/-- `getManyGoals t` returns the syntax nodes of the `InfoTree` `t` corresponding to tactic calls
+which
+* leave at least one goal that was not present before it ran;
+* are not excluded through `exclusions` or `ignoreBranch`;
+
+together with the total number of goals
+-/
+partial
+def getManyGoals : InfoTree → Array (Syntax × Nat)
+  | .node info args =>
+    let kargs := (args.map getManyGoals).toArray.flatten
+    if let .ofTacticInfo info := info then
+      if ignoreBranch.contains info.stx.getKind then #[] else
+      if let .original .. := info.stx.getHeadInfo then
+        let newGoals := info.goalsAfter.filter (info.goalsBefore.contains ·)
+        if newGoals.length != 0 && !exclusions.contains info.stx.getKind then
+          kargs.push (info.stx, newGoals.length)
+        else kargs
+      else kargs
+    else kargs
+  | .context _ t => getManyGoals t
+  | _ => default
+
+@[inherit_doc Mathlib.Linter.linter.style.multiGoal]
+def multiGoalLinter : Linter where run := withSetOptionIn fun _stx ↦ do
+    unless Linter.getLinterValue linter.style.multiGoal (← getOptions) do
+      return
+    if (← get).messages.hasErrors then
+      return
+    let trees ← getInfoTrees
+    for t in trees.toArray do
+      for (s, n) in getManyGoals t do
+        Linter.logLint linter.style.multiGoal s
+          m!"There are {n+1} unclosed goals before '{s}' and \
+            at least one remaining goal afterwards.\n\
+            Please focus on the current goal, for instance using `·` (typed as \"\\.\")."
+
+initialize addLinter multiGoalLinter
+
+end Style.multiGoal
+
+end Mathlib.Linter

lakefile.lean

@@ -36,6 +36,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.style.longLine, true⟩,
   ⟨`linter.style.longFile, .ofNat 1500⟩,
   ⟨`linter.style.missingEnd, true⟩,
+  ⟨`linter.style.multiGoal, true⟩,
   ⟨`linter.style.setOption, true⟩
 ]
 

test/Multigoal.lean

@@ -0,0 +1,123 @@
+import Mathlib.Tactic.Basic
+import Mathlib.Tactic.Conv
+import Mathlib.Tactic.Linter.Multigoal
+import Mathlib.Util.SleepHeartbeats
+
+-- The warning generated by `linter.style.multiGoal` is not suppressed by `#guard_msgs`,
+-- because the linter is run on `#guard_msgs` itself. This is a known issue, see e.g.
+-- https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/unreachableTactic.20linter.20not.20suppressed.20by.20.60.23guard_msgs.60
+-- We jump through an extra hoop here to silence the warning.
+set_option linter.style.multiGoal false
+
+-- A deactivated linter does nothing.
+example : True := by
+  by_cases 0 = 0
+  exact .intro
+  exact .intro
+
+#guard_msgs(drop warning) in
+set_option linter.style.multiGoal true in
+/--
+warning: There are 2 unclosed goals before 'exact .intro' and at least one remaining goal afterwards.
+Please focus on the current goal, for instance using `·` (typed as "\.").
+note: this linter can be disabled with `set_option linter.style.multiGoal false`
+-/
+#guard_msgs in
+example : True := by
+  by_cases 0 = 0
+  exact .intro
+  exact .intro
+
+#guard_msgs(drop warning) in
+set_option linter.style.multiGoal true in
+/--
+warning: There are 2 unclosed goals before 'assumption' and at least one remaining goal afterwards.
+Please focus on the current goal, for instance using `·` (typed as "\.").
+note: this linter can be disabled with `set_option linter.style.multiGoal false`
+-/
+#guard_msgs in
+example {n : Nat} (hn : n = 0) : n + 0 = 0 := by
+  conv =>
+    congr
+    rw [← Nat.add_zero 0]
+  conv_lhs =>
+    congr
+    rw [← Nat.add_zero n]
+    rfl
+  conv_rhs =>
+    rw [← Nat.add_zero 0]
+    congr
+    rfl
+    rfl
+  by_cases 0 = 0
+  assumption
+  assumption
+
+set_option linter.unusedTactic false in
+#guard_msgs(drop warning) in
+set_option linter.style.multiGoal true in
+/--
+warning: There are 2 unclosed goals before 'rfl' and at least one remaining goal afterwards.
+Please focus on the current goal, for instance using `·` (typed as "\.").
+note: this linter can be disabled with `set_option linter.style.multiGoal false`
+-/
+#guard_msgs in
+example (p : Prop) (hp : p) : (0 = 0 ∧ p) ∨ 0 = 0 := by
+  iterate left; decide
+  repeat' left; decide
+  refine Or.inl ⟨?_, ?_⟩
+  rfl
+  assumption
+
+#guard_msgs(drop warning) in
+set_option linter.style.multiGoal true in
+/--
+warning: There are 3 unclosed goals before 'rfl' and at least one remaining goal afterwards.
+Please focus on the current goal, for instance using `·` (typed as "\.").
+note: this linter can be disabled with `set_option linter.style.multiGoal false`
+---
+warning: There are 2 unclosed goals before 'trivial' and at least one remaining goal afterwards.
+Please focus on the current goal, for instance using `·` (typed as "\.").
+note: this linter can be disabled with `set_option linter.style.multiGoal false`
+-/
+#guard_msgs in
+example : 0 = 0 ∧ 0 = 0 ∧ 0 = 0 := by
+  refine ⟨?_, ?_, ?_⟩
+  rfl
+  trivial
+  rfl
+
+example (p : Bool) : 0 = 0 := by
+  cases p
+  case' false => rfl
+  case' true => rfl
+
+#guard_msgs in
+-- `assumption'` is allowed, as it is useful precisely when there are multiple active goals
+example (p : Bool) (f : False) {h : 0 = 0} : 0 = 0 ∧ 0 = 1 := by
+  cases p <;>
+  constructor
+  assumption'
+  any_goals cases f
+
+#guard_msgs in
+-- `focus` is ignored
+example : True ∧ True := by
+  constructor
+  focus
+    exact .intro
+  focus
+    exact .intro
+
+set_option linter.unusedTactic false in
+example : 1 = 1 := by
+  sleep_heartbeats 1000
+  rfl
+
+-- we test that a tactic closing all remaining goals does not trigger the linter
+macro "bi_trivial" : tactic => `(tactic| (trivial; trivial))
+
+set_option linter.style.multiGoal true in
+example : True ∧ True := by
+  constructor
+  bi_trivial