Coqで学ぶ証明プログラミング！ テストだけでなく「証明」で安全性を保証する

Coqは、関数型プログラミング言語と仕様記述言語の特徴を持っています。Coqの中でプログラムを書いて、その正しさを「証明」できるというわけです。

ここで「証明」というのは、数学の授業でやったような「証明」と同じような作業を指しています。数学の授業では、例えば三角形の内角の和が180度になることを証明するとき、すべての三角形の内角を測ってみて180度になっているかどうかを確かめるようなことはしません（そもそも、すべての三角形を用意することなんてできません）。そうではなく、三角形の基本的な性質から導かれる事実を使った推論により、すべての三角形の内角の和に関する事実を導きます。

プログラムの正しさを証明できるというのも、これと同じように、あるプログラムに思いつく限りの値を実際に入力してみて期待する実行結果が得られるかどうかを確認するわけではありません。プログラムの部品が満たす性質から、プログラムが必ず然るべき結果になることを「証明」します。 そのようにして証明されたプログラムであれば、どのような入力がきても意図しない挙動を引き起こすことがないと分かり、安全に使えるというわけです。

そのような証明つきのプログラムを書くことにCoqで挑戦してもらうことが、この記事のひとつの目標です。

プログラムを「証明する」ってどういうこと？

関数を定義してプログラムを組み立てていくという点では、Coqは多くのプログラミング言語と同様です。その上でCoqでは、定義した関数の性質を数学的に述べて、それを証明することができます。

また、定義した関数を他のプログラミング言語のソースへ変換するExtractionと呼ばれる機能があります。これによって、既存のプロジェクトなど大きいシステムのうち、関数1つをCoqで検証するということが可能になっています。

Coqを使ってみよう

Coqのインストール方法

Coqの開発はGitHub上で行われており、ソースコードだけでなくWindowsやmacOSのインストーラも、GitHubのリリースページから入手できます。

WindowsやmacOSの場合には、上記からインストーラを入手して実行すれば、必要なものはすべてインストール完了です。

それ以外のOS（Linuxなど）では、各OSのディストリビューションのパッケージマネージャー（aptやRPM）経由か、OPAMからインストールすることもできます。

OPAMは、Coqの実装に使われているプログラミング言語OCamlのパッケージマネージャで、利用できる環境では次のように必要なパッケージをインストールできます。

opam install coq

CoqIDE：Coqによる証明開発のフロントエンド

Coqによるプログラミングで実際にやることを大雑把に要約すると、次のような工程に分けられます。

1. 関数の定義を書く
2. 1で定義した関数についての定理を書く
3. 2の定理に対する証明を書く
4. 証明済みの関数を安心して使ったり、他のプログラミング言語に書き出したりする

定理を与えるだけでCoqが勝手に証明してくれれば楽なのですが、それは不可能です。上記のうち、3での証明は人が与える必要があります。ただし、Coqには証明を楽に進めるための仕組みがあります。そのように証明を支援してくれる環境ということで、Coqは「証明支援器」と呼ばれています。

Coqによる支援を受けるときは、Coqとの対話的なやり取りのためのフロントエンドを使います。そうしたフロントエンドの1つが、ここで紹介するCoqIDEです。

WindowsやmacOSでインストーラを使ってCoqをインストールすれば、このCoqIDEも一緒にインストールされます。さっそくCoqIDEを起動してみてください。次のような3つの領域に分かれた画面が立ち上がるはずです。

• 左側全体を占めるいちばん大きな領域は、script buffer（スクリプトバッファ）といい、ここにプログラムと証明を書いていきます。
• 右側の上の領域はgoal window（ゴールウィンドウ）といい、その段階までに証明済みであると仮定できること（仮定）と、残りの証明すべきこと（サブゴール）が表示されます。
• 右側の下の領域には、コマンドの実行に応じたメッセージや、エラーが表示されます。

「スクリプトバッファに何を書けばいいのか」、そして「ゴールウィンドウにどんなふうに情報が表示されるか」は、次節で、簡単なプログラムと証明の開発例を通して説明していきます。

CoqIDEの説明を終える前に、画面の上側に並んでいるボタンのうち、上下矢印の使い方について説明しておきましょう。下向きの矢印はForward one command、上向きの矢印はBackward one commandと呼びます。

この図はWindows版のCoqIDEで、上下矢印が緑色になっています（環境によってはボタンの色が違うこともあるようです）。

Forward one commandボタンは、文字通り、スクリプトバッファに書いたコマンドを1つ実行するために使います。このボタンを押すたびに、まだ実行されていないコマンドが1つずつ実行されます。Backward one commandボタンは、逆に、コマンドの実行を1つ巻き戻すのに使います。

