🍫
クリスマスは Lean で毒チョコゲーム Chomp を楽しもう
こちらは、証明支援系 Advent Calendar 2025 16日目の記事です。
ですが、本記事では証明のあれこれは取り扱いません。
汎用プログラミング言語 Lean
Lean 言語は、(なぜか数学の定理の証明も記述できてしまう) 汎用の関数型プログラミング言語です。なので、普通のプログラムも書くことができます。モナドやその Do 記法も導入されており、手続き型プログラミング言語のようにも記述することができます。
この記事では、Lean で、毒チョコゲーム (Chomp) をコマンドラインゲームとして実装し、ゲームを楽しみます。
毒チョコゲーム Chomp
毒チョコゲームは二人で楽しめる、毒の入ったチョコピースを相手に押し付けあう素敵なゲームです。
詳しいルールは YouTube チャンネル「えびまラボ」の動画「毒チョコゲームの必勝法〖ゆっくり解説〗」をご覧ください。
Chomp のプログラム (LLMで生成)
今日日、これぐらいのプログラムなら ChatGPT や Gemini などの生成 AI が作ってくれます。
以下のコードは Gemini に依頼して作成したものです。 2 か所ほど文法的な誤り(リストの要素取得方法)があったのでその部分だけを修正しています。
ChompGame.lean
/-- ゲームの設定: 幅と高さ -/
def width : Nat := 5
def height : Nat := 4
/-- 盤面の状態
各列に残っているチョコレートの高さ（個数）のリスト -/
abbrev Board := List Nat
/-- 初期盤面の作成 -/
def initBoard : Board := List.replicate width height
/-- 盤面の表示 -/
def printBoard (b : Board) : IO Unit := do
IO.println " 0 1 2 3 4 (列)"
IO.println " -----------"
for r in [0:height] do
let mut line := s!"{r}| "
for c in [0:width] do
-- その列の高さが現在の行 r より大きければチョコがある
if let some h := b[c]? then
if r < h then
line := line ++ "O "
else
line := line ++ ". "
else
line := line ++ " "
IO.println line
IO.println ""
/-- 入力解析 -/
def parseInput (s : String) : Option (Nat × Nat) := do
let parts := s.trim.splitOn " "
match parts with
| [rStr, cStr] =>
let r ← rStr.toNat?
let c ← cStr.toNat?
some (r, c)
| _ => none
/-- 移動ロジック
指定された (r, c) より右下のチョコを全て削除します。
リストを先頭から見ていき、指定列 c に到達するまでは何もしません。
指定列 c 以降は高さを r で制限 (min) します。 -/
def makeMove (b : Board) (r c : Nat) : Board :=
match b with
| [] => []
| h :: t =>
if c > 0 then
-- 指定列より左側なので、高さ h はそのまま。次の列へ (cを1減らす)
h :: makeMove t r (c - 1)
else
-- 指定列以降なので、高さは min h r になる。cは0のまま維持して右側全てに適用
min h r :: makeMove t r 0
/-- メインゲームループ -/
partial def gameLoop (b : Board) (player : Nat) : IO Unit := do
printBoard b
let playerNum := player + 1
IO.println s!"プレイヤー {playerNum} の番です (行 列 を入力, 例: 1 2): "
let stdin ← IO.getStdin
let input ← stdin.getLine
match parseInput input with
| some (r, c) =>
let colHeight := b[c]!
if c >= width || r >= height then
IO.println "エラー: 範囲外です。もう一度入力してください。"
gameLoop b player
else if r >= colHeight then
IO.println "エラー: そこにはもうチョコがありません。"
gameLoop b player
else if r == 0 && c == 0 then
IO.println s!"\n!!! 毒(0,0)を食べました！ プレイヤー {playerNum} の負けです !!!"
else
let newBoard := makeMove b r c
gameLoop newBoard (1 - player)
| none =>
IO.println "エラー: '行 列' の形式で数字を入力してください。"
gameLoop b player
/-- エントリーポイント -/
def main : IO Unit := do
IO.println "=== CHOMP ゲームへようこそ ==="
IO.println "左上の (0, 0) を食べると負けです。"
IO.println "右下の領域を消していきます。\n"
gameLoop initBoard 0
プレイ方法
-
Leanのインストールがまだの人はインストールしましょう。
https://lean-lang.org/install/ -
上記の Lean のソースコードを
ChompGame.leanとして保存します。 -
lean コマンドで実行します。
lean --run ChompGame.lean
実行例
$ lean --run ChompGame.lean
=== CHOMP ゲームへようこそ ===
左上の (0, 0) を食べると負けです。
右下の領域を消していきます。
0 1 2 3 4 (列)
-----------
0| O O O O O
1| O O O O O
2| O O O O O
3| O O O O O
プレイヤー 1 の番です (行 列 を入力, 例: 1 2):
1 2
0 1 2 3 4 (列)
-----------
0| O O O O O
1| O O . . .
2| O O . . .
3| O O . . .
プレイヤー 2 の番です (行 列 を入力, 例: 1 2):
2 0
0 1 2 3 4 (列)
-----------
0| O O O O O
1| O O . . .
2| . . . . .
3| . . . . .
プレイヤー 1 の番です (行 列 を入力, 例: 1 2):
0 1
0 1 2 3 4 (列)
-----------
0| O . . . .
1| O . . . .
2| . . . . .
3| . . . . .
プレイヤー 2 の番です (行 列 を入力, 例: 1 2):
1 0
0 1 2 3 4 (列)
-----------
0| O . . . .
1| . . . . .
2| . . . . .
3| . . . . .
プレイヤー 1 の番です (行 列 を入力, 例: 1 2):
0 0
!!! 毒(0,0)を食べました！ プレイヤー 1 の負けです !!!
Chomp は先手必勝？
ところで、「えびまラボ」の動画によると、この毒チョコゲーム Chomp は先手必勝のようです。せっかくなので、定理証明支援系 である Lean でこのことを証明したいと思います。
証明は後日、記事にする予定です。しばらくお待ちください。
(追記) 証明しました。
Discussion