🌟
Lean 言語の手続き的プログラムの検証フレームワークについて

2025/12/01に公開
この記事は、証明支援系 Advent Calendar 2025 の記事です。
https://adventar.org/calendars/11438

 前提知識この記事では「手続き的プログラムの形式検証」について説明するのですが、以下のことは既知とします。
モナドと、do 構文による手続き的なプログラムの記述
Lean 言語の基本的な文法と仕様
基本的なプログラム検証の知識
これらについてまじめに解説するとそれだけで一冊の本が書けてしまうレベルの分量になってしまうので、ご容赦ください。

 えっ、手続き的プログラムで形式検証を！？さて、この記事ではプログラム検証について説明するのですが、基本的に文献に載っているプログラム検証というのは、関数型スタイルで書かれたプログラムに対する検証だと思います。
たとえば、「リストを逆順にしたものを計算する関数を再帰的に定義してみて、その関数の末尾再帰バージョンを定義して、両者が等しいことを示しましょう」というような例が本では紹介されるんじゃないかなと思います。参考までにそれを Lean で書くとこういう感じになりますね。
variable {α : Type}

/-- リストを逆順にする関数 -/
def reverse (xs : List α) : List α :=
  match xs with
  | [] => []
  | x :: xs => (reverse xs) ++ [x]

/-- 末尾再帰バージョンのリスト逆順関数 -/
def reverseTR (xs : List α) : List α :=
  let rec go (ys : List α) (acc : List α) : List α :=
    match ys with
    | [] => acc
    | y :: ys => go ys (y :: acc)
  go xs []

/-- `acc` の部分を外に出すことができるという補題 -/
@[grind =]
theorem reverseTR.go_spec (xs acc : List α) :
    reverseTR.go xs acc = reverseTR.go xs [] ++ acc := by
  induction xs generalizing acc with grind [go]

/-- `reverseTR` は `reverse` と同じ関数等式を満たす(基底ケース) -/
@[simp, grind =]
theorem reverseTR_nil : reverseTR ([] : List α) = [] := by
  dsimp [reverseTR, reverseTR.go]

/-- `reverseTR` は `reverse` と同じ関数等式を満たす(再帰ケース) -/
@[grind =]
theorem reverseTR_cons (x : α) (xs : List α) :
    reverseTR (x :: xs) = reverseTR xs ++ [x] := by
  grind [reverseTR, reverseTR.go]

-- 両者が等しいことを証明
theorem reverse_eq_reverseTR (xs : List α) : reverse xs = reverseTR xs := by
  fun_induction reverse with grind
(Lean の知識を前提知識として仮定したので)まあこれは見慣れたものだと思います。[1]
一方で、手続き的に定義されたプログラムに対する形式検証というのは、あまり見慣れないのではないかと予想します。なぜかといえばおそらくその理由は単純で、難しいからだと思います。再帰的に定義された関数であれば「この場合はこう」みたいな関数等式が容易に得られて、それを手掛かりに帰納法を回して証明をするということができたわけなんですけど、手続き的に定義されているとそうはいかないことが多いです。Lean でも、基本的にプログラム検証と言えば関数型スタイルのコードに対するものでした。しばらく前までは。[2]
しかし、割と最近 Lean には手続き的に（つまりモナディックに）定義されたプログラムに対する形式検証を行うためのフレームワークが用意され、手続き型プログラムに対しても形式検証が可能になりつつあります。この記事ではこれについて紹介します。

 モナディックプログラムに対する検証フレームワークさてそのモナディックプログラムに対する検証フレームワークですが、習うより慣れよということで例をお見せしましょう。
先ほどご紹介した「リストを逆順にする関数」をまず再帰ではなく for ループを使って手続き的に定義してみます。Lean 4 の do 構文はとても強力なので、こんな感じに書くことができます。
/-- 手続き的に実装した、リストを逆順にする関数 -/
def reverseDo (xs : List α) : List α := Id.run do
  let mut acc : List α := []
  for x in xs do
    acc := x :: acc
  return acc