なお、この記事で「コマンド」と言っているのは、Coqでプログラムと証明を書くための特別な言語から利用できる、これまた特別な命令のようなものだと考えてください。

Coqで関数プログラミング

Coqを使ってプログラムを書くときは、高階関数、再帰による繰り返し、パターンマッチによる場合分けなどを使います。こうしたプログラミングの方法になじみがない方は、いわゆる関数型プログラミングの入門記事などを参照してみてください。例えば、過去のエンジニアHubで掲載されたElixirの入門記事やHaskellの入門記事に一通り目を通してみることをお勧めします。

準備ができたら、Coqで初めての関数を定義してみましょう。「引数に100を足す」という単純な関数fをCoqで書くには、次のようにします。

Require Import Arith.
Definition f x := x + 100.

1行目では、数値を扱うために、標準ライブラリにある自然数モジュールArithをインポートしています。Arithのような、既存のモジュールをインポートするには、このようにRequire Importというコマンドが使えます。このコマンドを一回書けば、以降の行で、そのモジュールを使用できるようになります。

2行目が関数fの定義になります。Coqで関数を定義するときは、このように、Definitionコマンドを使います。

Definitionコマンドで、xや戻り値の型を特に書いていないことに注目してください。このように書けば、「関数fは自然数から自然数への関数である」と型推論されます。

さっそく、この関数fを使った式を評価してみましょう。式の計算は次のようにします。

Compute f 10.

CoqIDEでは、上下の矢印ボタンにより、コマンドを段階的に実行できます。うまく動いていれば、右下のメッセージが表示される領域に、次のような結果が現れるはずです。

     = 110
     : nat

期待どおりに動いているようですね。

次項から、いよいよプログラムに対する証明を開発していきます。

プログラムの仕様を記述しよう

前に触れたとおり、ここまでは普通の関数型言語でのプログラミングによく似ています。しかし、Coqでは、普通じゃできないこと、つまり、「プログラムを証明する」ことができます。

プログラムを証明するというからには、まず「何を証明するか」を決めないといけませんよね。ほかの形式的な手法でも同様ですが、この証明したい性質をうまく設計することが、高信頼なプログラムを作る上で重要です。ここでオススメしたいのは、プログラムの全体の仕様を最初からまるごと証明しようと思わないことです。一般的には証明は困難なことが多いですし、数学的に完全な仕様を書き下すこと自体が大変だったりします。

そこで、ここではCoqで初めての証明の題材として、数学的に書き表しやすい性質を考えてみましょう。まず、次のような関数gの定義を追加します。

Definition g x := x - 100.

見てのとおり、gは、「引数から100を引く」という関数です。

ここで、先ほど定義した関数fのことを思い出してください。fは、「引数に100を足す」関数でした。したがって、もしfに続けてgを適用したら、もとの引数の値になってほしいところです。

fが100足す関数で、gが100引く関数なので、このことは明らかに正しそうです。ですが、それではこの性質が正しいかどうかを保証したことなりません。

そこで、「g (f x)がxにいつでも等しくなる」かどうかを、Coqで証明してみることにしましょう。こういう数学的に書き表しやすい性質は、Coqでの検証に向いています。

Coqでは、Theoremコマンドによって、「証明開発モード」というものに移行できます。Theoremコマンドに続けて、Coqで証明したい性質（定理）を書き出します。

Theorem 定理名 : 成り立ってほしい性質.

いまの例の場合は、次のようにすればいいでしょう。

Theorem g_f : forall x, g (f x) = x.

この定理は、「任意のxにおいて、g (f x) = x」と読みます。引数がどんな値であってもfとgを続けて適用すればもとの値と等しくなる、というのを形式的に書いたわけです。

証明開発モード

それでは、この定理の証明を与えていきましょう。多くの場合、定理と証明は次のような見た目になるようにします。

Theorem 定理名 : 成り立ってほしい性質.
Proof.
  証明
Qed.

前項の最後に書いたTheorem g_f : forall x, g (f x) = x.の次の行にProof.と書いて、CoqIDEの緑矢印ボタンで実行を進めてみてください。Theoremコマンドによって証明開発モードになっているので、いままで何も表示されていなかった右上のゴールウィンドウに次のような表示が現れるはずです。

先頭の「1 subgoal」は、この段階で証明すべきサブゴールが1つであることを示しています。

この画面で注目してほしいのは、水平線の上下に示されている情報です。いまは、水平線の上側は空になっています。そして、水平線の下側に、証明しようとしている定理の全体がある状態です。Coqの証明開発モードでは、この水平線の上側に「現時点で自分が使える変数や仮定」、下側には「示すべき帰結（conclusion）」が表示されることになっています。ここに表示される情報を見ながら、対話的に証明を開発していくのです。

