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

プログラミング言語「Coq」では、プログラムを「証明」して間違いを防ぐことができます。プログラムの正しさを保証できる一歩進んだエンジニアになりましょう! coqtokyoを主催する今井宜洋さんの解説です。

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

みなさん、Coqってご存知ですか? プログラムを証明して間違いを防ぐという優れものです。今回はそのCoqについて、coqtokyoという勉強会を主催している今井宜洋がお届けします。

プログラムをただ作るだけではなく、その正しさを保証できる一歩進んだエンジニアになってみましょう!

Coqって何?

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

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

1

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

2

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

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

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

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

3

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つの領域に分かれた画面が立ち上がるはずです。

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

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

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

5

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

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

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

Coqのフロントエンドとしては、CoqIDEのほかに、Proof Generalもよく利用されます。 Proof Generalは、Emacsで証明支援器を使うための汎用インターフェイスで、Coqをフルサポートするほか、Isabelleなども扱うことができます。

Emacsに慣れている人にはProof Generalをオススメしますが、本記事は軽くCoqを試したい人向けということで、CoqIDEの利用を前提に、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」と読みます。引数がどんな値であってもfgを続けて適用すればもとの値と等しくなる、というのを形式的に書いたわけです。

証明開発モード

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

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

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

6

先頭の「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という部分が、水平線の上側に移動した、つまり、仮定になったことが分かると思います。

次は、帰結にある関数fgを定義に従って展開します。そのためには、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.

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

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

エンジニアHubに会員登録すると
続きをお読みいただけます(無料)。
登録のメリット
  • すべての過去記事を読める
  • 過去のウェビナー動画を
    視聴できる
  • 企業やエージェントから
    スカウトが届く