Zenn
📝

Lean 4のメタプログラミングで数独チェッカーを作った

に公開
editor
型
メタプログラミング
数独
lean4
tech

TypeScriptとScalaで型レベルプログラミングを使ってエディタ上で数独をプレイできるようにするという遊びを見かけました。

https://x.com/jalva_dev/status/1832282610233675829
https://xuwei-k.hatenablog.com/entry/2024/09/07/184403

Leanでもやってみた

Leanなら割と簡単に、普通の(メタ)プログラミングでいけそうだなと思ったのでやってみました。
コードはgistにありますが、↓のリンクからWeb上で実際に遊べます。
https://live.lean-lang.org/#url=https%3A%2F%2Fgist.githubusercontent.com%2Fspinylobster%2Fda6b5a818f4f757cf12e270be85aa42f%2Fraw%2Fc088b5a227c6d932ef41f315feac4ef2c98fb01d%2FSudokuChecker.lean

数独をプレイするには、エディタの一番下の行に移動してこんな感じで問題を入力します。
ハイフン(-)の部分を自分で埋めていくと、重複があるとエラーになり、全部埋まると褒めてくれます。

#sudoku
  - , 5 , - ,   2 , - , - ,   4 , - , 6,
  - , 6 , 4 ,   1 , - , - ,   - , 7 , 5,
  - , 2 , 8 ,   - , 6 , 5 ,   1 , - , 3,

  8 , - , 6 ,   - , 7 , 2 ,   - , - , -,
  - , - , 3 ,   8 , - , 1 ,   5 , - , -,
  - , 1 , 7 ,   - , 4 , - ,   - , 2 , 8,

  - , - , 5 ,   9 , - , - ,   - , 4 , 1,
  4 , - , - ,   - , 1 , 3 ,   - , - , 9,
  9 , 8 , - ,   - , 5 , - ,   - , 3 , -
end

まるで最初からLeanに数独をプレイするための機能があったかのように見えて楽しくないですか？

コードの前半は数独のルールを素直に書いていて、後半にメタプロで「エディタ上でプレイする」部分を実装しています。
元ネタとは根本的に違うことをやっていますが、まあエディタ上で数独ができるという点では同じなので見逃してください。
(「型チェックが通るなら数独として間違いがないことが保証される」という仕組みも簡単に作れると思うので、あとで追記します)

差別化ポイントとして、並の言語では真似できなさそうな、エラーメッセージで重複がどこにあるか指摘したり、全部解けた時にお祝いする機能もあったりします。

「依存型があって数学の証明さえ書ける」というのがLeanのウリですが、数学とか関係なく自分の思いついた構文や機能を自由に追加できるというのもまた大きな魅力だったりします。

自分がインプットするばっかりで全然布教のための記事を書けてないんですが、非関数型言語ユーザのためのLean入門コンテンツもそのうち作りたい…

日本語のLeanコミュニティの紹介

  • Discord: LEAN勉強会
    • Leanの教材やその他の題材をテーマにしたゼミが日夜開催されています
    • 「この教材を理解したいけど一人では途中で詰まってしまう」という時はここに書いてもらえれば一緒に勉強できます
    • 初心者歓迎です
  • Discord: LEAN JA
    • 勉強会に限らない、Leanの話題全般のための場所です

追記(2025/8/3)

めっちゃ久しぶりにZennにログインしました。
「Leanのバージョン上がって壊れてそうだな〜」と思ってたら案の定壊れてたので直しました。

あと、↓のやつも(意味わからんくらい遅いけど)一応やってたので追記しておきます。

「型チェックが通るなら数独として間違いがないことが保証される」という仕組みも簡単に作れると思うので、あとで追記します

https://live.lean-lang.org/#url=https%3A%2F%2Fgist.githubusercontent.com%2Fspinylobster%2F101e22ec395a976bbd521c8d26b4f756%2Fraw%2Fc115f0e564bf95af27b94b916edc9790f5cffc56%2FSudoku2.lean
元のgistは https://gist.github.com/spinylobster/101e22ec395a976bbd521c8d26b4f756 です。

example : AllCells.Solve [sudoku|
  - , 5 , - ,   2 , - , - ,   4 , - , 6,
  - , 6 , 4 ,   1 , - , - ,   - , 7 , 5,
  - , 2 , 8 ,   - , 6 , 5 ,   1 , - , 3,

  8 , - , 6 ,   - , 7 , 2 ,   - , - , -,
  - , - , 3 ,   8 , - , 1 ,   5 , - , -,
  - , 1 , 7 ,   - , 4 , - ,   - , 2 , 8,

  - , - , 5 ,   9 , - , - ,   - , 4 , 1,
  4 , - , - ,   - , 1 , 3 ,   - , - , 9,
  9 , 8 , - ,   - , 5 , - ,   - , 3 , -
] := by
  simp
  place (4,8), (9,3), (1,1) <= 1
  ...

みたいな感じで、解いていく過程が証明の過程として残るようになってるのがお気に入りです。マジで意味わからんくらい遅いけど(二回目)

この次はまともなコードを書いて速くするのと、InfoView上の数独の状態表示をUserWidgetを使ってReactで実装できたらいいですね。

Discussion