ここから先の説明では、このゴールウィンドウの状態を、模式的に次のように表すことにします。

1 subgoal
  
  ============================
  forall x : nat, g (f x) = x

ゴールを目指して証明しよう

それでは、証明開発モードで証明を対話的に考えていきましょう。Coqで証明を開発するときには、タクティックという道具を使います。

この場面でまず使ってみるのは、introsというタクティックです（これまでのコマンドと違って、ほとんどのタクティックは小文字で始まります）。いまの例のように帰結がforallで始まる場合、introsタクティックにより変数を水平線の上側に移動させることができます。スクリプトバッファに次のように追記してください。

intros x.

そうしたら、CoqIDEのForward one commandボタン（下向きの緑矢印ボタン）を使って、いま追記したintrosタクティックを使用してみましょう。ゴールウィンドウの表示が次のように変化したでしょうか？

1 subgoal
  
  x : nat
  ============================
  g (f x) = x

上下のボタンを押してみて、タクティクの使用前と使用後のゴールウィンドウの形を比べてみてください。何が起きているか確認できるでしょう。introsタクティクの使用前には帰結の一部だったx:natという部分が、水平線の上側に移動した、つまり、仮定になったことが分かると思います。

次は、帰結にある関数fとgを定義に従って展開します。そのためには、unfoldというタクティックを使います。次のようにカンマで区切って指定することで、複数の関数を展開できます。

unfold f, g.

上記をスクリプトバッファに追記したら、再びForward one commandボタンを押してみてください。帰結のfおよびgが定義に従って展開されて、ゴールウィンドウの表示が次のように変化したでしょうか？

1 subgoal
  
  x : nat
  ============================
  x + 100 - 100 = x

ここまでくると、あとは単に変数を含む数値演算の性質の証明になります。帰結の左辺を見ると、100という数を足してから引いているので、必ずxと同じ値になりそうです。もちろん、「なりそう」というだけではだめなので、本当にその性質が成り立つかどうか、やはり証明が必要になります。

実は、そういう補題は、すでにCoqの標準ライブラリで証明されています。そこで、そういう補題を標準ライブラリから探す方法と、探し出した補題を自分の証明で使う方法を説明しましょう。

いまの例のように、部分的な置き換えに関して成り立つような性質を利用したい場合は、等式の形をしている定理や補題を探すことになります。そのためには、SearchRewriteというコマンドが使えます。「何かに何かを足した後で引く」という形の定理を見つけるには、SearchRewriteコマンドに「(_ + _ - _)」というクエリを指定します。

SearchRewrite(_ + _ - _).

この例のように、「なんでもよい」という部分を表すにはアンダースコア「_」を使います。

上記をスクリプトバッファに追記したら、Forward one commandボタンを押してみてください。すると、CoqIDEの画面で右下の領域に、次のようなメッセージが表示されるはずです。

Nat.add_sub: forall n m : nat, n + m - m = n
minus_plus: forall n m : nat, n + m - n = m
minus_plus_simpl_l_reverse: forall n m p : nat, n - m = p + n - (p + m)
Nat.add_sub_swap: forall n m p : nat, p <= n -> n + m - p = n - p + m
Nat.add_sub_assoc: forall n m p : nat, p <= m -> n + (m - p) = n + m - p

これらが、標準ライブラリにある「証明済み」の定理のうち、「何かに何かを足した後で引く」という形をしたものというわけです。ここでは、5つの定理が見つかりました。

このうち、いまの例で使えそうなのは、一番めに表示されているNat.add_subという名前の定理です。等式の定理を使って現在の帰結の一部を置き換えたいときは、rewriteというタクティックを使います。スクリプトバッファに次のように追記して、この定理を使ってみましょう。

rewrite Nat.add_sub.

すると、定理Nat.add_subにより、ゴールウィンドウに表示されていた帰結x + 100 - 100 = xの左辺がxという簡単な式に置き換わります。結果として、帰結は、見るからに同じx = xという等式になりました。

1 subgoal
  
  x : nat
  ============================
  x = x

このような、左辺と右辺が見るからに同じ等式は、reflexivityタクティックを使って証明を終わらせることができます。

reflexivity.

Forward one commandボタンを押すと、ゴールウィンドウには次のように表示されます。

No more subgoals.

最後にQed.と書けば、定理g_fの証明は完成です。現在のスクリプトバッファの状態は次のようになっているはずです。

Require Import Arith. 
Definition f x := x + 100.
Definition g x := x - 100.
Compute f 10.

