Lean4でハノイの塔の最小手を証明しよう

はじめに

ハノイの塔というゲームを知っていますか? これは3本の棒と何枚かのサイズの異なる穴あき円盤があり、スタートの棒からゴールの棒へとルールを守りながら何手で円盤を全部移せるかを試すパズルゲームの一種です。(知らない人はWikiを見てください)

円盤が$n$枚のときの最小手が$2^n-1$となることが知られているのですが、これをLean4を使って証明してみましょう。^[1]　実際のコードも見てみたい方はbigchee/lean-hanoiからどうぞ。
この記事ではLean4の基本的な仕組みや構文については詳しく触れていないので、知らない方は雰囲気で読むか、公式レファレンス(Theorem Proving in Lean 4など)を参照してください。

ハノイの塔の定式化

まずはハノイの塔の設定とルールをLean4で表す必要があります。盤面を表す状態と、操作によるその間の遷移を定義していきます。移動元/先になる塔に相当する部分を「棒(rod)」、移動させる対象を「円盤(disk)」と呼びましょう。

状態の定義

$n$段のハノイの塔では、小さなサイズの方から円盤$0,1,\dots,n-1$があり、棒の位置A,B,Cがあります。それぞれの棒に入っている円盤の番号を上から列挙したリストを集めたものが状態を表します。
状態が有効であるためには、1. ディスクが増えたり減ったりしていないこと (disk_valid) と 2. 自分より大きな円盤を上に乗せていないこと (rod_valid) が必要です。これを踏まえ、状態を表現するためのデータ構造は次のように定義できます。

structure State (n : ℕ) where
  a : List ℕ
  b : List ℕ
  c : List ℕ
  disk_valid : (a ++ b ++ c).Perm (List.range n)
  rod_valid : Sorted (· ≤ ·) a ∧ Sorted (· ≤ ·) b ∧ Sorted (· ≤ ·) c

l1.Perm l2はl1を並び替えるとl2にできること、Sorted r lは順序rに従ってlの要素が並んでいることを表します。

遷移の定義

操作は移動元/先の棒の位置Posを指定できればOKです。別の棒へ移動するものを有効手と考えれば、素朴には遷移を表すデータ構造は次の通りです。

structure Move where
  s : Pos
  t : Pos
  valid : s ≠ t

一方で操作が可能であるための条件も考える必要があり、それは移動元の棒に円盤が少なくとも1つあることです。また、状態と操作を紐づけるための条件として、移動元の一番上の円盤と移動先の一番上の円盤が一致しなければなりません。これによって移動中に円盤が別のサイズに変わらないことを保証します。

def valid_move {n : ℕ} (qFrom : State n) (qTo : State n) : Prop :=
  ∃ m : Move, ∃ h1 : proj_ith_tower qFrom m.s ≠ [], ∃ h2 : proj_ith_tower qTo m.t ≠ [],
      ((proj_ith_tower qFrom m.s).head h1 = (proj_ith_tower qTo m.t).head h2)

proj_ith_tower q iは状態qにおける位置iの棒に相当するリストを取り出す関数です。

開始状態から終了状態への一連の操作を選び、有効な遷移列が作れれば、それがハノイの塔を解く解答手順になります。

最小手を構成しよう

最小手は帰納的に作ることができます。移動元の棒から$n-1$枚までの山を(移動元でも移動先でもない)中間の棒に移し、 $n$枚目を移動先に移した後、中間の棒からの残りの山を移動させます。これで$(2^{n-1} - 1) + 1 + (2^{n-1} - 1) = 2^n - 1$ 手です。
以下が最小手を返す関数ですが、adab2SListについては次のセクションで説明します。ここでは一段小さい場合の最小手prev,afterを再帰により求め、適切に変更したうえで連接することで新たな最小手を構成していることを確認してください。

