Linter

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

使用例

選択原理を証明の中で使用すると警告してくれるリンターを自作する例を紹介します。¹ まず以下のように記述したファイルを作成します。

-- Linter/DetectClassical.lean の内容

import Lean

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

open Lean Elab Command

/--
ある位置 `pos` 以降にソースコード内で登場するすべての宣言名を収集する
-/
private def getNamesFrom (pos : String.Pos.Raw) : CommandElabM (Array Syntax) := do
  let drs := declRangeExt.toPersistentEnvExtension.getState (asyncMode := .local) (← getEnv)
  let fm ← getFileMap
  let mut nms := #[]
  for (nm, rgs) in drs do
    if pos ≤ fm.ofPosition rgs.range.pos then
      let ofPos1 := fm.ofPosition rgs.selectionRange.pos
      let ofPos2 := fm.ofPosition rgs.selectionRange.endPos
      nms := nms.push (mkIdentFrom (.ofRange ⟨ofPos1, ofPos2⟩) nm)
  return nms

@[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`.\nAll axioms: {axioms.toList}"

initialize addLinter detectClassicalLinter

このファイルを読み込むと、次のように使用できます。

import LeanByExample.Type.Linter.DetectClassical

-- 選択原理を使用しているため警告が出る
/-
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

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

Lean by Example

Linter

使用例