feat: add lemma code-action

Batteries.lean

@@ -80,6 +80,7 @@ import Batteries.Tactic.Congr
 import Batteries.Tactic.Exact
 import Batteries.Tactic.Init
 import Batteries.Tactic.Instances
+import Batteries.Tactic.Lemma
 import Batteries.Tactic.Lint
 import Batteries.Tactic.Lint.Basic
 import Batteries.Tactic.Lint.Frontend

Batteries/Tactic/Lemma.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2024 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Damiano Testa
+-/
+import Lean.Meta.Tactic.TryThis
+
+/-!
+#  Control for `lemma` command
+
+The `lemma` command exists in `Mathlib`, but not in `Std`.
+
+This file enforces the convention by introducing a code-action
+to replace `lemma` by `theorem`.
+-/
+
+namespace Batteries.Tactic.Lemma
+
+open Lean Elab.Command Meta.Tactic
+
+/-- Enables the use of `lemma` as a synonym for `theorem` -/
+register_option lang.lemmaCmd : Bool := {
+  defValue := false
+  descr := "enable the use of the `lemma` command as a synonym for `theorem`"
+}
+
+/-- Check whether `lang.lemmaCmd` option is enabled -/
+def checkLangLemmaCmd (o : Options) : Bool := o.get `lang.lemmaCmd lang.lemmaCmd.defValue
+
+/-- `lemma` is not supported, please use `theorem` instead -/
+syntax (name := lemmaCmd) declModifiers
+  group("lemma " declId ppIndent(declSig) declVal) : command
+
+/-- Elaborator for the `lemma` command, if the option `lang.lemmaCmd` is false the command
+emits a warning and code action instructing the user to use `theorem` instead.-/
+@[command_elab «lemmaCmd»] def elabLemma : CommandElab := fun stx => do
+  unless checkLangLemmaCmd (← getOptions) do
+    let lemmaStx := stx[1][0]
+    Elab.Command.liftTermElabM <|
+      TryThis.addSuggestion lemmaStx { suggestion := "theorem" }
+    logErrorAt lemmaStx
+      "`lemma` is not supported by default, please use `theorem` instead.\n\
+      Use `set_option lang.lemmaCmd true` to enable the use of the `lemma` command in a file.\n\
+      Use the command line option `-Dlang.lemmaCmd=true` to enable the use of `lemma` globally."
+  let out ← Elab.liftMacroM <| do
+    let stx := stx.modifyArg 1 fun stx =>
+      let stx := stx.modifyArg 0 (mkAtomFrom · "theorem" (canonical := true))
+      stx.setKind ``Parser.Command.theorem
+    pure <| stx.setKind ``Parser.Command.declaration
+  Elab.Command.elabCommand out

test/lemma_cmd.lean

@@ -0,0 +1,34 @@
+import Batteries.Tactic.Lemma
+
+-- lemma disabled by default
+/--
+info: Try this: theorem
+---
+error: `lemma` is not supported by default, please use `theorem` instead.
+Use `set_option lang.lemmaCmd true` to enable the use of the `lemma` command in a file.
+Use the command line option `-Dlang.lemmaCmd=true` to enable the use of `lemma` globally.
+-/
+#guard_msgs in
+lemma test1 : 3 < 7 := by decide
+
+-- lemma enabled for one command
+set_option lang.lemmaCmd true in
+lemma test2 : 3 < 7 := by decide
+
+-- lemma disabled again
+/--
+info: Try this: theorem
+---
+error: `lemma` is not supported by default, please use `theorem` instead.
+Use `set_option lang.lemmaCmd true` to enable the use of the `lemma` command in a file.
+Use the command line option `-Dlang.lemmaCmd=true` to enable the use of `lemma` globally.
+-/
+#guard_msgs in
+lemma test3 : 3 < 7 := by decide
+
+-- lemma enabled for rest of file
+set_option lang.lemmaCmd true
+
+lemma test4 : 3 < 7 := by decide
+
+lemma test5 : 3 < 7 := by decide