Lean4で学ぶ「仕様と実装と証明」

Lean4で「仕様と実装と証明」をひとまとめに書く

記事の目的

この記事は、Lean4を使えば「仕様を定義する」「参照実装を書く」「実装が正しいと示す」の３点がすっきり書けるということを、フィボナッチ数列を題材に取って伝えることを目的としています。

対象者

• Lean4を触りはじめた方
• 証明支援系の雰囲気を小さなコードで掴みたい方

次のような方には内容が冗長かもしれません。

• Leanの型理論を体系的に深掘りしたい方（本記事は導入に絞っています）
• 高速実装や最適化手法を中心に学びたい方

要点（Lean４の強みとは）

• 命題Prop として仕様を書ける
• 普通の関数として実装を書ける
• 実装が仕様を満たすことを「証明」できる

「仕様・実装・証明」が全部ひとまとまりに書けることがLeanの強みです。

動作確認の前提

• Lean4が動く環境
• Main.lean を編集できること
• エディタは VSCode + Lean拡張があるとゴールや型を確認しやすいです

コード（仕様、実装、証明）

以下は仕様、実装、証明になります。次に細部の説明に入ります。

def FiboSpec (f : Nat → Nat) : Prop :=
  f 0 = 0 ∧
  f 1 = 1 ∧
  ∀ n, f (n + 2) = f (n + 1) + f n
  
def fibo : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fibo (n + 1) + fibo n

theorem fibo_spec : FiboSpec fibo := by
  constructor
  · rfl
  constructor
  · rfl
  · intro
    rfl

1. 仕様を定義する（Prop）

FiboSpec は、フィボナッチ関数なら満たすべき条件を定義したものです。
この関数は、自然数の関数 f : Nat → Nat を受け取り、「fがフィボナッチの条件を満たす」という命題を返します。数学・論理学でいう述語に似ています。

def FiboSpec (f : Nat → Nat) : Prop :=
  f 0 = 0 ∧
  f 1 = 1 ∧
  ∀ n, f (n + 2) = f (n + 1) + f n

フィボナッチとして満たすべきは、次の3条件です。

1. f 0 = 0　
2. f 1 = 1
3. 任意の n に対して f (n + 2) = f (n + 1) + f n

記号の意味は次のとおりです。

• Prop は「命題の型」を表します
• ∧ は「かつ」を表す連言です
• ∀ は「任意の」を表す全称量化子です

自然言語に近い感触で、Lean が読める命題を書けるのがポイントです。

2. 実装を書く（Nat → Nat）

次に仕様を満たす関数の候補として、 fibo を定義します。

def fibo : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fibo (n + 1) + fibo n

これは引数 Nat に対するパターンマッチです。

• 入力が 0 なら 0
• 入力が 1 なら 1
• 入力が n + 2 の形なら、前 2 項の和

最後の行が、フィボナッチの再帰式そのものに対応しています。

重要なのは、Lean は再帰関数を無条件には受理しないという点です。
再帰呼び出しのたびに、引数がきちんと小さくなっていき、最終的には入力が 0, 1の場合まで帰ってきて、定義が停止すると判断できる場合にだけ受理します。

この fibo が n + 2 の場合に再帰呼び出しするのは fibo (n + 1) と fibo n です。
元の引数 n + 2 より小さい引数が渡されているので、Lean はこの定義を構造的再帰として受理します。

3. 実装が仕様を満たすことを証明する

実装した fibo が、先ほどの FiboSpec を満たすことを示します。

theorem fibo_spec : FiboSpec fibo := by
  constructor
  · rfl
  constructor
  · rfl
  · intro n
    rfl

Lean で「証明する」とは何か

Lean では、命題は型として扱われ、証明はその型の項として扱われます。このため、命題を証明するとは、その命題の項を構成することを意味します。
ここでは、 fibo がフィボナッチの条件を満たすことを証明したいので、FiboSpec fibo を証明することが目標になります。言い換えると、FiboSpec fibo という型の項を 1 つ構成することが目標になります。実際、

theorem fibo_spec : FiboSpec fibo

は、 FiboSpec fibo という型の項が存在することを主張する定理です。

紙の数学では「命題 A から命題 B を導く」と表現しがちですが、Lean では

• 証明済みの命題はすでに項として手元にある
• 新しい証明は、それらの項を組み合わせて構成する

という見方が基本になります。

証明のゴールはどんな形か

FiboSpec fibo を展開すると、ゴールは次の形をしています。

fibo 0 = 0 ∧ fibo 1 = 1 ∧ ∀ n, fibo (n + 2) = fibo (n + 1) + fibo n

∧ は右結合なので、次と同じです。

