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 (← Linter.getLinterOptions) 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

-- 選択原理に依存しない証明には警告が出ない
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

---

1. この例は Lean 公式の Zulip の restricting axioms というトピックにおける、Damiano Testa さんの投稿を参考にしています。 ↩