Theorem g_f : forall x, g (f x) = x.
Proof.
  intros x.
  unfold f, g.
  SearchRewrite(_ + _ - _).
  rewrite Nat.add_sub.
  reflexivity.
Qed.

タクティックは1行に複数書くこともできるので、最終的に以下のように定理と証明を整理するとよいでしょう。

Theorem g_f : forall x, g (f x) = x.
Proof.
  intros x. unfold f, g.
  rewrite Nat.add_sub. reflexivity.
Qed.

以上で、関数fとgに関する網羅的な性質が証明できたことになります。

再帰的に定義された関数の証明：reverseの例

前節では、整数の引数に100を足したり引いたりする関数fとgを使って、Coqによる証明開発を体験してみました。ここからは、もう少し難しい例として、リストに対する処理を扱ってみましょう。アルゴリズムも、もう少し複雑にしてみます。

題材は、リストを反転させるreverse関数です。もちろん、単にreverseの機能を実装するだけでなく、「証明されたreverse関数」を開発していきます。

Coqで再帰的な関数定義をする

とはいえ、まずはリストを反転させる関数の定義です。多くの関数型言語でリストの反転関数を定義するときと同様に、再帰的に定義します。

まず、今回は整数ではなくリストを扱うので、ListモジュールをインポートするためにRequire Import List.とします。さらに、[1;2;3]のような表記でリストを表せるように、ListNotationsというモジュールもインポートしてください。

Require Import List.
Import ListNotations.

それではreverse関数を定義しましょう。Coqでシンプルな再帰関数を定義するには、次のようにFixpointコマンドを使います。

Fixpoint reverse {A : Type} (xs : list A) :=
  match xs with
  | nil => nil
  | x :: xs' =>
    reverse xs' ++ [x]
  end.

{A:Type}の部分は、「型変数がある」くらいの理解で十分です。処理そのものは、リストxsのtail側（xs'）を再帰呼出しで反転し、その右側にリストのheadであるxを追加する、というコードになっています。++によりリストを連結（append）しています。

前と同様にComputeコマンドを使って、定義したreverse関数の動作を確かめてみましょう。

Compute reverse [1;2;3].

CoqIDEの下矢印ボタンを押すと、メッセージ領域に次のように表示されるはずです。

     = [3; 2; 1]
     : list nat

期待どおりに動いているようですね。

reverse関数の性質を定理にしよう

ここまでは、よくある関数型言語における開発と同じです。ここからは、いま定義したreverse関数の振る舞いについて「証明」してみましょう！ reverse関数が満たしてほしい性質はなんでしょうか？ 皆さんなら、どんな性質が保証されていてほしいですか？ ここでは、「reverseを2回施すと元に戻る」という性質を証明してみることにしましょう。

「reverseを2回施すと元に戻る」という性質をCoqの定理として書くと、次のようになります。

Theorem reverse_reverse : forall (A : Type) (xs : list A),
    reverse (reverse xs) = xs.

ここで証明したい性質は、型がリストであるような値であれば何を入力としてもってきても成り立ってほしいので、forall (A : Type) (xs : list A)としています。そのような値xsについてreverse (reverse xs) = xs.が成り立つ、ということを、reverse_reverseという定理として定義したわけです。

このような性質は、論理式にしてみると、このようにシンプルに書けます。言い換えると、このような定理の宣言は、「このコードについてこんな性質が成り立つ」という事実を簡潔に表したものです。そのため、取引先や株主のような非技術者にもぜひ見てほしい部分だといえます。実際、筆者は、開発した証明付きプログラムから定理の宣言だけを抜き出す方法（coqdocの-gオプション）を使って文書化することがあります。

reverse関数の性質を証明しよう

reverse_reverseでは、入力として任意のリストを考えます。ということは、整数のリスト、文字列のリスト、場合によってはタプルのリストや、リストのリスト、さらには関数のリストなんてものまであり得るということです。

とはいえ、リストは、中身がなんであれheadとtailにより帰納的に構成されています。そのような型で再帰的に定義された関数についての性質を証明するときには、しばしば帰納法が効果的です。高校の数学でやった数学的帰納法を思い出す方もいるでしょう。リストに関しても、あれと同様の方針で、すべてのリストに関する性質を証明することができます。

さっそく、スクリプトバッファにProof.と書いて下矢印ボタンを押し、対話的な証明開発を始めましょう。

1 subgoal
  
  ============================
  forall (A : Type) (xs : list A), reverse (reverse xs) = xs

forallなので、前回の証明と同じように、まずはintrosタクティックを使います。今回は次のようにしてください。

intros A xs.