def opt_play {n : ℕ} (i j : Pos) (h1 : i ≠ j) : SList n := by
  match n with
    | 0  => exact SList.mk [make_state0]
    | n'+ 1 =>
      let ⟨k, ⟨i_neq_k, j_neq_k⟩⟩ := rest_tower i j h1
      let prev : SList n' := opt_play i k i_neq_k
      let after : SList n'  := opt_play k j (Ne.symm j_neq_k)
      let adab_prev := adab2SList i 1 prev -- `[range n ,[],[]] -> [[n-1],range (n-1),[]]`
      let adab_after  := adab2SList j 1 after -- `[[],range (n-1),[n-1]] -> [[],[],range n]`
      exact SList.mk <| adab_prev.t ++ adab_after.t

状態列の長さが$2^n$(間の操作が$2^n-1$回)であることと、確かにこの手順が解になっていることを示すのが最終目標です。

theorem opt_play_is_minimum_ans {n : ℕ} (i j : Pos) (h1 : i ≠ j) :
    (List.length (opt_play i j h1 : SList n).t = 2^n) ∧ (is_solution i j (opt_play i j h1 : SList n)) := by sorry

帰納法の仮定を使うための下準備 (add_disk_at_bottom)

帰納法の仮定(IH)として使えるのは、$n-1$枚の山を$n-1$段の設定で動かす操作が$2^{n-1}-1$手で実現可能ということです。
これを$n$段の盤面で使うためには、$n-1$枚設定の状態を$n$枚設定の状態に拡張できる必要があります。一番下にサイズ$n-1$の円盤を足すことになりますが、これは既存のどの円盤よりもサイズが大きいのでこれによって状態の有効性(rod_valid)が崩されることはありません。

円盤の追加操作に関して保存される性質に関する補題とともに段数の拡張はDiskAddition.leanに定義されています。状態列の長さは変わらないことや、元の棒に一枚でも円盤があったら下に追加操作をしても一番上の円盤は変わらないことなど一見当たり前に成り立つことを改めて証明していく必要がありました。この追加操作を状態列全体に対して行うのが先ほど出てきたadab2SListの内容です。

メインの証明

状態列の長さが$2^n$になることは前半の状態列prevと後半の状態列afterがそれぞれIHより長さ$2^{n-1}$であり、これらを連接したのが$n$段の場合の最小手なので$2^{n-1} + 2^{n-1} = 2^n$より比較的簡単に示せます。

解であることの証明は、新しい状態列の最初と最後がそれぞれ開始状態と終了状態であること、および隣接する2状態の間に有効な遷移が存在することを確かめることになります。一番重いのはこの遷移の存在性valid_transitionの証明です。

def valid_transition (play : SList n ) :=
    ∀ m : ℕ, (hm : m < play.t.length - 1) → valid_move play.t[m] play.t[m+1]

今証明しないといけないのはplay.t = adab_prev.t ++ adab_after.tについてです。
リストl1 l2について、 m < l1.lengthならば(l1 ++ l2)[m] = l1[m]、 l1.length ≤ m < (l1 ++ l2).lengthならば(l1 ++ l2)[m] = l2[m - l1.length]であること(定理List.getElem_append)を使って3通りの場合分けが生じます。
m < prev.t.length - 1、 m ≥ prev.t.length の場合はそれぞれprev,after内の遷移があることがIHより従います。この遷移の有効性は下に一枚円盤を追加しても保たれます。
このような新しく仮定を導入して、その真偽により場合分けをしたいときは次のような構文が利用できます。

by_cases h : p(x)
case pos => -- 文脈にh : p(x) が追加される
case neg => -- 文脈にh : ¬p(x) が追加される

残るは m = prev.t.length - 1のケースです。この場合には二つの状態列をつなげた間に遷移があることを新しく確かめる必要があります。prevの終了状態/ afterの開始状態に円盤を追加した状態が問題になっており、棒Aから棒Cに移動させる場合にはそれぞれ次のような状態になっています。

play.t[m]   = { a:= [n-1], b:= range (n-1), c:= [], ...}
play.t[m+1] = { a:= [],    b:= range (n-1), c:= [n-1], ...}

ここまでくれば、valid_moveを示すにはAからCへの操作を選んだうえで、仕上げとして[n-1].head = [n-1].headを示せばよいだけになります。

