[Merged by Bors] - feat: have/let linter

Mathlib.lean

@@ -3627,6 +3627,7 @@ import Mathlib.Tactic.GuardGoalNums
 import Mathlib.Tactic.GuardHypNums
 import Mathlib.Tactic.Have
 import Mathlib.Tactic.HaveI
+import Mathlib.Tactic.HaveLetLinter
 import Mathlib.Tactic.HelpCmd
 import Mathlib.Tactic.HigherOrder
 import Mathlib.Tactic.Hint

Mathlib/Tactic.lean

@@ -82,6 +82,7 @@ import Mathlib.Tactic.GuardGoalNums
 import Mathlib.Tactic.GuardHypNums
 import Mathlib.Tactic.Have
 import Mathlib.Tactic.HaveI
+import Mathlib.Tactic.HaveLetLinter
 import Mathlib.Tactic.HelpCmd
 import Mathlib.Tactic.HigherOrder
 import Mathlib.Tactic.Hint

Mathlib/Tactic/HaveLetLinter.lean

@@ -0,0 +1,99 @@
+/-
+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 Std.Data.List.Basic
+
+/-!
+#  The `have` vs `let` linter
+
+The `have` vs `let` linter flags uses of `have` to introduce a hypothesis whose Type is not `Prop`.
+
+TODO:
+* `replace` implies `have`: should it be ignored?
+* `haveI` may need to change to `let/letI`?
+* also do `let` vs `have`.
+-/
+
+open Lean Elab Command Meta
+
+namespace Mathlib.Linter
+
+/-- The `have` vs `let` linter emits a warning on `have`s introducing a hypothesis whose
+Type is not `Prop`. -/
+register_option linter.haveLet : Bool := {
+  defValue := true
+  descr := "enable the `have` vs `let` linter"
+}
+
+namespace haveLet
+
+/-- find the `have` syntax. -/
+partial
+def isHave? : Syntax → Bool
+  | .node _ ``Lean.Parser.Tactic.tacticHave_ _ => true
+  |_ => false
+
+/-- `SyntaxNodeKind`s that imply a `have` but should be ignored anyway. -/
+abbrev exclusions : HashSet SyntaxNodeKind := HashSet.empty
+  |>.insert ``Lean.Parser.Tactic.replace
+  |>.insert `Std.Tactic.classical!
+  |>.insert `Mathlib.Tactic.Tauto.tauto
+
+end haveLet
+
+end Mathlib.Linter
+
+namespace Mathlib.Linter.haveLet
+
+/-- returns the `have` syntax whose corresponding hypothesis does not have Type `Prop` and
+also a `Format`ted version of the corresponding Type. -/
+partial
+def nonPropHaves : InfoTree → CommandElabM (Array (Syntax × Format))
+  | .node i args => do
+    let nargs := (← args.toArray.mapM nonPropHaves).flatten
+    if let .ofTacticInfo i := i then
+      let stx := i.stx
+      if exclusions.contains stx.getKind then return #[] else
+      if isHave? stx then
+        let mctx := i.mctxAfter
+        let mvdecls := (i.goalsAfter.map (mctx.decls.find? ·)).reduceOption
+        let _ : Ord MetavarDecl := { compare := (compare ·.index ·.index) }
+        -- we extract the `MetavarDecl` with largest index after a `have`, since this one
+        -- holds information about the metavariable where `have` introduces the new hypothesis.
+        let largestIdx := mvdecls.toArray.qsort (·.index > ·.index)
+        -- the relevant `LocalContext`
+        let lc := (largestIdx.getD 0 default).lctx
+        -- and the last declaration introduced: the one that `have` created
+        let ld := (lc.lastDecl.getD default).type
+        -- now, we get the `MetaM` state up and running to find the type of `ld`
+        let res ← liftCoreM do MetaM.run (ctx := { lctx := lc }) (s := { mctx := mctx }) <| do
+            let typ ← inferType (← instantiateMVars ld)
+            if ! typ.isProp then
+              return nargs.push (stx, ← ppExpr ld)
+            else return nargs
+        return res.1
+      else return nargs
+    else return nargs
+  | .context _ t => nonPropHaves t
+  | .hole _ => return #[]
+
+/-- Gets the value of the `linter.haveLet` option. -/
+def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.haveLet o
+
+/-- The main implementation of the `have` vs `let` linter. -/
+def haveLetLinter : Linter where run := withSetOptionIn fun _stx => do
+  unless getLinterHash (← getOptions) && (← getInfoState).enabled do
+    return
+  if (← MonadState.get).messages.hasErrors then
+    return
+  let trees ← getInfoTrees
+  for t in trees.toArray do
+    for (s, fmt) in ← nonPropHaves t do
+      Linter.logLint linter.haveLet s m!"'{fmt}' is a Type and not a Prop. \
+        Consider using 'let' instead of 'have'"
+
+initialize addLinter haveLetLinter

test/HaveLetLinter.lean

@@ -0,0 +1,73 @@
+import Mathlib.Tactic.HaveLetLinter
+import Mathlib.Tactic.Tauto
+
+#guard_msgs in
+-- check that `tauto` does not trigger the linter
+example : True := by
+  tauto
+
+#guard_msgs in
+-- replace is ignored, no matter what
+example : True := by
+  let zero := 0
+  replace _zero := zero
+  let eq := (rfl : 0 = 0)
+  replace _eq := eq
+  exact .intro
+
+set_option linter.haveLet false in
+set_option linter.haveLet true in
+/--
+warning: 'Nat' is a Type and not a Prop. Consider using 'let' instead of 'have' [linter.haveLet]
+---
+warning: 'Nat' is a Type and not a Prop. Consider using 'let' instead of 'have' [linter.haveLet]
+---
+warning: 'Nat' is a Type and not a Prop. Consider using 'let' instead of 'have' [linter.haveLet]
+---
+warning: 'Nat' is a Type and not a Prop. Consider using 'let' instead of 'have' [linter.haveLet]
+-/
+#guard_msgs in
+example : True := by
+  have _a := 0
+  have _b : Nat := 0
+  have _b : 0 = 0 := rfl
+  have _oh : Nat := 0
+  have _b : Nat := 2
+  tauto
+
+set_option linter.haveLet false in
+set_option linter.haveLet true in
+/--
+warning: 'Nat' is a Type and not a Prop. Consider using 'let' instead of 'have' [linter.haveLet]
+-/
+#guard_msgs in
+example : True := by
+  have := Nat.succ ?_;
+  exact .intro
+  exact 0
+
+#guard_msgs in
+example : True := by
+  have := And.intro (Nat.add_comm ?_ ?_) (Nat.add_comm ?_ ?_)
+  apply True.intro
+  exact 0
+  exact 0
+  exact 0
+  exact 0
+
+#guard_msgs in
+example (h : False) : True := by
+  have : False := h
+  exact .intro
+
+-- (← `(tactic| have := 0))
+
+set_option linter.haveLet false in
+set_option linter.haveLet true in
+/--
+warning: 'Nat' is a Type and not a Prop. Consider using 'let' instead of 'have' [linter.haveLet]
+-/
+#guard_msgs in
+theorem ghi : True := by
+  have : Nat := Nat.succ 1;
+  exact .intro