下矢印ボタンを押すと、ゴールウィンドウの表示が次のようになるはずです。

1 subgoal
  
  A : Type
  xs : list A
  ============================
  reverse (reverse xs) = xs

第1引数のリストxsに関して再帰する状況なので、ここでxsに関する帰納法を使います。帰納法を使うときのタクティックは、inductionです。

induction xs.

スクリプトバッファに上記のように追記したら、下矢印ボタンを押してください。ゴールウィンドウの表示が次のようになるはずです。

2 subgoals
  
  A : Type
  ============================
  reverse (reverse []) = []

subgoal 2 is:
  reverse (reverse (a :: xs)) = a :: xs

これまでの例では、すべて1行目が「1 subgoal」となっていましたが、ここで初めて「2 subgoals」となりました。これは、2つのサブゴールが生まれたことを意味しています。

サブゴールが2つということは、この段階で証明すべきことが2つあるということです。具体的には、次の2つの証明を与える必要があります。

1. リストxsが空リストの場合にreverse (reverse xs) = xsが成り立つか、つまり、reverse (reverse []) = []が成り立つか
2. 空でないxsについてreverse (reverse xs) = xsが成り立つか、つまり、reverse (reverse (a :: xs)) = a :: xsが成り立つか

複数のサブゴールを場合分け

Coqでサブゴールごとに分けて証明をしていくときは、bulletという道具を使います。bulletとしては、「-」、「+」、「*」の記号が使えます。 ここでは「-」を使うことにします。スクリプトバッファに「-」とだけ書いて下矢印ボタンを押してください。

-

すると、1つめのサブゴールに対する証明の開発が続行されます。

1 subgoal
  
  A : Type
  ============================
  reverse (reverse []) = []

1つめのサブゴールは、リストxsが空の場合です。この場合は、具体的に計算をすることで、性質が成り立つかどうかを確かめられそうです。計算を進めるためにはsimplタクティックを使います。

simpl.

下矢印ボタンを押すと、次のような自明な等式が出てきます。

1 subgoal
  
  A : Type
  ============================
  [] = []

自明な等式なので、前回と同様にreflexivityを使って証明を完了しましょう。

reflexivity.

これで無事に1つめのサブゴールが完了しました。

This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet -.

1 subgoal

subgoal 1 is:
 reverse (reverse (a :: xs)) = a :: xs

今度は2つめのサブゴールを証明します。証明するサブゴールを変えるために、再びスクリプトバッファにbullet「-」を打ちましょう。

-

下矢印ボタンを押すと、2つめのサブゴールがゴールウィンドウに表示されます。水平線の上側の仮定がいままでよりも多く、少し複雑な見た目をしていますね。

1 subgoal
  
  A : Type
  a : A
  xs : list A
  IHxs : reverse (reverse xs) = xs
  ============================
  reverse (reverse (a :: xs)) = a :: xs

2つめのサブゴールの帰結では、リストがa :: xsという形になっています。いまは単なる場合分けではなく、リストに対する帰納法の途中なので、「1つ小さいリストに関して性質が成り立っている」という仮定が使えます。実際、ゴールウィンドウの水平線より上側の仮定の部分に、a :: xsよりも1つ小さいリストxsに対して性質が成り立つという仮定「reverse (reverse xs) = xs」が、IHxsという名前で含まれていますね。

ここでも、とりあえず計算を進められる部分がないかどうか、まずはsimplタクティックを試してみましょう。

simpl.

下矢印ボタンを押すと、ゴールウィンドウの表示が次のようになります。

1 subgoal
  
  A : Type
  a : A
  xs : list A
  IHxs : reverse (reverse xs) = xs
  ============================
  reverse (reverse xs ++ [a]) = a :: xs

帰結の内側のreverse関数の部分が少し変形しました。

しかし、このままでは帰納法の仮定IHxsをそのまま使うことはできなそうです。次に何をすればよいかも自明ではありません。reverse( ＿++＿ )という形の式を分解する補題が欲しい気がします。

こういうときは、そういう分解ができるような等式の定理がすでに存在するかどうか、とりあえず検索してみましょう。等式の証明を検索するにはSearchRewriteコマンドを使うのでしたね。

SearchRewrite (reverse (_ ++ _)).

しかし、この場合には、残念ながら何も見つかりませんでした。

補題を考えて証明する

こういうときは、reverse_reverseの証明はひとまず諦めます。代わりに、証明したい定理に必要な補題を考えて、まずはその補題の証明を開発しましょう。

スクリプトバッファで定理reverse_reverseを定義した前の行に戻り、次のような補題reverse_appendを用意してください。

Lemma reverse_append : forall (A : Type) (xs ys : list A),
    reverse (xs ++ ys) = reverse ys ++ reverse xs.