-- 動作確認
#guard reverseDo [1, 2, 3, 4] = [4, 3, 2, 1]
これに対する証明ですが、Lean 4 のフレームワークを使うと次のように書くことができます。(まだ正式リリースされていないものなので構文が将来変わる可能性があることをお断りしておきます)
-- mvcgen はまだ使用しないでというwarningを消す
set_option mvcgen.warning false

open Std.Do

/-- `reverse` は単一要素リストに適用しても変わらない -/
@[grind =, simp]
theorem reverse_singleton (x : α) : reverse [x] = [x] := by
  dsimp [reverse]

/-- `reverse` の、リストの末尾に要素を追加したときの挙動 -/
@[grind =]
theorem reverse_append_singleton (xs : List α) (x : α) : reverse (xs ++ [x]) = x :: reverse xs := by
  fun_induction reverse with grind [= reverse]

theorem reverseDo_eq_reverse (xs : List α) : reverseDo xs = reverse xs := by
  -- モナディックに実装されている（`Id.run do ...`）部分にフォーカスする
  generalize h : reverseDo xs = s
  apply Id.of_wp_run_eq h

  -- 検証条件の生成
  mvcgen invariants
  · ⇓⟨xs, acc⟩ => ⌜reverse xs.prefix = acc⌝ -- ループ中に変わらない「不変条件」を指定する
  with grind -- すべての枝に対して `grind` を適用する
相変わらず証明がgrindで爆速完了してしまうために、何が行われているのかわかりづらいと思うのですが、重要なことは「for ループに対して不変条件を指定している」ということです。ループを進めると当然いろいろものが書き変わっていくわけですが、その最中「ループを進めてもこの条件は変わらずに成り立ち続ける」という条件を指定してやることで、証明ができるようになります。
上記の例だと ⇓⟨xs, acc⟩ => ⌜reverse xs.prefix = acc⌝ という部分がループの不変条件を指定している個所で、xs という変数がループの進捗を管理しています。xs.prefix というのが「今までループで見てきた部分」を表していて、acc という変数はループの間書き変わっていくローカル可変変数です。
あとは、mvcgen というタクティクが重要ですね。これを使うことによって、手続き的プログラムの背景にあるモナドのことを気にせずに証明ができるようになっています。

 Further Readingこの記事はここで終わりです！駆け足解説ですみません！！
以下はさらに詳しく知りたい方への文献案内です。

Verifying imperative programs using mvcgen: このフレームワークを開発している人が書いた、公式のドキュメントです。（英語）この記事を執筆している2025年11月時点では世界でいちばん詳しい情報源なので、直接 Zulip で聞く以外ではここを読むのがいちばんです。

mvcgen を使って命令的プログラムの検証をする: 上記の記事の私が書いた日本語訳です。

Lean by Example: 私が書いている Lean のオンラインリファレンスです。全部日本語なので安心してください。mvcgen タクティクについても解説記事があります。

脚注
最近の Lean のリリース内容を追っていない人にとっては、証明が全部 grind で爆速完了しているのが気になるかもしれません。grind は v4.22.0 から正式リリースされた超強力証明自動化タクティクです。あまりに強力過ぎて、simp 以外のすべての証明自動化タクティクは過去のものになったといっても過言ではないレベルです。 ↩︎
既存の手続き的プログラムの検証ができるツールとしては、たとえば Dafny があります。Dafny にあまり詳しくないので詳細はわからないのですが、Dafny は Lean と比較すると「証明支援系として de Bruijn 基準を満たしておらず、多くの健全性に関するバグを有する」という大きな欠点が指摘されているようです。 ↩︎
前提知識

えっ、手続き的プログラムで形式検証を！？

モナディックプログラムに対する検証フレームワーク

Further Reading

Discussion
