feat: dupNamespace as a syntax linter (#11154)

An implementation of the `dupNamespace` from `Std` as a syntax linter.  The linter emits a warning for declarations that have a repeated, consecutive namespace:
* `Nat.Nat.foo` triggers the linter;
* `Nat.foo.Nat` does *not* trigger the linter.

*Note.* This linter will not detect duplication in namespaces of autogenerated declarations (other than the one whose `declId` is present in the source declaration).


[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60dupNamespace.60.20linter)

The linter found
```lean
private theorem Seminorm.Seminorm.isLUB_sSup ...
```
that is skipped by the environment `dupNamespace` linter.

Mathlib/Tactic/Lint.lean

@@ -3,6 +3,8 @@ Copyright (c) 2023 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
+import Lean.Linter.Util
+import Std.Data.Array.Basic
 import Std.Tactic.Lint
 
 /-!
@@ -34,3 +36,66 @@ Linter that checks whether a structure should be in Prop.
     let allProofs ← projs.allM (do isProof <| ← mkConstWithLevelParams <| declName ++ ·)
     unless allProofs do return none
     return m!"all fields are propositional but the structure isn't."
+
+end Std.Tactic.Lint
+
+/-!
+#  `dupNamespace` linter
+
+The `dupNamespace` linter produces a warning when a declaration contains the same namespace
+at least twice consecutively.
+
+For instance, `Nat.Nat.foo` and `One.two.two` trigger a warning, while `Nat.One.Nat` does not.
+-/
+
+namespace Mathlib.Linter
+
+/--
+The `dupNamespace` linter is set on by default.  Lean emits a warning on any declaration that
+contains the same namespace at least twice consecutively.
+
+For instance, `Nat.Nat.foo` and `One.two.two` trigger a warning, while `Nat.One.Nat` does not.
+
+*Note.*
+This linter will not detect duplication in namespaces of autogenerated declarations
+(other than the one whose `declId` is present in the source declaration).
+-/
+register_option linter.dupNamespace : Bool := {
+  defValue := true
+  descr := "enable the duplicated namespace linter"
+}
+
+namespace DupNamespaceLinter
+
+open Lean Parser Elab Command Meta
+
+/-- Gets the value of the `linter.dupNamespace` option. -/
+def getLinterDupNamespace (o : Options) : Bool := Linter.getLinterValue linter.dupNamespace o
+
+/-- `getIds stx` extracts the `declId` nodes from the `Syntax` `stx`.
+If `stx` is an `alias` or an `export`, then it extracts an `ident`, instead of a `declId`. -/
+partial
+def getIds : Syntax → Array Syntax
+  | .node _ `Std.Tactic.Alias.alias args => #[args[2]!]
+  | .node _ ``Lean.Parser.Command.export args => #[args[3]![0]]
+  | stx@(.node _ _ args) =>
+    ((args.attach.map fun ⟨a, _⟩ => getIds a).foldl (· ++ ·) #[stx]).filter (·.getKind == ``declId)
+  | _ => default
+
+@[inherit_doc linter.dupNamespace]
+def dupNamespace : Linter where run := withSetOptionIn fun stx => do
+  if getLinterDupNamespace (← getOptions) then
+    match getIds stx with
+      | #[id] =>
+        let ns := (← getScope).currNamespace
+        let declName := ns ++ (if id.getKind == ``declId then id[0].getId else id.getId)
+        let nm := declName.components
+        let some (dup, _) := nm.zip (nm.tailD []) |>.find? fun (x, y) => x == y
+          | return
+        Linter.logLint linter.dupNamespace id
+          m!"The namespace '{dup}' is duplicated in the declaration '{declName}'"
+      | _ => return
+
+initialize addLinter dupNamespace
+
+end Mathlib.Linter.DupNamespaceLinter

test/Lint.lean

@@ -0,0 +1,46 @@
+import Mathlib.Tactic.Lint
+import Mathlib.Tactic.ToAdditive
+
+set_option linter.dupNamespace true in
+/-- warning:
+The namespace 'add' is duplicated in the declaration 'add.add'
+[linter.dupNamespace]
+-/
+#guard_msgs in
+def add.add := True
+
+namespace Foo
+set_option linter.dupNamespace true in
+/-- warning:
+The namespace 'Foo' is duplicated in the declaration 'Foo.Foo.foo'
+[linter.dupNamespace]
+-/
+#guard_msgs in
+def Foo.foo := True
+
+-- the `dupNamespace` linter does not notice that `to_additive` created `Foo.add.add`.
+#guard_msgs in
+@[to_additive] theorem add.mul : True := .intro
+
+--  However, the declaration `Foo.add.add` is present in the environment.
+run_cmd Lean.Elab.Command.liftTermElabM do
+  let decl := (← Lean.getEnv).find? ``Foo.add.add
+  guard decl.isSome
+
+namespace Nat
+/--
+warning:
+The namespace 'Nat' is duplicated in the declaration 'Foo.Nat.Nat.Nats' [linter.dupNamespace]
+-/
+#guard_msgs in
+alias Nat.Nats := Nat
+
+end Nat
+end Foo
+
+namespace add
+/--
+warning: The namespace 'add' is duplicated in the declaration 'add.add' [linter.dupNamespace]
+-/
+#guard_msgs in
+export Nat (add)

test/Simps.lean

@@ -123,15 +123,15 @@ example (n : ℕ) : foo.rfl.toFun n = n := by rw [foo.rfl_toFun, id]
 example (n : ℕ) : foo.rfl.invFun n = n := by rw [foo.rfl_invFun]
 
 /- the declarations are `simp` lemmas -/
-@[simps] def foo : ℕ × ℤ := (1, 2)
+@[simps] def bar : ℕ × ℤ := (1, 2)
 
 -- note: in Lean 4 the first test succeeds without `@[simps]`, however, the remaining tests don't
-example : foo.1 = 1 := by simp
-example {a : ℕ} {h : 1 = a} : foo.1 = a := by rw [foo_fst, h]
-example {a : ℕ} {h : 1 = a} : foo.1 = a := by simp; rw [h]
-example {a : ℤ} {h : 2 = a} : foo.2 = a := by simp; rw [h]
-example {a : ℕ} {h : 1 = a} : foo.1 = a := by dsimp; rw [h] -- check that dsimp also unfolds
-example {a : ℤ} {h : 2 = a} : foo.2 = a := by dsimp; rw [h]
+example : bar.1 = 1 := by simp
+example {a : ℕ} {h : 1 = a} : bar.1 = a := by rw [bar_fst, h]
+example {a : ℕ} {h : 1 = a} : bar.1 = a := by simp; rw [h]
+example {a : ℤ} {h : 2 = a} : bar.2 = a := by simp; rw [h]
+example {a : ℕ} {h : 1 = a} : bar.1 = a := by dsimp; rw [h] -- check that dsimp also unfolds
+example {a : ℤ} {h : 2 = a} : bar.2 = a := by dsimp; rw [h]
 example {α} (x y : α) (h : x = y) : foo.rfl.toFun x = y := by simp; rw [h]
 example {α} (x y : α) (h : x = y) : foo.rfl.invFun x = y := by simp; rw [h]
 -- example {α} (x y : α) (h : x = y) : foo.rfl.toFun = @id α := by { successIfFail {simp}, rfl }