この補題では、「2つのリストを結合したあとに反転させることは、それぞれリストの反転結果を左右逆に結合させる結果と同じになる」と言っています。これを証明できれば、その結果を使って、reverse_reverseの証明を続行できそうですね。

では、補題reverse_appendを証明していきましょう。これもリストxsに関する帰納法で証明します。

1 subgoal
  
  ============================
  forall (A : Type) (xs ys : list A),
  reverse (xs ++ ys) = reverse ys ++ reverse xs

まずは、やはり冒頭にforallがあるので、introsタクティックを使いましょう。

intros A xs ys.

いつものとおり、ゴールウィンドウが次のように変化します。

1 subgoal
  
  A : Type
  xs, ys : list A
  ============================
  reverse (xs ++ ys) = reverse ys ++ reverse xs

ここでxsに関する帰納法を開始します。帰納法を使うためのタクティックはinductionでしたね。

induction xs.

すると、やはり2つのサブゴールに分かれます。

2 subgoals
  
  A : Type
  ys : list A
  ============================
  reverse ([] ++ ys) = reverse ys ++ reverse []

subgoal 2 is:
 reverse ((a :: xs) ++ ys) = reverse ys ++ reverse (a :: xs)

先ほどと同様に、bulletとして「-」を使います。最初のサブゴールでsimplをして計算できるところを計算してしまいたいので、次のように一気に書いてしまいましょう。

- simpl.

これでゴールウィンドウは次のようになるはずです。

1 subgoal
  
  A : Type
  ys : list A
  ============================
  reverse ys = reverse ys ++ []

これはもう、ほとんど自明な等式に見えます。しかし、単にsimplをしても、これ以上には簡略化できません。なぜかというと、Listモジュールの++演算子は、左側のリストに関して再帰的に計算を行うからです。

でも、こういうパターンは一般的によくありそうなので、すでに補題がどこかにあるかもしれません。SearchRewriteで探してみましょう。

SearchRewrite(_ ++ []).

今度は次のような候補が見つかりました！

app_nil_end: forall (A : Type) (l : list A), l = l ++ []
app_nil_r: forall (A : Type) (l : list A), l ++ [] = l

ここでは、このうちapp_nil_rを使って帰結を書き換えてみましょう。

rewrite app_nil_r.

下矢印ボタンを押すと、ゴールウィンドウの表示が次のように変わります。

1 subgoal
  
  A : Type
  ys : list A
  ============================
  reverse ys = reverse ys

これはもう自明な等式なので、reflexivityで証明完了です。

reflexivity.

すると、次のサブゴールが表示されます。次のサブゴールは、「左側のリストが(a :: xs)の場合」です。

This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet -.

1 subgoal

subgoal 1 is:
 reverse ((a :: xs) ++ ys) = reverse ys ++ reverse (a :: xs)

先ほどと同様に、bullet「-」とsimplによる計算を一度に済ませましょう。

- simpl.

帰納法の仮定を含む、次のようなサブゴールが現れます。

1 subgoal
  
  A : Type
  a : A
  xs, ys : list A
  IHxs : reverse (xs ++ ys) = reverse ys ++ reverse xs
  ============================
  reverse (xs ++ ys) ++ [a] = reverse ys ++ reverse xs ++ [a]

帰結の左辺は、仮定IHxsの左辺と同じ式です。rewriteしていきましょう。

rewrite IHxs.

サブゴールが次のような形に変わります。

1 subgoal
  
  A : Type
  a : A
  xs, ys : list A
  IHxs : reverse (xs ++ ys) = reverse ys ++ reverse xs
  ============================
  (reverse ys ++ reverse xs) ++ [a] = reverse ys ++ reverse xs ++ [a]

いま、帰結の左辺と右辺がほとんど同じになっています。しかし、微妙に違うところがあります。それは、カッコの有無です。3つのリストをどちら側から先に結合するかの順番が違うわけです。

とはいえ、++による結合は順番にかかわらず同じ結果になるはずです。しかし、そのような++の性質も証明が必要です。すでに証明されていないかどうか、補題を探してみましょう。

SearchRewrite((_ ++ _) ++ _).

次のような補題が見つかりました。

app_assoc_reverse:
  forall (A : Type) (l m n : list A), (l ++ m) ++ n = l ++ m ++ n
app_assoc: forall (A : Type) (l m n : list A), l ++ m ++ n = (l ++ m) ++ n

2つの補題が見つかりました。ここでは、app_assocの方を使うことにします。

rewrite app_assoc.

これで下矢印ボタンを押すと、帰結の左辺と右辺がまったく同じ形になります。

