fix: update defLemma and related linters correctly

Batteries/Tactic/Lint/Misc.lean

@@ -68,69 +68,49 @@ We skip all declarations that contain `sorry` in their value. -/
   noErrorsFound := "No definitions are missing documentation."
   errorsFound := "DEFINITIONS ARE MISSING DOCUMENTATION STRINGS:"
   test declName := do
-    -- leanprover/lean4#12263: isGlobalInstance was removed, use isInstance instead
-    if (← isAutoDecl declName) || (← isInstance declName) then
-      return none -- FIXME: scoped/local instances should also not be linted
+    if ← isAutoDecl declName <||> isInstance declName then
+      return none
     if let .str p _ := declName then
       if ← isInstance p then
-        -- auxillary functions for instances should not be linted
+        -- auxiliary functions for instances should not be linted
         return none
     if let .str _ s := declName then
       if s == "parenthesizer" || s == "formatter" || s == "delaborator" || s == "quot" then
-      return none
+        return none
     let kind ← match ← getConstInfo declName with
-      | .axiomInfo .. => pure "axiom"
-      | .opaqueInfo .. => pure "constant"
-      | .defnInfo info =>
-          -- leanprover/lean4#2575: Prop projections are generated as `def`s
-          if ← isProjectionFn declName <&&> isProp info.type then
-            return none
-          pure "definition"
+      | .axiomInfo ..  => pure "axiom"
+      | .opaqueInfo .. => pure "opaque constant"
+      | .defnInfo ..   => pure "definition"
       | .inductInfo .. => pure "inductive"
       | _ => return none
-    let (none) ← findDocString? (← getEnv) declName | return none
-    return m!"{kind} missing documentation string"
+    if (← findDocString? (← getEnv) declName).isSome then return none else
+      return m!"{kind} missing documentation string"
 
 /-- A linter for checking theorem doc strings. -/
 @[env_linter disabled] def docBlameThm : Linter where
   noErrorsFound := "No theorems are missing documentation."
   errorsFound := "THEOREMS ARE MISSING DOCUMENTATION STRINGS:"
   test declName := do
-    if ← isAutoDecl declName then
+    if ← isAutoDecl declName then return none
+    unless (← getConstInfo declName) matches .thmInfo .. do
       return none
-    let kind ← match ← getConstInfo declName with
-      | .thmInfo .. => pure "theorem"
-      | .defnInfo info =>
-          -- leanprover/lean4#2575:
-          -- projections are generated as `def`s even when they should be `theorem`s
-          if ← isProjectionFn declName <&&> isProp info.type then
-            pure "Prop projection"
-          else
-            return none
-      | _ => return none
-    let (none) ← findDocString? (← getEnv) declName | return none
-    return m!"{kind} missing documentation string"
+    if (← findDocString? (← getEnv) declName).isSome then return none else
+      return m!"theorem missing documentation string"
 
 /-- A linter for checking whether the correct declaration constructor (definition or theorem)
 has been used. -/
 @[env_linter] def defLemma : Linter where
   noErrorsFound := "All declarations correctly marked as def/lemma."
   errorsFound := "INCORRECT DEF/LEMMA:"
   test declName := do
-    if (← isAutoDecl declName) || (← isImplicitReducible declName) then
-      return none
-    -- leanprover/lean4#2575:
-    -- projections are generated as `def`s even when they should be `theorem`s
-    if ← isProjectionFn declName then return none
+    if ← isAutoDecl declName then return none
     let info ← getConstInfo declName
-    let isThm ← match info with
-      | .defnInfo .. => pure false
-      | .thmInfo .. => pure true
-      | _ => return none
-    match isThm, ← isProp info.type with
-    | true, false => pure "is a lemma/theorem, should be a def"
-    | false, true => pure "is a def, should be lemma/theorem"
-    | _, _ => return none
+    if info.isDefinition then
+      -- Delta-derived instances are not theorems even when they should be. (leanprover/lean4#13295)
+      -- The only indication we have is that they are instances marked `@[implicit_reducible]`.
+      if ← isInstance declName <&&> isImplicitReducible declName then return none
+      if ← isProp info.type then return some "is a def, should be a lemma/theorem"
+    return none
 
 /-- A linter for checking whether statements of declarations are well-typed. -/
 @[env_linter] def checkType : Linter where

BatteriesTest/lint_defLemma.lean

@@ -0,0 +1,18 @@
+import Batteries.Tactic.Lint
+
+@[implicit_reducible]
+def foo : True := trivial
+
+@[reducible, instance]
+def bar : Nonempty Bool := ⟨true⟩
+
+instance bar' : Nonempty String := ⟨""⟩
+
+/--
+error: /- The `defLemma` linter reports:
+INCORRECT DEF/LEMMA: -/
+#check foo /- is a def, should be a lemma/theorem -/
+#check bar /- is a def, should be a lemma/theorem -/
+-/
+#guard_msgs in
+#lint- only defLemma