---
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 を使う

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

lakefile の設定は [reference/configuration.md](reference/configuration.md) を参照。

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

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

ツール詳細は [reference/ide.md](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 がよく間違える構文

### 定義の構文

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

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

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

### パターンマッチ

```lean
-- 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 記法

```lean
-- 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

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

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

### 構造体の構文

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

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

### do 内の let 束縛

```lean
-- 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
```

## クイックリファレンス

| 項目 | コマンド / 構文 | 説明 |
|------|----------------|------|
| ビルド | `lake build` | プロジェクトをビルド |
| 実行 | `lake env lean --run Main.lean` | main を実行 |
| REPL | `lake env lean` | 対話モード |
| 型チェック | `#check expr` | 型を表示 |
| 評価 | `#eval expr` | 式を評価 |
| 定義表示 | `#print name` | 定義を表示 |
| 検索 | `exact?` / `apply?` | タクティック・補題を検索 |
| ドキュメント | https://leanprover-community.github.io/mathlib4_docs/ | Mathlib ドキュメント |

## 追加リファレンス

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

| ファイル | 内容 |
|---------|------|
| [reference/language.md](reference/language.md) | 型、構文、パターンマッチ、型クラス、モナド、do 記法 |
| [reference/tactics.md](reference/tactics.md) | タクティック: intro, apply, exact, simp, omega, rw, induction 等 |
| [reference/stdlib.md](reference/stdlib.md) | 標準ライブラリ、Batteries、Mathlib 基礎、よく使う型 |
| [reference/configuration.md](reference/configuration.md) | lakefile.toml, lean-toolchain, 依存関係、プロジェクト構成 |
| [reference/testing.md](reference/testing.md) | #eval, #check, example, テストパターン、証明デバッグ |
| [reference/ide.md](reference/ide.md) | LSP 機能、Lake コマンド、エディタ連携 |