1 subgoal
  
  A : Type
  a : A
  xs, ys : list A
  IHxs : reverse (xs ++ ys) = reverse ys ++ reverse xs
  ============================
  (reverse ys ++ reverse xs) ++ [a] = (reverse ys ++ reverse xs) ++ [a]

いつものようにreflexivityで証明完了です。

reflexivity.

サブゴールがすべてなくなり、補題reverse_appendが証明できました。

No more subgoals.

補題reverse_appendとその証明のコードを下記にまとめます。

Lemma reverse_append : forall (A : Type) (xs ys : list A),
    reverse (xs ++ ys) = reverse ys ++ reverse xs.
Proof.
  intros A xs ys. induction xs.
  - simpl.
    rewrite app_nil_r. reflexivity.
  - simpl.
    rewrite IHxs.
    rewrite app_assoc. reflexivity.
Qed.

定理reverse_reverseの証明を完了させる

さて、これでようやく本題に戻って、先ほど中断させていた定理reverse_reverseの証明を先に進められます。先ほどは次のようなサブゴールで中断していました。

1 subgoal
  
  A : Type
  a : A
  xs : list A
  IHxs : reverse (reverse xs) = xs
  ============================
  reverse (reverse xs ++ [a]) = a :: xs

ここで、補題reverse_appendを使ってみましょう。

rewrite reverse_append.

すると、ゴールウィンドウの表示が次のように変わります。

1 subgoal
  
  A : Type
  a : A
  xs : list A
  IHxs : reverse (reverse xs) = xs
  ============================
  reverse [a] ++ reverse (reverse xs) = a :: xs

ここで、仮定IHxsが帰結の一部に出てきました。この仮定をrewriteで使ってみるとどうなるでしょうか？

rewrite IHxs.

帰結の左辺が次のように変化します。

1 subgoal
  
  A : Type
  a : A
  xs : list A
  IHxs : reverse (reverse xs) = xs
  ============================
  reverse [a] ++ xs = a :: xs

reverse [a] ++ ... の部分は単純に計算できそうです。simplタクティックで計算を進めてみます。

simpl.

すると、帰結の右辺と左辺が等しくなりました！

1 subgoal
  
  A : Type
  a : A
  xs : list A
  IHxs : reverse (reverse xs) = xs
  ============================
  a :: xs = a :: xs

よさそうです。証明を完了しましょう。

reflexivity.

無事にサブゴールがすべてなくなりました。

No more subgoals.

定理reverse_reverseの最終的な証明は次のようになります。

Theorem reverse_reverse : forall (A : Type) (xs : list A),
    reverse (reverse xs) = xs.
Proof.
  intros A xs. induction xs.
  - (* 空リスト *)
    reflexivity.
  - (* それ以外 *)
    simpl.
    (* make a Lemma reverse_append *)
    rewrite reverse_append. rewrite IHxs. simpl.
    reflexivity.
Qed.

Coqでは、(*と*)で囲んだ部分がコメントになります。

これで、「どんなリストであっても、関数reverseを2回連続して適用すれば、元の姿に戻る」という性質が証明できました。このように抽象度の高いプログラムの性質は、具体的な値を与えてテストしてみるだけでは完全に保証することが難しい場合もあります。

一方、証明では、プログラムを抽象的なまま扱えます。関数型言語の影響もあって、抽象度の高いプログラミングスタイルが採用されるケースも増えています。具体的なテストに加えて、このような検証が重要になる場面は、これからますます多くなるでしょう。

このように、簡潔に述べられる純粋な関数の性質は証明に向いています。このような網羅的な性質を、テストで保証するのは不可能です。

逆に、DBの読み書きやHTTP接続などを含んだ大きな処理全体の検証は、しばしば困難です。シナリオテストや単体テストで補強しましょう。

で、Coqは何に使えるの？

この記事では、Coqを使って簡単なプログラム（関数）と証明を開発してみましたが、いかがでしたでしょうか。CoqIDEの使い方や、関数を定義して証明を与える流れは体験できたけど、「これが現実世界のプログラミングで何の役に立つのかなあ？」と感じた人も少なくないと思います。

安全性の検証や脆弱性の発見に役立つ

実際、Coqを使ってゼロから商用のアプリケーションを書くというのは、あまり現実味はありません。むしろCoqが威力を発揮するのは、そうしたアプリケーションやシステムそのものに対する安全性の検証や、未知のバグや脆弱性の発見といった場面です。

例えば、Coqを開発しているInria（フランス国立情報学自動制御研究所）では、エアバス社と一緒に、安全なCコンパイラの処理系であるCompCertを開発しています。

▼ CompCert - Inria

