lean4-practice

name: lean4-practice description: Lean 4 code generation best practices. Use when writing Lean 4 code to avoid common AI mistakes with syntax, types, tactics, and project configuration.

Lean 4 プラクティスガイド

AI が Lean 4 コードを生成する際のベストプラクティス。

ガイドライン

プロジェクト管理には Lake を使う

lake new myproject     # 新規プロジェクト作成
lake build             # ビルド
lake env printPaths    # 検索パス表示

lakefile の設定は reference/configuration.md を参照。

LSP と #check / #eval で探索する

#check Nat.add         -- 型シグネチャを表示
#eval 2 + 3            -- 式を評価
#print Nat.add         -- 定義を表示
#check @List.map       -- 暗黙引数を含む型を表示

ツール詳細は reference/ide.md を参照。

よくある落とし穴

• インデントが意味を持つ - do, where, match, if でインデントが重要
• 定義には := を使う（= ではない） - def f (x : Nat) : Nat := x + 1
• by でタクティックモードに入る - theorem t : P := by exact h（by なしは不可）
• 宇宙多相 - Type は Type 0、Type 1 は Type 0 を含む
• 依存型が至る所にある - 関数型が引数の値に依存できる
• sorry は未完成の穴 - コンパイルは通るが証明未完了（本番コードに残さない）
• #eval で Prop は評価できない - #check か Decidable インスタンスを使う
• 暗黙引数 {} とインスタンス [] - [] は型クラス解決を起動する
• match には with が必要 - match x with | ...（with なしはエラー）
• if には then/else が両方必要 - else なしの if-then は不可
• 停止性チェック - 再帰関数は停止が証明可能でなければならない。必要に応じ decreasing_by や termination_by を使う

AI がよく間違える構文

定義の構文

-- NG: `:=` がない
def double (n : Nat) : Nat
  n + n

-- OK
def double (n : Nat) : Nat :=
  n + n

-- OK: 等式コンパイラスタイル（パターンマッチ）
def double : Nat -> Nat
  | n => n + n

パターンマッチ

-- NG: `with` がない
def isZero (n : Nat) : Bool :=
  match n
  | 0 => true
  | _ => false

-- OK
def isZero (n : Nat) : Bool :=
  match n with
  | 0 => true
  | _ => false

do 記法

-- NG: `do` キーワードがない
def main : IO Unit :=
  IO.println "hello"
  IO.println "world"

-- OK
def main : IO Unit := do
  IO.println "hello"
  IO.println "world"

theorem と def

-- NG: 命題の証明に `def` を使っている
def myTheorem : 1 + 1 = 2 := by rfl

-- OK: 命題には `theorem` を使う（実行時に消去される）
theorem myTheorem : 1 + 1 = 2 := by rfl

構造体の構文

-- NG: 他言語風の `{` `}`
structure Point {
  x : Float
  y : Float
}

-- OK: `where` 構文を使う
structure Point where
  x : Float
  y : Float

do 内の let 束縛

-- NG: モナディックバインドに `let x = ...` を使っている
def readAndPrint : IO Unit := do
  let line = IO.getStdIn >>= fun stdin => stdin.getLine

-- OK: モナディックバインドには `<-` を使う
def readAndPrint : IO Unit := do
  let stdin <- IO.getStdin
  let line <- stdin.getLine
  IO.println line

クイックリファレンス

追加リファレンス

各トピックの詳細は以下のファイルを参照: