Lean4: コードの読み方スニペット集

※随時更新ページ（2025/07/16 17:01 現在）

１、２行のコードに凝縮された情報量が多い Lean 🧠 脳内展開が難しい。

記号

記号の読み方を最初に身に着けなければ、非効率だったということを知る。
こういうところが、にわか数学者の弱い所。だけど、私は別に急いでない。
なにかの縁で知り得た時に知ることが脳内の輝きが増し、定着しやすい！
（※個人差、趣味嗜好によって異なります）（まえ置きは良い→本題へ）

キッカケ記事

論理学

計算論理学は、小学生の頃からやってるから、めちゃくちゃ解るのだけど、証明や論文なんて大学行ってない私には無縁！必要ない。よって知りもしないし使いもしない。最近、触れる機会が出てきたので関わることになるが、論理学という分野の一部が、計算機論理だって事に気づいたのが、今さら。

コンピュータは計算してるんではなく、常に論理で真偽をビットで表現しているだけに過ぎない。なので、計算という操作は真偽ビットの操作と言える。ならば、証明は演算。と逆に言い換えられる。のであろう。✍️

証明は演算を証明する。は、面白そうなテーマだけど🦴骨が折れそうだ😂

記号の解説サイト（未読✍️）

日本語訳

Lean で使える記号の例

（※ここに Lean ソースコードに出てくる記号例を列挙していく✍️）

記号 "$" ブラケットの省略と二重適用

/-- 二重適用を行う関数の例です。
- Q. 二重適用とは？
- A. 与えられた関数 `f` を二回適用することです。
  - 例えば、`f` が `x + x` の場合、`square 5 f` は `f (f 5)` を計算します。
  - この例では、`square` 関数は整数 `x` に対して関数 `f` を二回適用します。
  - `square 5 $ λ x => x + x` の場合、最初に `5` に `f` を適用し、次にその結果に再度 `f` を適用します。
-/
def square (x : Nat) (f : Nat → Nat) := f (f x)
-- $ の例
#eval square 5 $ λ x => x + x  -- 20 が出力されれば成功
-- $ は、ブラケットを省略して関数を適用する方法です。
-- ここでは、`square` 関数に `5` と `λ x => x + x` を渡しています。
-- `square 5 $ λ x => x + x` は `square 5 (λ x => x + x)` と同じ意味です。

二重適用を行う関数の例です。

• Q. 二重適用とは？

• A. 与えられた関数 $${f}$$ を二回適用することです。

  • 例えば$${f}$$ が $${x + x}$$ の場合 `square 5 f` は $${f (f(5))}$$ を計算します。

  • この例では `square` 関数は整数 $${x}$$ に対して関数 $${f}$$ を二回適用します。

  • `square 5 $ λ x => x + x` の場合、最初に $${5}$$ に $${f}$$ を適用し、次にその結果に再度 $${f}$$ を適用します。

• つまり、展開した式は、

• `λ x => x + x (λ x => x + x 5)` となり、最終的に `20` になります。
  ※右のカッコから先に評価適用、その結果が次のラムダ式の引数となる。

どうして？と、まだ解らない人へ

• 1回目の適用で `5 + 5 = 10` になり、

• 2回目の適用で `10 + 10 = 20` になるからです。

このように、二重適用は関数を連続して適用することで、結果を変化させる手法です。

$ 記号

$ は、ブラケットを省略して関数を適用する方法です。
ここでは `square` 関数に $${5}$$ と $${λ x.x + x}$$ を渡しています。
`square 5 $ λ x => x + x` は `square 5 (λ x => x + x)` と同じ意味です。

コメント行

Lean には複数のコメントの書き方がある。
それぞれには目的別の役割があるので、適当に使うわけにも行かない。

うん、Lean（特に Lean 4）にはいくつかのコメント記法があって、目的によって使い分けるようになってるよ。以下に 全種類 をまとめるね：

🔹 1. 行コメント（Line comment）

-- これは1行コメント

• `--` のあとに書く。

• その行の終わりまでコメントになる。

• `--` の直後にスペースがあってもなくてもOK。

• よくコード中のメモや、短い補足説明に使う。

🔹 2. ブロックコメント（Block comment）

/- 
これは複数行にわたる
ブロックコメントです。
-/

• `/-` で始まり `-/` で終わる。

• 中に改行を含んでも大丈夫。

• ネスト（入れ子）できるのが特徴！

/- 外部
  /- 内部 -/
外部続き -/

🔹 3. ドキュメントコメント（Doc comment）

定義・定理などに説明をつけたいときはこれ。

/-- この関数は1を足すよ -/
def inc (n : ℕ) := n + 1

• `/-` にハイフンが 2本： `/-- ... -/`

• 直後のコマンド（定義や定理など）に紐づく doc-string になる。

• Markdown や LaTeX 風数式（`$x^2$`）が使える。

• mathlib ではかなり重要。

🔹 4. モジュールドキュメント（Module doc comment）

ファイルの先頭に書く特別な doc-comment。

/-!
# セクションタイトル

このファイルは〜を定義します。
-/

• `/-! ... -/`（ハイフン1本、ビックリマークつき）

• `module doc string` として扱われる。

• ファイル全体に関する説明を書くときに使う。

• これも Markdown OK。

🔹 5. 行ベースのモジュールドキュメント（ややマイナー）

--!
このファイルは〜を扱うよ

• `--!` は `/-! -/` のショート版（1行用）。

• あんまり見かけないけど一応ある。

🎯 まとめ表

| 記法       | 目的           | 特徴           |
| -------- | ------------ | ------------ |
| `--`     | 1行コメント       | シンプル、コード中の補足 |
| `/- -/`  | ブロックコメント     | 複数行、ネストOK    |
| `/-- -/` | doc-comment  | 定義・定理の説明     |
| `/-! -/` | モジュールdoc     | ファイル全体の説明    |
| `--!`    | モジュールdoc（1行） | ややマイナー       |

もし「doc-comment で定理の表示変わるの？」とか「VS Code 上でどう見えるの？」みたいな話も興味あったら続けて説明できるよ〜！

2025/07/16 17:13　追加：記号
2025/07/13 23:49　追加：コメント記法
2025/07/13 12:01　新規

D.