はじめに
「定理証明支援系」という言葉を、聞いたことはありますでしょうか。
数学の定理や、プログラムの正しさを、コンピュータに検査させる仕組みのことです。
証明を書くための専用の言語と、それを読み取って検査する処理系が、一組になっています。
人間が証明を書き、それをソフトウェアが一段ずつ確かめる。
論理の飛躍があれば、そこで止まります。
「この段階は、前の段階から導かれません」と教えてくれるのです。
Isabelle、Lean 4、Rocq（旧名 Coq）、Agda、Mizar などが、そう呼ばれるものです。
何に使われているのか。 ２つの領域があります。
一つは、数学です。
2005年、ケプラー予想という400年来の難問が、この方法で検証されました。
近年では、フェルマーの最終定理の証明 を、丸ごとコードに書き写す計画も進んでいます。
もう一つは、ソフトウェアの検証です。
OSの中核部分 や、クラウド基盤の重要な部分 が、この方法で 検証 された事例があります。
この記事について
本記事は、全２回の連載記事の前編（１本目）です。
本記事では、定理証明支援系における２つの証明の書き方 のうち、まずタクティクスタイルを詳しく見ます。
そのうえで、もう一つの書き方である 宣言的スタイル の入口までをご紹介します。
続編（後編）の記事 では、宣言的スタイルを主題 として、６つの言語のコードを並べて比較し、その30年の歴史と、AI が証明を書く時代における意味までを扱います。
想定読者
- Python は書けるが、定理証明支援系は学んだことがないという方
- 「コードなのに、そのまま数学の証明文として読める」という話に関心のある方
- AIが証明を書く時代 に、人間が何を読み、何を判断すべきかを考えたい方
論理学や関数型プログラミングの予備知識は、仮定しません。
数学の予備知識も、仮定しません。
専門用語は、登場するたびに日常の言葉で説明します。
筆者の過去記事を読んでいることも、前提としません。
この記事を読む価値
-
定理証明支援系とは何をするものなのかを、Jupyter Notebook での作業に喩えて理解できる
-
タクティクとは何か、そしてその語源が分かる
-
Rocq、Isabelle、Lean 4、Agda、Mizar という５つの言語で、実際の入力と処理系の応答を比べられる
-
なぜタクティクで書かれた証明は読みにくいのかを、実際のコードを見ながら確かめられる
-
宣言的スタイルとは何か、そしてその本質が「語彙」ではなく「論理構造をコードに残すこと」にあると分かる
-
カントールの定理を例に、２つの書き方の差を目で見て比べられる
- 続編を読む準備が整う。 続編では、６つの言語のコード比較と、宣言的スタイルの30年の歴史を扱います
TL;DR
（この節の専門用語は、いずれも本文で説明します）
-
定理証明支援系とは、数学の定理やプログラムの正しさを、コンピュータに検査させる仕組みである。証明を書く専用の言語と、それを検査する処理系が一組になっている
-
その証明の書き方には、対照的な２つのスタイルがある。 タクティクスタイルと宣言的スタイルである
-
タクティクスタイルは、処理系と対話しながら書く。 「場合分けせよ」と指示を出すと、処理系が「では次はこれを証明してください」と応答する。Jupyter Notebook でセルを実行し、出力を見ながら次を書くのに似ている
-
この書き方には、証明の道筋が分かっていなくても試しながら進められるという大きな利点がある
-
しかし、書き上がったファイルには、処理系からの応答が残らない。 指示だけが並んだコードからは、何を証明しようとしていたのかが読み取れない
-
一括で実行しても、出力されるのはバイナリファイルである。 対話中に画面へ表示されていた証明の状態は、そこには含まれない
-
この読みにくさは、定理証明支援系を作った人たち自身が指摘してきた。 Isabelle を公開したポールソンは「その形式的な証明は読めない」と書いている
-
もう一つの書き方が、宣言的スタイルである。「仮定する」「よって」「示す」といった語を並べ、論証の筋道を文章として書く
-
証明の途中で何を仮定し、何を導き、次に何を示すのかという論理構造 を、コードそのものに明示する ことができる
-
２つのスタイルに優劣はない。 タクティクスタイルは証明を探す作業に向き、宣言的スタイルは完成した論証を第３者が読む場面に向く
-
Agda と Mizar は、事情が違う。 Agda は「穴」を埋めていく独自の方式を採り、Mizar には対話的な仕組みがそもそも無い
-
本記事は連載の１本目 である。
- 続編では、同じ定理を６つの言語で書いたコードの比較、宣言的スタイルが読みやすい理由が1934年にさかのぼること、30年で10種類以上の実装が作られながら広く使われているのは一つだけという事実に光をあてる
証明を「書く」とは、どういうことか
ここから、本題に入ります。
定理証明支援系では、証明をどう書くのでしょうか。
紙に書く数学の証明とは、少し違います。
コンピュータが検査できる形にする必要があるからです。
定理証明支援系には、いくつかの証明の書き方があります。
本記事では、その中でも 対照的な２つのスタイルに注目 します。
一つは、処理系と対話しながら、一手ずつ進めていく書き方 です。
これを、タクティクスタイル（tactic style）、あるいは**手続き的スタイル（procedural style）**といいます。
もう一つは、論証の筋道を最初から文章として書き切る書き方 です。
これを、**宣言的スタイル（declarative style）**といいます。
なお、日本語では「宣言型スタイル」と書かれることもありますが、本記事では「宣言的スタイル」で統一します。
両者の書き方の違い を、図にすると次のようになります。
タクティクスタイル では、この往復を繰り返します。
ファイルに残るのは、入力したタクティクだけです。
論証の筋道を、そのまま上から下へと流れるように書いていきます。
そして、書いたものだけで、何を証明しようとしているのかが読み取れます。
まず、１つ目のタクティク から見ていきます。
この書き方の感覚は、Python の作業に喩えることで、イメージがつかみやすくなります。
Jupyter Notebook のような書き方
Python でデータを分析するとき、Jupyter Notebook を使うことがあります。
- セルにコードを打ち込む
- 実行する
- 出力結果を目で見る
- その結果を解釈して、次に何をすべきかを考える
- 新しいセルに、次のコードを打ち込む
この繰り返しです。
大事なのは、３番目と４番目です。
出力結果を見なければ、次に何を書けばよいか分かりません。
定理証明支援系にも、これによく似た書き方があります。
「ここで場合分けせよ」「これを簡単にせよ」という短い指示 を打ち込むと、処理系が 「では、次はこれを証明してください」と画面に表示 します。
それを見て、プログラマ（人間）は、また次の指示を考える。
この指示のことを、タクティク と呼びます。
英語では tactic と書きます。
この言葉は、もともとは軍事用語です。
ギリシャ語の τάσσω（tassō、「順序立てて並べる」）に由来し、そこから τακτικός（taktikos、「並べることに関する」）という語が生まれました。
古代ギリシャの歴史家クセノフォンが、兵を隊列に並べる技術を指して使ったのが始まりとされています。
英語の tactic は、この流れを受けて「目的を達するための、個別の手立て」を意味します。
戦略（strategy） が全体の方針を指すのに対し、tactic は個々の場面での具体的な動きを指します。
全体を見通す大局的な視野に立った「戦略」（strategy）と、個々の戦闘や戦闘地域に視野を限定した作戦立案を行う「戦術」（tactics）という概念の違いに対応しています。
証明を組み立てるとき、エンジニアは一手ずつ指示を出していきます。
- 「ここで場合分けせよ」
- 「これを簡単にせよ
その一手一手が、目的である証明の完成へ向けた個別の手立てにあたります。
そこから、この呼び名が使われるようになりました。
なお、この意味での「タクティク」という語は、定理証明支援系を扱う方でなければ、まず耳にすることのない専門用語です。
どのようなタクティクが用意されているのか、主なものを挙げます。
| タクティク | 用意されている言語 | 何を指示するか |
|---|---|---|
intro / intros
|
Rocq、Lean 4 | 「すべての〜について」の変数や、仮定を手元に取り出す |
exact |
Rocq、Lean 4 | 示すべきことに、ちょうど合う証明を与える |
apply |
Rocq、Isabelle、Lean 4 | 既知の定理を当てはめる。残った部分が新しい目標になる |
assumption |
Rocq、Lean 4 | 手元にある仮定の中から、目標に合うものを探して使う |
reflexivity |
Rocq | 左辺と右辺が同じ形であることを示す |
rfl |
Lean 4 |
reflexivity と同じ |
rewrite / rw
|
Rocq、Isabelle、Lean 4 | 等式を使って、目標の中の式を書き換える |
subst |
Rocq、Lean 4 |
x = e という仮定を使い、目標の中の x をすべて e に置き換える |
simpl |
Rocq | 式を計算して簡単にする |
simp |
Isabelle、Lean 4 | 登録された規則を使って、式を簡単にする |
cbn |
Rocq |
simpl より控えめに簡単にする |
unfold |
Rocq、Isabelle、Lean 4 | 定義を展開する |
destruct |
Rocq | 値の形で場合分けする |
cases |
Isabelle、Lean 4 |
destruct と同じ働き |
induction |
Rocq、Isabelle、Lean 4 | 数学的帰納法で証明を進める |
induct_tac |
Isabelle |
induction の古い書き方 |
split |
Rocq | 「A かつ B」を、A と B の２つの目標に分ける |
left / right
|
Rocq、Lean 4 | 「A または B」のうち、どちらを示すかを選ぶ |
exists / use
|
Rocq、Lean 4 | 「〜が存在する」を示すために、具体的な値を挙げる |
constructor |
Rocq、Lean 4 | データの構成方法を使って、目標を組み立てる |
contradiction |
Rocq、Lean 4 | 矛盾する仮定があることを示して、証明を終える |
discriminate |
Rocq | 異なる構成子どうしが等しくないことを使う |
symmetry |
Rocq |
a = b を b = a に入れ替える |
assert / have
|
Rocq、Isabelle、Lean 4 | 途中の主張を立てて、それを別に証明する |
specialize |
Rocq、Lean 4 | 「すべての x について」という仮定に、具体的な値を当てはめる |
revert |
Rocq、Lean 4 | 手元にある仮定を、目標の側へ戻す |
auto |
Rocq、Isabelle | 簡単な目標を自動で片付ける |
blast |
Isabelle |
auto より強力な自動証明 |
ring |
Rocq、Lean 4 | 足し算と掛け算だけからなる等式を、自動で証明する |
omega / lia
|
Rocq、Lean 4 | 整数の一次不等式を、自動で証明する |
sledgehammer |
Isabelle | 外部の自動証明器に問い合わせ、証明の候補を探させる |
try |
Rocq、Lean 4 | 指定したタクティクを試し、失敗しても止まらない |
repeat |
Rocq、Lean 4 | 指定したタクティクを、失敗するまで繰り返す |
出典
Coq Tactics Index、coq-lean-cheatsheet、および各言語の公式文書
同じ働きのタクティクでも、言語によって名前が違うことに注目してください。
Rocq の reflexivity は、Lean 4 では rfl です。
また、Rocq の destruct は、Lean 4 では cases です。
この違いも、タクティクスタイルのコードを読みにくくする一因になっています。
この書き方には、大きな利点があります。
証明の道筋が分かっていなくても、試しながら進められるのです。
実際の入力と応答を、お見せします。
それぞれ違う言語、違う定理ですが、やりとりの形は同じです。
Rocq の場合
証明する定理：
「どんな命題 $P$ についても、$P$ が成り立つならば $P$ が成り立つ」
Theorem p_implies_p : forall P : Prop, P -> P.
Proof.
上記は、Rocq の処理系にプログラマが入力するコードです。
タクティク・スタイル で書かれています。
１行目は、証明する定理の宣言です。
p_implies_p は、プログラマが任意に付けた名前です。
my_theorem でも foo でも動きます。
P も同じで、Q でも A でも構いません。
Theorem、forall、Prop は、Rocq の予約語です。
他の文字列に変えると動きません。
２行目の Proof. も予約語 です。
「ここから証明を始めます」という宣言にあたります。
1 subgoal
-------------------(1/1)
forall P : Prop, P -> P
上記は、先ほどのコードが入力された後、Rocq の処理系が画面に出力する応答結果です。
３行あります。順に見ていきます。
１行目の 1 subgoal は、「証明すべきことが、いま１つ残っています」という意味です。
証明を進めると、この数が増えたり減ったりします。
場合分けをすれば増え、一つ片付ければ減ります。
この数が 0 になれば、証明の完了です。
２行目の -------------------(1/1) は、区切り線です。
この線には、意味があります。
- 線より上 ── いま手元にあるもの。使ってよい仮定や変数
- 線より下 ── いま示すべきこと
先ほどの応答では、線より上には何もありません。
まだ何も取り出していないからです。
末尾の (1/1) は、「１つある目標のうちの、１つ目」という意味です。
３行目の forall P : Prop, P -> P が、示すべき内容そのものです。
-
forall P : Prop── 「Prop すなわち命題である、すべての $P$ について」 -
P -> P── 「$P$ ならば $P$」
つまり、「どんな命題 $P$ についても、$P$ が成り立つならば $P$ が成り立つ」ということです。
これは、最初に宣言した定理と、まったく同じ内容です。
これは当然のことです。
まだ何も証明していないのですから、示すべきことは最初のままです。
intros P P_holds.
上記は、プログラマが次に入力するコード です。
intros は、「取り出せ」という指示です。これは予約語です。
「すべての $P$ について」の $P$ を取り出し、
さらに、「$P$ が成り立つ」という仮定を取り出して、P_holds という名前を付けています。
P_holds は、プログラマが任意に付けた名前です。
h でも hyp でも構いません。
ただし、後でその仮定を使うときは、付けた名前で呼ぶ必要があります。
1 subgoal
P : Prop
P_holds : P
-------------------(1/1)
P
上記は、Rocq の処理系が画面に出力する応答結果です。
線の上に、２つの項目が増えました。
-
P : Prop── 「P は命題である」 -
P_holds : P── 「P が成り立つという仮定を、P_holdsという名前で持っている」
そして、線の下、つまり示すべきことが P だけになりました。
先ほどまで forall P : Prop, P -> P だったものが、P に減っています。
assumption.
上記は、プログラマが 次に入力するコード です。
assumption は、「手元にある仮定を使え」という指示です。
いま手元には P_holds : P があり、示すべきは P です。
そのまま使えます。
No more subgoals.
上記は、Rocq の処理系が画面に出力する応答結果です。
「証明すべきことは、もうありません」。
証明が完了 しました。
出典
Coq Tactics Cheatsheet, コーネル大学 CS3110
Isabelle の場合
証明する定理：
「足し算の結合法則」。
$x$ に「$y$ と $z$ の和」を足したものは、「$x$ と $y$ の和」に $z$ を足したものに等しい。
theorem add_associativity : "plus x (plus y z) = plus (plus x y) z"
apply(induct_tac x)
上記は、Isabelle の処理系にプログラマが入力するコードです。
タクティク・スタイル で書かれています。
１行目は、定理の宣言です。
add_associativity は、プログラマが任意に付けた名前です。
assoc でも thm1 でも動きます。
x、y、z という変数名も、任意です。
plus は、別の場所で 定義された関数の名前 です。
定義したときの名前と一致していれば、任意に決められます。
theorem と apply は 予約語、
induct_tac は タクティクの名前 です。
いずれも他の文字列に変えると動きません。
induct_tac は、「指定した変数について、数学的帰納法で証明を進めよ」という指示です。
自然数について帰納法を使うとは、次の２つに分けて示すことを意味します。
-
その変数が 0 のとき、主張が成り立つこと
- その変数である数について成り立つならば、その次の数についても成り立つこと
この２つが示されれば、すべての自然数について成り立つと言えます。
２行目の apply(induct_tac x) が、タクティクです。 「
「$x$ について場合分けせよ」という指示です。
自然数についての場合分けとは、「0 のとき」と「ある数の次の数のとき」の２つに分けることを意味します。
proof (prove)
goal (2 subgoals):
1. plus Zero (plus y z) = plus (plus Zero y) z
2. ⋀x. plus x (plus y z) = plus (plus x y) z ⟹
plus (Suc x) (plus y z) = plus (plus (Suc x) y) z
上記は、先ほどのコードが入力された後、Isabelle の処理系が画面に出力する応答結果です。
「証明すべきことが２つに増えました」という意味です。
１つ目は、$x$ が 0 の場合です。
Zero が 0 を表します。
２つ目は、$x$ が１つ大きくなった場合です。
Suc x が「$x$ の次の数」を表します。
記号の読み方 を説明します。
-
⟹── 「ならば」を表します -
⋀── 「すべての x について」という意味です
つまり２つ目は、「どんな $x$ についても、$x$ で成り立つならば、$x$ の次の数でも成り立つ」ことを示せ、と言っています。
apply(auto)
done
上記は、プログラマが次に入力するコード です。
auto は、「自動で片付けよ」という指示です。
これは タクティクの名前で、変えられません。
Isabelle が持つ自動証明の仕組みを呼び出します。
done は、「証明を終える」という宣言です。
これも 予約語です。
この２つで、残った２つの目標が解決され、証明が完了します。
出典
Fundamentals of Isabelle ── Learn Mathematics and Computer Science with Isabelle
Lean 4 の場合
証明しようとしているのは、次の主張です。
「$x$ と $y$ は自然数である。$x$ は素数であり、偶数ではない。そして $y$ は $x$ より大きい。このとき、$y$ は4以上である。」**
1 goal
x y : ℕ,
h₁ : Prime x,
h₂ : ¬Even x,
h₃ : y > x
⊢ y ≥ 4
上記は、Lean 4 の処理系が画面に出力する応答結果です。
⊢ という記号が、境目です。
この記号より前の行が「文脈」、つまり、いま手元にあるものです。
-
x y : ℕ── x と y は自然数である -
h₁ : Prime x── 「x は素数である」という仮定を、h₁という名前で持っている -
h₂ : ¬Even x── 「x は偶数ではない」という仮定 -
h₃ : y > x── 「y は x より大きい」という仮定
そして ⊢ の後が、示すべきことです。
-
⊢ y ≥ 4── 「$y$ は4以上である」ことを示せ
x、y、h₁、h₂、h₃ は、いずれもプログラマが任意に付けた名前です。
別の名前でも動きます。
ℕ（自然数）、Prime（素数）、Even（偶数）は、ライブラリで定義された名前 です。
他の文字列に変えると動きません。
Mathematics in Lean という教材に、次の説明があります。
The lines before the one that begins with ⊢ denote the context: they are the objects and assumptions currently at play.
（筆者による日本語訳）
⊢で始まる行より前の行が、文脈を表す。それらは、いま扱っている対象と仮定である。
そして、同じ教材には次の記述もあります。
When a cursor is in the middle of a tactic proof, Lean reports on the current proof state in the Lean Infoview window. As you move your cursor past each step of the proof, you can see the state change.
（筆者による日本語訳）
**カーソルがタクティクによる証明の途中にあるとき、Lean は現在の証明状態を Infoview という枠に表示する。
証明の各段階にカーソルを動かすにつれて、状態が変わっていくのが見える。**
出典
同上
Infoview とは、コードを書いている画面の横に置かれた、専用の表示領域のことです。
そこに表示されるのが、上に示した内容です。
すなわち、⊢ の前に並ぶ「いま手元にあるもの」と、⊢ の後に書かれた「示すべきこと」 です。
カーソルをタクティクの行から次の行へ動かすと、その表示が切り替わります。
たとえば、仮定を一つ取り出すタクティクを実行した直後にカーソルを置けば、⊢ の前の行が一つ増えた状態が表示されます。
Rocq や Isabelle と、表示の形は違います。
しかし、「いま何が使えるか」と「何を示すべきか」を表示している点は、同じです。
タクティクスタイルを持つ３つの言語に共通していること
言語が違っても、やりとりの形は同じです。
| Rocq | Isabelle | Lean 4 | |
|---|---|---|---|
| 示すべきこと | 線の下 |
goal の後 |
⊢ の後 |
| 使える仮定 | 線の上 | 目標の中に、⟹ の左側として含まれる |
⊢ より前の行 |
| 目標が複数のとき | 2 subgoals |
goal (2 subgoals) |
2 goals |
| 完了したとき | No more subgoals. |
目標が消える | goals accomplished |
コラム: Isabelle の「使える仮定」について
上の表に書いたのは、apply を使う タクティクスタイルでの表示 です。
先ほど見た応答でも、仮定は ⟹ の左側に置かれ、目標の一部として書かれていました。
しかし、Isabelle にはもう一つの書き方があります。
それが、本記事の主題である Isar です。
Isar で assume を使って仮定を置くと、その仮定は名前を持ち、Rocq や Lean 4 と同じように、目標とは区別された文脈として扱われます。
同じ Isabelle でも、書き方によって表示のされ方が変わるのです。
この点は、この後 Isar のコードを見ていくときに、改めて確認できます。
いかがでしたでしょうか。
ここまで、複数の定理証明言語で、タクティクのコマンドを入力して、処理系からの応答を見ながら、次のタクティクコマンドを入力する対話的プログラミングの事例をご紹介しました。
いずれの言語でも、一目見て何をしているのかを理解するのは難しいと、お気づきになられたのではないでしょうか。
この記事では、最初にどの問題を証明しようとしているのかを日本語で明示し、各コードに解説文を付けさせていただきました。
しかし、皆様が、こうした日本語の注釈抜きに、いきなり同僚や先輩、後輩や取引先から、タクティクコードと処理系からの応答結果が並んで数百行も記述されたファイルを見せられたら、何をしようとしている対話プログラミングの記録なのか、すぐに解読できずに困惑するのではないでしょうか。
しかし、タクティクスタイルが劣っているわけではありません。
タクティクスタイルは、証明を探す作業には、非常に向いているからです。
処理系と対話しながら、どの道筋で進めばよいかを試すことができます。
タクティクスが不便なのは、完成した証明を第３者が目を通して、その論証の意図を理解しようとする場面です。
つまり、書くときと読むときで、向き不向きが違うのです。
それでは、次に、定理証明支援系が持つもう一つの書き方である、宣言的スタイル について見ていきましょう。
このスタイルは、数学の教科書や論文に印刷された、ときには数ページ、数十ページに及ぶ証明文のように、上から下に視線を流していくと、出発点となる前提や過程が何で、証明がどのように論理的に連なっているのか、論理の鎖のつながりを読み取ることができる書き方 です。
これから、先ほどタクティクの書き方を示した同じ言語での、宣言的スタイルのコードの例をお示しします。
ただし、宣言的スタイルには難点もあります。
それは、最終的に読者へ見せたい証明の構造を、ある程度は意識して書く必要がある、ということ です。
宣言的スタイル は、タクティク のように、一段ずつ試行錯誤しながら証明作業を進めていって、うまくいかなかったり行き詰まったと気づいたときに前の段階へ戻る、という進め方には向いていません。
タクティク では、あらかじめプログラマが証明全体の筋道を描いていなくても、試行錯誤できました。指示を打ってみて、返ってきた応答から次の方針を得られたからです。
宣言的スタイルでは、そうはいきません。
できることといえば、証明全体の筋道がある程度は見えている状態で、「この部分の証明は後回しにして、他の部分を先に進める」と決めることくらいです。
そのための仕組みが、sorry です。
ただし、筋道が見えていなければ使えません。そこが制約です。
sorry という仕組み
Isabelle には sorry という語があります。
「この部分は、まだ証明していません」と処理系に伝える印 です。
- まず証明の骨組みだけを書き、細かい部分には
sorryと書いておく。 - 骨組みが正しく組めているかを確かめてから、
sorryを一つずつ埋めていく。
この進め方が実際に使われています。
（出典）
"HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement", arXiv:2505.15740, 2025年
原文:
a user could write a proof sketch in Isar by writing sorry instead of by simp—telling Isabelle to assume the subgoal is correct. Then, after using Isabelle to check that the proof sketch is sufficient, users can fill in the details to finish the proof.
筆者による日本語訳:
利用者は、
by simpの代わりにsorryと書くことで、Isar による証明の素描を書ける。それは Isabelle に「この部分目標は正しいものとして扱え」と伝えることを意味する。
そして Isabelle を使って、その素描で足りることを確かめたあと、細部を埋めて証明を仕上げられる。
さらに、この進め方を徹底した事例があります。
出典:"Munkres' General Topology Autoformalized in Isabelle/HOL", arXiv:2604.07455, 2026年
ムンクレスの『位相空間論』という教科書 を、Isabelleで形式化した研究 です。
そこでは、「sorry-first workflow」と名付けられた手順 が採られました。
（原文）
1. Write the proof skeleton with sorry at every step. No other tactic is permitted in new code
6. When sledgehammer fails, decompose the step into finer have blocks and repeat.
（筆者による日本語訳）
１. 証明の骨組みを書き、そのすべての行に
sorryと書く。新しいコードでは、他のタクティクを一切使わない。
６. sledgehammer が失敗したら、その行をより細かいhaveのブロックへ分解し、繰り返す。
６番に注目してください。
うまくいかない箇所があれば、その行を have のブロックへ分解するとあります。
have は、宣言的スタイルの語です。
「この時点で、これが成り立つ」と、途中の主張を書き記すために使います。
なぜ、分解するとうまくいくのでしょうか。
sledgehammer は、「いま示すべきこと」と「手元にある定理」の隔たりを埋める仕組みです。その隔たりが大きすぎると、探索が終わりません。
have で分解するとは、その隔たりを小さく刻むことです。
「$A$ から $D$ が導出される」を一度に示すことができないときは、途中に have "B"、have "C" と書き足します。
すると、$A$ から $B$、$B$ から $C$、$C$ から $D$ という短い区間を、それぞれ探せばよい、という状況を生み出せるのです。
１つの大きな跳躍を、３つの小さな歩みに置き換える わけです。
骨組みを書き、足りなければ行を分け、sorry を埋めていく。そうした戦略です。
さて。
これから、宣言的スタイル を見ていただく前に、Agda と Mizar では、タクティクの仕方が少し違ったり、タクティク のスタイルが存在しないことを、先にご紹介します。
Agda の場合 ── 穴を埋めていく方式
Agda には、これまで見てきたような タクティクがありません。
Agda では、「穴」と呼ばれる仕組みを使います。
まず、書けるところまで書き、まだ分からない部分に ? と書きます。
proof : P → P
proof x = ?
上記は、Agda の処理系にプログラマが入力するコードです。
proof は、プログラマが任意に付けた名前です。 x も同じく任意です。
? の部分が、「ここはまだ書けていません」という印です。
このファイルを読み込ませると、Agda はその ? を「穴」として扱います。
そして、穴にカーソルを置いて命令を出すと、Agda が応答します。
Agdaの公式文書に、主な命令が挙げられています。
| 命令 | 何をするか |
|---|---|
C-c C-l |
ファイルを読み込み、型を検査する |
C-c C-, |
その穴に何を入れるべきか、その型と、使える変数を表示する |
C-c C-c |
変数について場合分けする |
C-c C-SPC |
穴に式を入れる。型が合っていれば受け付ける |
出典:A Taste of Agda ── Agda documentation
C-c とは、Ctrl キーを押した状態で c を押すことを意味しています。
Emacs をお使いの方には、おなじみの書き方です。
したがって C-c C-l は、「Ctrl キーを押しながら c、続けて Ctrl キーを押しながら l」という操作になります。
先述の公式文書には、次の説明があります。
Agda programs are typically developed interactively, which means that one can type check code which is not yet complete but contain "holes" which can be filled in later.
（筆者による日本語訳）
Agda のプログラムは、通常、対話的に書き進められる。
つまり、まだ完成しておらず「穴」を含むコードを、型検査にかけることができる。
その穴は、後から埋めることができる。
これは、タクティクとは根本的に違います。
タクティクでは、「こう証明せよ」という指示を処理系に出します。
すると、処理系が、その指示に従って証明を組み立ててくれます。
Agda ではこの関係が逆です。
プログラマが穴に対して「ここに入るべきものの型は何か」と問い合わせ、Agda がそれを表示します。
そして、その型に合う式を、プログラマ自身がキーボードから打ち込んで、穴を埋めます。
なぜ、こういう仕組みになっているのでしょうか。
Agda では、証明そのものが、プログラムの一部として書かれるからです。
Agda において、証明を書くこととプログラムを書くことは、同じ作業です。
「この定理を証明する」ことは、「この型を持つ関数を書く」ことにあたります。
そのため、穴を埋める作業は、関数の中身を書く作業そのものになります。
すべての穴を、Agda の処理系と対話しながら埋めることができたとき、プログラマが証明したい命題を、Agda のソースコードに置き換えられたことを意味します。
なお、ここには理論的な背景があります。
詳細には立ち入りませんが、数理論理学 の世界では、証明すべき論理命題の証明が、実行可能なプログラミングのコードに対応するという事実 が知られています。
カリー・ハワード同型対応と呼ばれるものです。
Agda の穴を埋める作業は、この対応関係を、そのまま実行しているのです。
この仕組みの背景については、続編の記事で詳しく扱います。
Mizar の場合 ── Mizar は対話スタイルという仕組みがない
Mizar には、タクティクがありません。
そして、対話的に証明を組み立てる仕組みもありません。
Mizar は、対話的にコードを一つ一つ入力して実行するのではなく、スクリプトファイルにコードを全行書いて、ファイルを一括実行する言語です。
ここで、各言語のスクリプトファイルの拡張子を挙げておきます。
| 言語 | 拡張子 |
|---|---|
| Rocq（旧 Coq） | .v |
| Isabelle | .thy |
| Lean 4 | .lean |
| Agda | .agda |
| Mizar | .miz |
| HOL Light | .ml |
Mizar のスクリプトファイルの拡張子は、.miz です。
では、そのファイルを、どうやって検査にかけるのでしょうか。
mizf というコマンドを使います。
書き上げた .miz ファイルを、まとめて検査するためのコマンドです。
mizf text/test
この例では、text というフォルダにある test.miz を検査しています。
ファイル名から拡張子を除いた部分を指定する書き方です。
Mizar の公式資料には、次の趣旨が記されています。
原稿は任意のエディタで書き、それを Accommodator という部分が処理して環境を用意し、Verifier という部分が検査する。そして、この２つは通常 mizf という利用者向けのコマンドから呼び出される、と。
出典:Mizar Home Page: Mizar System
うまくいけば、誤りの報告は出ません。誤りがあれば、.miz ファイルそのものに印が書き込まれ、その箇所とエラーの番号が示されます。
ここまでを整理します。
Mizar には、タクティク がありません。
処理系と対話しながら一手ずつ進める仕組みもありません。
できるのは、書き上げたファイルを、まとめて検査にかけることだけです。
ところで、Mizar は、宣言的スタイルを最初に示した言語です。
詳しくは、この後の本文で扱います。
以上、Agda ではタクティクの書き方が、「穴」を対話的に埋めていくという独特なスタイルをとることと、Mizar では対話的なプログラミングスタイルが存在しないことをご紹介しました。
宣言的スタイル に入りたいところですが、その前にもうひとつ、確認しておきたいことがあります。
タクティクスタイルで書いた入力と、処理系からの応答結果を、仮にファイルに一括出力することができた場合、そのファイルはどう見えるのか、という点 です。
実は、定理証明支援系ではそうしたことはできないのですが、その事情は後で説明します。
仮にできたとしても、タクティク・コマンドの入力と、処理系からの応答出力のペアを書き連ねたファイルは、何を行おうとしているコードなのか、可読性が低いのです。
そのことを確認した後で、宣言的スタイル の解説に入らせていただきます。
タクティクスタイルのコードを、スクリプトファイルで一括実行した場合
では、すでに取り上げたものと同じ証明を、今度はファイルに書いて一括で実行する場合について見ていきます。
まず、ファイルの中身です。
Theorem p_implies_p : forall P : Prop, P -> P.
Proof.
intros P P_holds.
assumption.
Qed.
これが、ファイルの中身のすべてです。
ファイルの拡張子は .v です。
ファイル名は、プログラマが任意に付けることができます。
ここでは仮に、 my_proof.v としたとしましょう。
Python でいえば、my_script.py にあたるものだと考えてください。
さきほど対話的に実行したときと、同じタクティクが並んでいます。
では、このファイルを実行すると、どうなるでしょうか。
対話的に作業したときには、1 subgoal や P : Prop、No more subgoals. といった応答が、画面に表示されていました。
それと同じ内容が、実行後にファイルとして得られるのでしょうか？
Theorem p_implies_p : forall P : Prop, P -> P.
Proof.
intros P P_holds.
assumption.
Qed.
上記のファイルを、一括で実行してみます。
Rocq の場合、次のコマンドを使います。
rocq compile my_proof.v
Python でいえば、python my_script.py にあたります。
このコマンドを実行すると、作業ディレクトリに新しいファイルが作られます。
Rocq の場合、my_proof.vo というファイルです。
元のファイル名の拡張子が、.v から .vo に変わったものです。
では、その中身を見てみましょう。
テキストエディタで開いても、人間の目には、何が書かれているのか解読不能です。
.vo はバイナリファイルだからです。
では、この .vo ファイルは、何のために作られるのでしょうか。
他の証明から読み込むためです。
証明は、積み重ねて書きます。
ある定理を証明したら、次はそれを使って別の定理を証明する。
その繰り返しです。
このとき、毎回すべてを最初から検査し直していては、時間がかかりすぎます。
そこで、一度検査を通した証明は、.vo という形で保存しておきます
次に別のファイルからその定理を使うときは、既に検査を通った成果物を読み込みます。
証明を最初から組み立て直し、検証し直す必要がありません。
Python でいえば、.pyc ファイルに近い役割です。
一度処理した結果を保存しておき、次回はそれを使って起動を速くする。
Rocq の公式文書にも、.v ファイルをコンパイルすると .vo ファイルが作られ、それは他の証明から読み込むためのコンパイル済みライブラリである、と記されています。
出典:The Rocq commands ── Rocq Prover documentation
Lean 4 も同じです。
.lean ファイルから .olean ファイルが作られます。
Lean の公式文書には、次の記述があります。
In these files, Lean terms and values are represented just as they are in memory; thus the file can be directly memory-mapped.
筆者による日本語訳:
これらのファイルでは、Lean の項と値が、メモリ上にあるのとまったく同じ形で表現されている。そのため、このファイルは直接メモリに写し取ることができる。
出典:Elaboration and Compilation ── Lean Language Reference
つまり、.olean ファイルは、Lean の処理系がメモリに読み込んで、そのまま使うための形式です。
人間が読むことは、想定されていません。
この点は、Rocq の .vo も同じです。
どちらも、「次にこの定理を使うときに、検査をやり直さずに済ませる」ための保存形式です。
対話的に作業していたときに表示されていた「1 subgoal」「P : Prop」「No more subgoals.」といった応答は、この出力ファイルに一文字も含まれていないのです。
対話しているときに画面へ表示される証明の状態そのものが、通常の証明のソースとして保存されるわけではないのです。
各言語について、まとめます。
| 言語 | 入力ファイル | 実行コマンド | 出力ファイル | 中身 |
|---|---|---|---|---|
| Rocq | my_proof.v |
rocq compile |
my_proof.vo |
バイナリ |
| Lean 4 | MyProof.lean |
lake build |
MyProof.olean |
バイナリ |
| Isabelle | MyProof.thy |
isabelle build |
セッションの保存形式 | バイナリ |
なお、実行が成功した場合、画面にも何も表示されません。 エラーがあったときだけ、その内容が表示されます。
仮に、入力と出力の両方が記録されたとしても・・・
ここまでで、次のことが分かりました。
対話中は処理系からの応答出力が表示されるが、ファイルには残らない。
では、こう考えられるかもしれません。
「入力と出力をペアで記録すれば、後から読めるのではないか。」
技術的には、それは可能です。
Rocq には Show という命令があり、その時点の証明状態を出力させることができます。
Isabelle にも同様の仕組みがあります。
リダイレクトでファイルへ送ることも可能です。
しかし、それでも読みやすくはなりません。
先ほど見た、Rocq や Isabelle、Lean 4 のタクティクを思い出してください。
その入力の合間に、処理系からの応答が挟まったものを想像してください。
（タクティクの入力）
→ 処理系からの出力
（タクティクの入力）
→ 処理系からの出力
（タクティクの入力）
→ 処理系からの出力
……
これが、数百行にわたって続きます。
一つ一つの応答は、その時点で何が残っているかを教えてくれます。
しかし、「なぜここでこの指示を出したのか」「この先どこへ向かうのか」は、どこにも出てきません。
タクティクの列は、アセンブリ言語の命令の並びに似ています。
一つ一つの命令が何をするかは分かります。
しかし、その連なりが全体として何を実現しようとしているのかは、読み取りづらいのです。
Java や Ruby、Python、Scala のコードを読むのとは、質が違います。
それらの言語のコードなら、関数名や変数名がソースコードの処理内容を物語ってくれます。
例えば、calculate_monthly_total という名前を見れば、その関数が何のためにあるかは分かります。
タクティクの列には、そうした手がかりがありません。
実例 をご覧ください。
let NSQRT_2 = prove
(`!p q. p * p = 2 * q * q ==> q = 0`,
MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
POP_ASSUM MP_TAC THEN CONV_TAC SOS_RULE);;
上記は、HOL Light という定理証明支援系で書かれた証明です。
（出典）
Freek Wiedijk 編, "The Seventeen Provers of the World", Lecture Notes in Artificial Intelligence 第3600巻, Springer, 2006年, 18頁。
このコードを書いたのは、HOL Light の作者である John Harrison です。
証明しているのは、「$p × p = 2 \times q \times q$ を満たす自然数 $p$ と $q$ があるならば、$q$ は $0$ である」という主張です。
これは、√2 が無理数であることを示すための、中心となる補題です。
さて、２行目より下をご覧ください。
大文字の命令が、延々と並んでいます。
MATCH_MP_TAC、REWRITE_TAC、REPEAT STRIP_TAC、FIRST_ASSUM、DISCH_THEN、X_CHOOSE_THEN、SUBST_ALL_TAC、FIRST_X_ASSUM、POP_ASSUM、CONV_TAC。
それぞれの命令が何をするかを知っていても、この列全体が何を示しているのかは読み取れません。
タクティクの名前は、何をするかを述べていても、なぜそれをするのかは述べていないからです。
なお、これは HOL Light に限った話ではありません。
先ほど見た Rocq の intros、assumption。
Isabelle の induct_tac、auto。
Lean 4 の rintro、obtain。
いずれも、その命令が何をするかは示していても、なぜその順序で出すのか、どこへ向かっているのかは示していません。
そして、これらの入力と処理系からの応答を対にして書き連ねたファイルは、どの言語であっても、同じように読み取りづらいものになります。
HOL Light の例は、大文字の命令が並ぶために見た目の印象が強いだけです。
問題の性質は、タクティクスタイルを採るすべての言語に共通しています。
【誤解を招かないために】証明が長くなるのは、タクティクのせいではありません
「タクティクで書くと証明が長くなる」と、誤解されないようお願いします。
証明は、書き方に関わらず、検証したいプログラムよりもはるかに長くなります。
例を挙げます。
seL4 という OS の中核部分を検証した事例では、8,700行のＣコードに対して、約20万行の証明が書かれました。約23倍です。
（出典）
Gerwin Klein, Kevin Elphinstone, Gernot Heiser ほか, "seL4: Formal Verification of an OS Kernel", Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles（SOSP'09）, 207〜220頁, 2009年
論文には、seL4 が「8,700行のＣコードと600行のアセンブラから成る」と記されています。
証明の規模については、約20万行、約20人年とされています。
なぜ、こうなるのでしょうか。
コードは「何をするか」だけを書けばよいのに対し、証明は「なぜ、あらゆる場合に正しいのか」を書かなければならないからです。
配列から最大値を取り出す関数を考えてください。
コードは十数行で書くことができます。
しかし、「この関数は必ず最大値を返す」ことを証明するには、次のすべてを示す必要があります。
- 配列が空のときはどうなるのか
- 要素が１つのときはどうなるのか
- 繰り返しのあいだ、何が保たれているのか
- 繰り返しが終わったとき、なぜ答えが正しいのか
そして、証明には省略が許されません。
人間が読む数学の本なら「明らかに」と書いて飛ばせる箇所も、処理系に検査させるには、すべて書き切る必要があります。
この事情は、タクティクでも宣言的スタイルでも変わりません。
むしろ、後の部で見るとおり、宣言的スタイルのほうが約２倍長くなるという報告があります。
この論点については、筆者が以前に公開した記事でも詳しく扱っています。
つまり、本記事が問題にしているのは、長さではありません。読みやすさです。
まったく同じ処理を、宣言的スタイルで見てみる
ここまで、タクティクの読みにくさ を見てきました。
では、同じ内容を宣言的スタイルで書くと、どうなるでしょうか。
先ほど見た、Rocq のスクリプトファイルの中身を思い出してください。
Theorem p_implies_p : forall P : Prop, P -> P.
Proof.
intros P P_holds.
assumption.
Qed.
同じ定理を、同じ処理系の宣言的スタイル で書くとこうなります。**
このコードは、C-zar という記法を説明するために、文献に記された構文をもとに筆者が書いたものです。
筆者の環境では実機での検証をしていません。
そのまま実行しても動かない可能性があります。構文の雰囲気を掴むための例示として、ご覧ください。
Theorem p_implies_p : forall P : Prop, P -> P.
proof.
let P : Prop.
assume P_holds : P.
thus thesis by P_holds.
end proof.
Qed.
書き綴られたコードの内容は以下の通りです。
-
let P : Prop.── 「$P$ を命題とする」 -
assume P_holds : P.── 「$P$ が成り立つと仮定する。それを P_holds と呼ぶ」 -
thus thesis by P_holds.── 「よって、示すべきことが、P_holds によって示された」
処理系を動かさなくても、何をしているのかが読み取れます。
今度は、タクティクを対話的に実行したときの応答を思い出してください。
処理系は「P : Prop」「P_holds : P」「示すべきは P」と応答結果を表示していました。
つまり、宣言的スタイルのコードには、それとほぼ同じ内容が、最初から書かれているのです。
対話的にタクティクを入力したときには画面にしか表示されなかった処理系からの応答が、宣言的スタイルではスクリプトファイルに書かれている。そういうことです。
なお、この Rocq の宣言的スタイルは C-zarと呼ばれる記法 です。
この記法の来歴と、なぜ広まらなかったのかについては、続編の記事で扱います。
宣言的スタイルが、何をしているのか
have "Q" by ... と書けば、「この時点で $Q$ が成り立つ」ということが、コードそのものに書き込まれます。
画面にしか出なかったものを、ファイルに残す。
しかも、すべての状態ではなく、書き手が「ここは書き留めておくべきだ」と判断したものだけを残します。
これが、宣言的スタイル のしていることです。
そして、その結果、できあがるコードは、数学の論文や教科書に印刷された証明と、似た見た目 になります。
「何を仮定し、どういう道筋で、何を示したのか」が、そのまま文章として書かれている からです。
【重要】宣言的スタイルの本質は、語彙ではありません
ここまで、assume（仮定する）、have（〜が成り立つ）、thus（よって）といった語を紹介してきました。
そのため、「assume や have、thusなど、自然言語（英文）に似た単語を使うことが、宣言的スタイルである」と受け取られた方もおられるかもしれません。
しかし、そうではありません。
宣言的スタイルの本質 は、証明の途中で何を仮定し、何を導き、次に何を示すのかという論理構造をコードの中に明示的に記述すること にあると筆者は考えています。
先ほどの Isar のコードを、もう一度ご覧ください。
theorem "even n ⟹ 4 dvd n^2"
proof -
assume "even n"
then obtain k where "n = 2 * k" ..
then have "n^2 = 4 * k^2" by simp
then show "4 dvd n^2" by simp
qed
assume、obtain、have、show という語が並んでいます。
しかし、大切なのは、人間がそのまま理解できる英単語が用いられていることではありません。
assume "even n" の後ろに書かれた "even n" という主張。
then have "n^2 = 4 * k^2" の後ろに書かれた "n^2 = 4 * k^2" という主張。
これらがコードに記述されていることこそが、本質的に重要なのです。
then という語は、「直前に示したことを使って、次を導く」という関係を示しています。
つまり、人間は、コードを眺めることで、次のことを読み取ることができるのです。
- 証明の出発点はどの状態か（
assume） - 証明の過程で何を導いたのか（
have） - 証明全体の中の各段階が、それより別のどの段階に依存しているのか（
then、with、from） - 最終的に何が示された（証明された）のか（
show）
タクティクスタイルには、この情報がありませんでした。
apply (rule exI) という行を見ても、その時点で何が成り立っている（何が証明されている）のかは、どこにも書かれていなかったのです。
証明の道筋の論理的な流れがコードに残るかどうか。 そこが、２つのスタイルを分けています。
英文の単語は、その構造を書き表すための手段にすぎないのです。
証明が長くなると、差は歴然とする
いま見ていただいた例では、タクティクスタイル も 宣言的スタイル も、どちらも短いものでした。
しかし、定理の証明過程が長くなると、両者の差は歴然としてきます。
実例をお見せします。
例その１:カントールの定理（Isabelle）
カントールの定理とは、次の主張です。
「どんな集合についても、その集合から、その集合のすべての部分集合を集めたものへの、全射は存在しない」
全射とは、行き先のすべての要素に、少なくとも一つは対応するものがある写像のことです。
言い換えると、「ある集合と、その部分集合を全部集めたものとは、決して同じ大きさにはならない」ということです。
無限の大きさにも段階があることを示した、集合論の基本的な定理 です。
まずは、この定理を証明するコードを、タクティクスタイル で書いた場合です。
theorem "∃S. S ∉ range (f :: 'a ⇒ 'a set)"
apply (rule exI)
apply (rule notI)
apply (erule rangeE)
apply (erule equalityCE)
apply (drule CollectD)
apply (erule contrapos_np)
apply (erule imageI)
apply (erule notE)
apply (rule CollectI)
apply assumption
done
apply が９回並んでいます。
それぞれの命令の意味は、次のとおりです。
-
rule exI── 「存在する」を示すための規則を当てはめる -
rule notI── 「〜でない」を示すための規則を当てはめる -
erule rangeE── 「値域に含まれる」という仮定を分解する -
erule equalityCE── 集合が等しいという仮定から、場合分けする -
drule CollectD── 集合の定義を使って、仮定を書き換える -
erule contrapos_np── 対偶を取る -
erule imageI── 像に含まれることを示す規則を当てはめる -
erule notE── 矛盾を導く -
rule CollectI── 集合に属することを示す -
assumption── 手元の仮定を使う
一つ一つの意味は分かります。
しかし、この９行を上から読んで、この証明が何をしているのかを掴める方は、まずいらっしゃらないと思います。
ちなみに、この証明で使われているのは、対角線論法と呼ばれる有名な論法 です。
これは、19世紀の数学者ゲオルク・カントールが考案した論法です。
どういう論法かというと、「自分自身を指す条件」を作り、そこから矛盾を導くアプローチをとります。
日常の例で説明します。
ある村に、床屋が一人いるとします。** そして、次の決まりがあるとします。
「この床屋は、自分で髭を剃らない人だけの髭を剃る」
さて、この床屋自身の髭は、誰が剃るのでしょうか。
もし床屋が自分で髭を剃るなら、 決まりにより、この床屋は「自分で髭を剃る人」なので、床屋は剃ってはいけません。 つまり、自分で剃っていないことになります。矛盾です。
もし床屋が自分で髭を剃らないなら、 決まりにより、この床屋は「自分で髭を剃らない人」なので、床屋が剃るはずです。 つまり、自分で剃っていることになります。やはり矛盾です。
どちらに転んでも矛盾する。
この形が、対角線論法です。
「自分自身」を条件の中に含めることで、どちらの答えを選んでも逆の結論が出る状況を作り出します。
カントールは、この論法を使って、「無限には大きさの違いがある」ことを証明しました。
なぜ「対角線」と呼ばれるのかについては、もともとカントールが表を作り、その対角線上の要素を取り出して新しいものを作るという形で証明を示したことに由来します。
本記事では、その形までは立ち入りません。
**この後の Isar 版のコードで、床屋の例と同じ構造が現れます。
そのとき、改めて対応を示します。
次に、同じ定理を Isar で書いた場合です。
なお、宣言的スタイルを Isabelle で実現した言語が Isar です。
theorem "∃S. S ∉ range (f :: 'a ⇒ 'a set)"
proof
let ?S = "{x. x ∉ f x}"
show "?S ∉ range f"
proof
assume "?S ∈ range f"
then obtain y where "?S = f y" ..
then show False
proof (rule equalityCE)
assume "y ∈ f y"
assume "y ∈ ?S"
then have "y ∉ f y" ..
with ‹y ∈ f y› show ?thesis by contradiction
next
assume "y ∉ ?S"
assume "y ∉ f y"
then have "y ∈ ?S" ..
with ‹y ∉ ?S› show ?thesis by contradiction
qed
qed
qed
出典:Makarius Wenzel, "Miscellaneous Isabelle/Isar examples", Isabelle 公式の資料集
行数は増えました。
タクティク・スタイルのコードが11行だったのに対して、宣言的スタイル（Isar）のコードは、18行 と増えています。
しかし、Isarのコードは、タクティク の時とは状況が大きく異なり、上から下に視線を流していくことで、処理の内容（証明の筋道）を追うことができます。
一行ずつ、見ていきましょう。
第１段階:特別な集合を作る
let ?S = "{x. x ∉ f x}"
{x. x ∉ f x} という書き方は、「〜という条件を満たす $x$ を、すべて集めたもの」という意味です。
その条件が、x ∉ f x です。
読み方を説明します。** f x は「$f$ が $x$ に対応させる集合」、∉ は「含まれない」を表します。
つまり、x ∉ f x は「$x$ は、$f$ が $x$ に対応させた集合に含まれない」という条件です。
具体例で考えてみましょう。
$f$ が、$1$ に「{1, 2}」を、$2$ に「{3}」を対応させているとします。**
- 1 の場合: $f$ が $1$ に対応させた集合は {1, 2} です。この中に $1$ は含まれています。 よって条件を満たしません
- 2 の場合: $f$ が $2$ に対応させた集合は {3} です。この中に $2$ は含まれていません。 よって条件を満たします
この ?S は、条件を満たすものだけを集めた集合です。
上の例なら、$2$ は入りますが、$1$ は入りません。
?S は、プログラマが任意に付けた名前です。 ?T でも動きます。
第２段階:示すべきことを宣言する
show "?S ∉ range f"
range f は、「f の行き先すべてを集めたもの」です。
つまりこの行は、「いま作った ?S は、$f$ の行き先のどこにも現れない」ということを示す、という宣言です。**
これが示されれば、定理の証明が終わります。
「$f$ がどこにも対応させることができない集合が存在する」ということだからです。
第３段階: 背理法で進めることを示す
assume "?S ∈ range f"
assume は「仮定する」という意味です。
ここでは、示したいことの逆を仮定しています。
「?S は $f$ の行き先に現れる」と。
これは背理法です。
逆を仮定して矛盾を導けば、もとの主張が示されます。
第４段階:対応する元を取り出す
then obtain y where "?S = f y" ..
obtain は、「そのようなものを取り出す」という意味です。
前の行で、「?S は $f$ の行き先に現れる」と仮定しました。
ならば、$f$ が ?S に対応させるような元があるはずです。
それを y と名付けています。
つまり、?S = f y です。
第５段階: y はどちらなのかを考える
then show False
proof (rule equalityCE)
False は、「矛盾」を表す記号です。
つまり show False は、「ここから矛盾を導きます」という宣言です。
背理法では、仮定から矛盾を導くことが目標でした。
その 目標 を、ここで明示しているわけです。
では、どこから矛盾を導くのでしょうか。
手元にあるのは、?S = f y という等式です。
第４段階で取り出したものです。
この等式が成り立っているとして、y 自身がどこに属するかを調べます。
問われているのは、次のことです。
「y は ?S に含まれるのか、含まれないのか」
どちらか一方であるはずです。
どちらであっても矛盾することを、これから示します。
equalityCE は、Isabelle のライブラリにある規則の名前です。
「集合が等しいという事実から、２つの場合に分けよ」という働きをします。
場合その１:y が f(y) に含まれる場合
assume "y ∈ f y"
assume "y ∈ ?S"
then have "y ∉ f y" ..
with ‹y ∈ f y› show ?thesis by contradiction
１行目:「$y$ は $f(y)$ に含まれる」と仮定します。
２行目:「$y$ は ?S に含まれる」と仮定します。
３行目が要点です。 then have "y ∉ f y" ── 「すると、$y$ は $f(y)$ に含まれないことになる」。
なぜでしょうか。
?S は「x ∉ f x を満たす x を集めたもの」でした。
$y$ がそこに含まれるなら、$y$ は当然その条件を満たします。 つまり y ∉ f y です。
４行目:with ‹y ∈ f y› ── 「１行目で仮定した『y は f(y) に含まれる』と合わせると」。
「含まれる」と「含まれない」が同時に成り立ちます。
これは矛盾です。
場合その２: y が f(y) に含まれない場合
next
assume "y ∉ ?S"
assume "y ∉ f y"
then have "y ∈ ?S" ..
with ‹y ∉ ?S› show ?thesis by contradiction
next は、「次の場合へ移る」という意味です。
１行目:「$y$ は ?S に含まれない」と仮定します。
２行目:「$y$ は $f(y)$ に含まれない」と仮定します。
３行目: then have "y ∈ ?S" ── 「すると、$y$ は ?S に含まれることになる」。
理由は、先ほどの逆です。
?S は「x ∉ f x を満たす x を集めたもの」でした。
$y$ がその条件を満たすなら、$y$ は ?S に含まれます。
４行目:「含まれない」と「含まれる」が同時に成り立ちます。やはり矛盾です。
結論
どちらの場合でも矛盾しました。
したがって、第３段階の仮定「?S は $f$ の行き先に現れる」が誤りだったことになります。
よって、?S は f の行き先のどこにも現れません。
これが、示したかったことです。
なぜ矛盾が起きるのか
改めて、?S の作り方をご覧ください。
?S は、「自分自身の行き先に含まれない要素」を集めた集合でした。
そして仮定により、?S 自身も $f$ の行き先のどこかにあり、それが f y だとしました。
すると、$y$ について次の問いが立ちます。
「y は ?S に含まれるか」
もし含まれるなら、?S の定義により、$y$ は $f(y)$ に含まれないはずです。
しかし ?S = f y なので、$y$ は ?S に含まれない**ことになります。
矛盾です。
もし含まれないなら、$y$ は $f(y)$ に含まれるはずです。
しかし ?S = f y なので、$y$ は ?S に含まれる**ことになります。
やはり 矛盾 です。
どちらに転んでも、逆の結論が出てしまう。
これが、先ほど述べた対角線論法です。
床屋の例と、比べてください
先ほどの床屋の話を、思い出してください。
「この床屋は、自分で髭を剃らない人だけの髭を剃る」
この決まりと、?S の定義を並べてみます。
| 床屋の例 | カントールの定理 | |
|---|---|---|
| 決まり | 自分で髭を剃らない人だけを剃る |
x ∉ f x を満たす x だけを集める |
| 問題になるもの | 床屋自身 |
?S に対応する元 y |
| 問い | 床屋は自分の髭を剃るか | y は ?S に含まれるか |
| 「はい」と答えると | 決まりにより、剃ってはいけない |
?S の定義により、含まれないことになる |
| 「いいえ」と答えると | 決まりにより、剃るはずである |
?S の定義により、含まれることになる |
| 結果 | どちらでも矛盾 | どちらでも矛盾 |
同じ構造です。
「自分自身」を条件の中に含めたために、どちらの答えを選んでも逆の結論が出る。
床屋の例 では、そのような床屋は存在しないという結論になりました。
カントールの定理 では、そのような $f$ は存在しないという結論になります。
つまり、「集合から、その部分集合をすべて集めたものへの全射」は、存在しないのです。
使われている語の区別
?S、y、x、f は、プログラマが任意に付けた名前です。
別の名前でも動きます。
let、show、assume、obtain、then、with、next、proof、qed は、Isar の予約語です。
他の文字列に変えると動きません。
?thesis は「いま示すべきこと」を指す、予約された記法です。
equalityCE、contradiction は、Isabelle のライブラリにある規則の名前です。
タクティク・スタイルとの比較
先ほどのタクティク・スタイル の９行を、もう一度ご覧ください。
apply (rule exI)
apply (rule notI)
apply (erule rangeE)
apply (erule equalityCE)
apply (drule CollectD)
apply (erule contrapos_np)
apply (erule imageI)
apply (erule notE)
apply (rule CollectI)
この９行のどこにも、次の情報がありません。
-
{x. x ∉ f x}という特別な集合を作ったこと - 背理法を使っていること
- $y$ という元を取り出したこと
- ２つの場合に分けたこと
- それぞれの場合で、なぜ矛盾するのか
Isar 版には、そのすべてが書かれていました。
なお、Isabelle の公式の資料集には、この Isar 版について「Isar 版は Gertrud Bauer による。元のタクティクスクリプトは Larry Paulson による」と記されています。
つまり、先に Paulson がタクティクスタイルで書いた証明を、Bauer が Isar に書き直したものです。
例その２:自動変換では、読みやすくならない
では、タクティクスタイルの証明を、機械的に宣言的スタイルへ変換すればよいのでしょうか。
そう考えた研究があります。
2026年 に発表された Apply2Isar という仕組みは、Isabelle の タクティク・スタイル の証明を、自動で Isar へ変換します。**
出典:"Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar", 2026年
この論文には、次の記述があります。
In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proof scripts since they enable rapid exploration of the search space.
（筆者による日本語訳）
**Isabelle/HOL において、Isar 言語で書かれた宣言的な証明は、その読みやすさと頑健さから広く評価されている。
しかし、探索の空間を素早く調べられるという理由で、手続き的な「apply スタイル」の証明スクリプトを書くほうを好む利用者もいる。**
（出典）
同上
この仕組みが作られたこと自体が、両者の性質の違い を物語っています。
探索の段階ではタクティクスタイルが向き、保守の段階では宣言的スタイルが向く。
その両方を得るために、自動変換という発想が生まれた のです。
ただし、機械的な変換には限界 もあります。
この点については、続編の記事で、ラグランジュの定理を例に、実際の行数の比較をお見せします。
次の記事に続きます
本記事では、定理証明支援系における２つの証明の書き方のうち、タクティク・スタイルを中心に見てきました。
処理系と対話しながら一手ずつ進められる一方、書き上がったコードからは、何を証明しようとしていたのかが読み取りにくい。
そして、その問題への答えとして生まれた 宣言的スタイル を、入口だけご紹介しました。
続編の記事では、次のことを扱います。
-
「宣言的」という言葉が、３つの違うものを指していること（SQL や React で使われる意味との違い）
-
assume、have、thusといった語が、それぞれ論証のどの働きを担っているのか
-
なぜ宣言的スタイルは読みやすいのか。その理由が、1934年の自然演繹の設計にさかのぼること
-
同じ定理を、６つの言語で書いたコードの比較（Mizar、Isabelle、Lean 4、Agda、HOL Light、Rocq）
-
30年にわたって10種類以上の実装が作られながら、広く使われているのは一つだけだという事実
- LLM が証明を書く時代に、この書き方が持つ意味
続編の記事は、以下になります。
本記事と併せてお読みいただけますと幸いです。