また、Rust処理系の形式化と標準ライブラリの検証を行うRustBeltというプロジェクトもあります。

▼ RustBelt: Securing the Foundations of the Rust Programming Language (POPL 2018)

国内では、産業技術総合研究所がCプログラムの検証などに利用していたり、株式会社レピダムがOpenSSLの脆弱性を発見したりしています。

CCS Injection脆弱性(CVE-2014-0224)発見の経緯についての紹介｜株式会社レピダム

Webサービスにおける応用としては、株式会社ドワンゴによるニコニコ動画や生放送の基盤システムに対する形式検証プロジェクトでCoqが使われており、筆者も証明を手伝っています。

もちろん、証明を本業とする数学の研究でも、Coqは利用されています。何百年ものあいだ数学者たちが議論を重ねてきた「四色定理」にも、2004年にCoqによる証明が与えられています¹。

他の関数型言語のコードとして書き出す

冒頭でも触れたように、Coqで開発した証明つきの関数は、他の関数型言語のコードとして書き出して利用することも可能です。例えば、この記事で開発したreverse関数の定義と証明のあとに次のように記述すれば、「Coqによって証明済みのリスト反転関数」のOCamlコードが手に入ります。

Require Extraction.
Extraction Language OCaml.

Extraction "reverse.ml" reverse.

標準では、OCamlのほか、HaskellやSchemeのコードを抽出できます。

もっと証明したい人のための情報

最後に、もっと証明したい人のための情報を少しだけ紹介します。

教科書・参考書

現在のところ、Coqを本格的に使いたいとなると、英語の本にあたることになります。

少し古いものの、いまもって堅実なCoqの教科書は“Interactive Theorem Proving and Program Development”、通称「Coq'Art」です。

▼ Coq'Art Home page

一方、より現代的なCoqの応用まで踏み込んだ教科書として“Certified Programming with Dependent Types”、通称「CPDT」があります。

▼ Certified Programming with Dependent Types

日本語の書籍としては、2018年4月に『Coq/SSReflect/MathCompによる定理証明』（萩原学、アフェルト・レナルド共著）が森北出版より発売されています。四色定理の証明のために開発されたSSReflectというCoqの拡張を使い、「数学の証明をプログラムでするとはどういうことか」を説明した内容になっています。

Coq/SSReflect/MathCompによる定理証明 | 森北出版株式会社

SSReflectはタクティクなどがCoqのオリジナルとは異なりますが、Coqによる証明開発の雰囲気を日本語でさらに味わう解説書として参考になると思います。

Webで読めるドキュメント

Web上で読める教科書として、『型システム入門』の著者であるBenjamin C. Pierce氏らが執筆とメンテナンスを続けている“Software Foundations”があります。プログラムの安全性に対する数学的な基礎が、すべて無料で学習できます。

▼ Software Foundations - University of Pennsylvania

筆者らが『ソフトウェアの基礎』として翻訳したものもあります。原文に比べると少し古いバージョンですが、独習できる数少ない日本語のCoq解説です。

▼ ソフトウェアの基礎 - ProofCafe

池渕未来氏による解説記事「プログラミングCoq」も、本記事と合わせて読むと理解が深まるでしょう。しばらく閲覧できなくなっていましたが、今年になって復活しました。

▼ プログラミング Coq - IIJ Innovation Institute

勉強会や学習サイト

実際にCoqを使っている人や習得中の人と一緒に学びたい人は地域の勉強会に参加するのもよいでしょう。私の知っている範囲では、銀座と名古屋にCoqの勉強会が存在します。

主に銀座で開催されるcoqtokyoによるreadcoqartという勉強会では、Coqだけでなく、圏論などの数学も取り上げることがあります。名古屋を拠点とするProofCafeでは、名古屋のエンジニアや学生が集まってCoqを学んでいます。

最後に、宣伝になってしまいますが、筆者も講師として参加している「トップ エスイー」という教育プログラムでは「定理証明と検証」という講義を実施しています。

「定理証明と検証」講義 - トップ エスイー

より本格的にプログラムの証明について学びたい方向けの選択肢として紹介しておきます。

今井 宜洋（いまい・よしひろ） @yoshihiro503 yoshihiro503

株式会社ドワンゴで、ニコニコ動画や生放送における基盤システムの開発・形式検証を担当するかたわら、名古屋大学やトップエスイーで客員教員を務める。 著書・訳書に『入門OCaml』（2007年、毎日コミュニケーションズ ）『型システム入門』（2013年、オーム社）がある。

編集協力：鹿野桂一郎（しかの・けいいちろう、 @golden_lucky） {$image_23}技術書出版ラムダノート