fibo 0 = 0 ∧ (fibo 1 = 1 ∧ ∀ n, fibo (n + 2) = fibo (n + 1) + fibo n)

そのため、constructor を 2 回使うと 3 つの条件を順に取り出せます。

各タクティクがしていること

• 1 回目の constructor は、連言 A ∧ B の証明を作るために、ゴールを A と B に分けます
• 2 回目の constructor は、残った fibo 1 = 1 ∧ ∀ n, ... をさらに 2 つに分けます
• intro n は、ゴール ∀ n, P n を「任意の n を 1 つ取ったときの P n」に変えます

ここで重要なのは、これらがそれぞれ証明項の形に対応していることです。

• A ∧ B の証明は、「A の証明」と「B の証明」の組です
• ∀ n, P n の証明は、「任意の n を受け取って P n の証明を返す関数」です

Lean のタクティクは、この証明項を対話的に組み立てるための補助と考えると理解しやすいです。

rfl は何を証明しているのか

rfl は reflexivity の略で、左右が 定義上同じ ときに使える証明です。
「見た目がたまたま似ている」ではなく、定義を展開して簡約すると本当に同じ式になる、という意味です。

この例では、

• fibo 0 = 0 は fibo の第 1 分岐を使えば 0 = 0
• fibo 1 = 1 は第 2 分岐を使えば 1 = 1
• fibo (n + 2) = fibo (n + 1) + fibo n は第 3 分岐を使えば左右がそのまま一致するため

どのゴールも rfl で閉じます。

この証明が短い理由は、実装 fibo が仕様とほぼ同じ形をしているからです。もしループや末尾再帰で実装すると、同じ仕様につなぐ補題を別途証明する必要が出てくることが多いです。

4. 同じ証明を「値」として直接書く

タクティクを使わず、証明項そのものをダイレクトに書くこともできます。

example : FiboSpec fibo :=
  ⟨rfl, rfl, fun n => rfl⟩

これは次のように読むと分かりやすいです。

• 最初の rfl が fibo 0 = 0 の証明
• 2 つ目の rfl が fibo 1 = 1 の証明
• fun n => rfl が ∀ n, fibo (n + 2) = fibo (n + 1) + fibo n の証明

∀ の証明は関数 fun n => rfl になっていることに注意します。

同じことをコンストラクタ名を明示して書くと、次の形になります。

example : FiboSpec fibo :=
  And.intro rfl (And.intro rfl (fun n => rfl))

⟨..., ..., ...⟩ は読みやすい省略記法で、And.intro はそれを明示的に書いたものです。タクティクで対話的に書いても、項を直接書いても、見た目が違うだけで本質的には同じ証明を表しています。

確認手順

lake new fibo-spec
cd fibo-spec

Main.lean をこの記事のコードに置き換えて、次を実行します。

lake env lean Main.lean

エラーが出なければ、定義も証明も通っています。

VSCode + Lean 拡張を使っている場合は、カーソルを各行に置くと、その時点のゴールが確認できます。
constructor や intro がゴールをどう変形するのかを見ると、証明の流れを理解しやすくなります。

この最小例から分かること

• 仕様は機械が読める命題として書ける
• 実装は普通の関数定義として書ける
• 証明では、その実装が仕様を満たすことを示す証明項を構成する

特に重要なのは、この例は「テストケースが通った」のではなく、「すべての入力に対してこの性質が成り立つ」ことを命題として明示しているという点です。

まとめ

今回はフィボナッチ数列を題材に、Lean4 で

• 仕様を Prop として書く
• 実装を関数として書く
• その実装が仕様を満たすことを証明する

ことを取り扱いました。

小さな例ですが、Lean の本質である「命題を型として扱い、証明をその項として構成する」という考え方がそのまま入っています。小さな例で繰り返しこの感覚を掴むようにすると、より大きな仕様や証明にもアプローチしやすくなると思われます。

PS

実を言うと、実務のコードではもっと複雑な仕様や補題が必要になり、人力では証明方針がすぐに立たないということも往々にしてあります。その場合であっても、仕様・実装・証明が 1 つの言語で書けるという基本構図は一貫しています。Leanの扱いやすい範囲は比較的はっきりしていて、コアロジック、不変条件、データ構造、変換処理のような数学的に書きやすい箇所です。外部環境や副作用のモデル化になると急に重くなります。また、可変状態や破壊的変更を伴うループでは難易度が上がりやすいです。今回の例みたいに関数型言語らしく再帰で書いたのは妥協ではなく、その方が仕様に沿って証明が書きやすいためです。もちろん実務では再帰でなくループで書くことが多いと思うので、再帰バージョンは参照実装として、本番の実装とは分けて考えるという整理が良い場面もあります。このようにLeanが効果的に使える範囲を見極めることも大事かと思います。