おわりに

初めての写経じゃない定理証明でした。
最初の問題の定式化パートが一番大事だし、これが終わるとほとんど一本道。証明を省略したり、概略だけで終わらせることに対して少し寛容になれそうです。
有効な状態の条件が抜けていたり間違っていたりすると嘘解法が証明できてしまいます。形式的な証明があるからといって100%信用できるわけではなくて、スタート時に穴ができる可能性があるということに気がつきました。すさまじく時間泥棒なので実務には全く向かないですが、Leanを書くと示したいことが成り立つための過不足ない条件について考えられるので、学習のお供としては良さそうだと思います。
定式化をちゃんと自分でやることと、こういう条件からこの性質が成り立つという連鎖を踏まえて全体の方針を考えることが本質的に頭を使う部分のような気がします。あとは証明のゴールを達成したときの一瞬の快楽のためにチマチマ頑張りました。

おまけ: Leanで躓いたポイント

1. Deprecated List.get?

前提: l : List αについて、 いつでも使える安全なアクセス方法l[i]? : Option αとインデックスが存在する証拠(h : i < l.length)をつけてOption型を外したl[i]'h : αを得る方法がある.

問題点: l[i]?に関する論理式とインデックスが正しい証拠hがある。 l[i]? = some l[i]'h を用いて論理式を書き換えたいが、hを引数としてこの等式を得られる定理List.get?_eq_getがdeprecated(今後のバージョンで廃止されるので非推奨)指定されている.

解決方法: 内部的な仕組みが全くわからないという欠点はあるが、have : l[i]? = some l[i]'h := by simpとするとうまく行った。

2. 邪魔なパターンマッチ

問題点: ユーザが定義した変数hが⟨h_a, ⟨h_b, h_c⟩⟩という形をしているとする。h_a,h_b,h_cに相当する部分がコンテキスト内の中で使われているとすると、 処理系はこれらの変数名を知らないので以下のようなパターンマッチの形で変数名を導入する。

match h with
    | ⟨h_a, ⟨h_b, h_c⟩⟩ => body -- この中ではh_aなどを使える

しかしこのパターンマッチがあることによってbody部分の簡約ができず、証明が進められないという問題が生じた。

解決方法: コンテキストにhを分解した際の変数名が定義されていないことが問題なので、let ⟨h_a, ⟨h_b, h_c⟩⟩ := hとすればパターンの分岐が進む。^[2]

3. 複数変数の場合分けをまとめる

前提: 位置A,B,Cに関して似たような証明を書くことになるのでそれらを一つに集約したい。^[3] 対称性などを利用して証明を簡略化する方法もありそうだが方法がわからなかったので、愚直に全パターンに対して証明することにした。

問題点:　match ~ withだと同じ証明をコピペすることになり、コードが嵩張る。

解決方法: 複数変数i1,i2,...に関して全部の場合分けを展開して、 いくつかのtacticを順に試す構文(first | tac1 | tac2 | ...)でまとめる。

cases i1
repeat
    cases i2
    repeat
        -- 全部のパターンに通用する証明を書く

欠点としては、InfoViewで外側の変数が最初のパターンしか見れないのでうまく行かない場合はmatchで外側の変数を指定して証明が失敗しているポイントを探す必要がある。

脚注

1. 厳密にいえばここで示しているのは$2^n-1$手の解が存在性だけで、最小性は示していません。しかし、一番大きな円盤を動かすためにはそれより上の円盤をすべてどかす必要があることを考えると$2^n-1$手以上必要になることは最小手の実現方法を考えると直感的には明らかです。ちゃんとした証明は面倒そうだったので割愛しました。

2. しかしこのように変数名を置くと型エラー(同じはずだがパターンマッチの有無でおそらく単一化できない)が生じる場合があり、これについては直接的な原因も解決法もわからなかった

3. そもそも場合分けが必要なのは邪魔なパターンマッチの問題と関係しており、位置が具体化されないとパターンの分岐が進まずにゴールと形を一致させられないからでした