Linter

Lean.Elab.Command.Linter は、よくない書き方をされたコードを検出して警告を発してくれるツールです。

使用例

たとえば、選択原理を証明の中で使用すると警告してくれるリンターを自作することができます。¹ 以下のように記述したファイルを読み込みます。

-- LinterLib.lean の内容

import Lean.Util.CollectAxioms
import Mathlib.Tactic.DeclarationNames

/--
「detectClassical」リンターは、`Classical.choice` 公理に依存する宣言に対して警告を発する。
デフォルト値は `true`
-/
register_option linter.detectClassical : Bool := {
  defValue := true
  descr := "detectClassicalリンターを有効にする"
}

namespace DetectClassical

  open Lean Elab Command Mathlib.Linter

  @[inherit_doc linter.detectClassical]
  def detectClassicalLinter : Linter where
    run := withSetOptionIn fun stx ↦ do
      -- リンターが有効になっていなければ何もしない
      unless Linter.getLinterValue linter.detectClassical (← getOptions) do
        return

      -- どこかにエラーがあれば何もしない
      if (← get).messages.hasErrors then
        return

      -- ユーザが定義した名前を取得する
      let names := (← getNamesFrom (stx.getPos?.getD default))
        |>.filter (! ·.getId.isInternal)

      for constStx in names do
        let constName := constStx.getId
        let axioms ← collectAxioms constName

        -- 公理に依存していなければスルーする
        if axioms.isEmpty then
          return

        -- 選択原理に依存していれば警告を出す
        if axioms.contains `Classical.choice then
          Linter.logLint linter.detectClassical constStx
            m!"'{constName}' depends on 'Classical.choice'.\n\nAll axioms: {axioms.toList}\n"

  initialize addLinter detectClassicalLinter

end DetectClassical

すると、次のように使用できます。

import LeanByExample.Type.LinterLib

-- 選択原理を使用しているため警告が出る
/-
warning: 'prop_iff_neg_self₀' depends on 'Classical.choice'.

All axioms: [Classical.choice, propext, Quot.sound]

note: this linter can be disabled with `set_option linter.detectClassical false`
-/
theorem prop_iff_neg_self₀ (P : Prop) : ¬ (P ↔ ¬ P) := by
  intro h
  by_cases hp : P
  · have : ¬ P := by
      rwa [h] at hp
    contradiction
  · have : ¬ ¬ P := by
      rwa [h] at hp
    contradiction

-- 選択原理に依存しない証明には警告が出ない
#guard_msgs (warning) in
  theorem prop_iff_neg_self₁ (P : Prop) : ¬ (P ↔ ¬ P) := by
    intro h
    have hnp : ¬ P := by
      intro hp
      have hnp : ¬ P := by
        rwa [h] at hp
      contradiction
    have hp : P := by
      have : ¬ ¬ P := by
        rwa [h] at hnp
      contradiction
    contradiction