Haskell
Coq
Agda
定理証明

目的

定理証明支援とは何かと現状の整理。

定理証明支援とは

定理証明支援とは数学の定理を自動で証明することではなく、ステップバイステップでコンピュータに命令を送り、数学の定理を証明するのを助けるシステムである。

支援だから意味ないということでなく、最近の数学の証明は長くなり証明の検証が難しいのを助ける意味がある。定理証明支援の意義についてはこちらが詳しい。
また、信頼性が求めらる難しいアルゴリズムの検証、たとえばTLS(暗号通信)やRaft(分散合意アルゴリズム)のサーバーに利用されつつある。

ここでいう定理は大げさなものだけでなく、$1+1=2$、$0*何か=0$、$a*b=b*a$といった簡単なものを証明しながらどんどん積み上げていく。通常のプログラムと違うのは証明であるので使用する変数が整数ならそのすべての値について成り立つ定理を証明する。

定理を証明するのに使うツールは下記である。(他にもあるとは思いますが。)

Inductive nat : Set := 
  | O : nat
  | S : nat -> nat.

証明のやり方

証明の具体的なやり方は次の入門書を直接読むのがいいです。
さまざまな言語による証明の例にあるように言語により証明のスタイルが異なります。下記のように2つあります。

  1. Coqのように数式と証明用の言語が完全に分離していて、数式はGallina、証明はtacticsという言語で書く。
  2. Agdaのようにカリー=ハワード同型対応を生かしているのか、数式が型、証明がプログラム。

どちらがいいのかよくわかりませんが、どちらも証明でやっていることは既存の定義や仮説の式を置き換えたり、つなげたりしてゴールの証明を目指します。証明はテトリスのように組み合わせゲームです。
Coqはtacticsが多すぎて既存のソースが大変読みにくく、Agdaのほうが読みやすいと思います。

入門書

  • Coq
    • Software Foundation
      • 英語ですがわかりやすいです。最近3部だてに分かれたようです。
      • 日本語訳
        • 2011と、かなり古い訳です。
    • Mathematical Components
      • 素のCoqはtacticsが多く、可読性が悪いのでSSReflectというマクロのようなもの?を使い、証明の可読性をあげ、大規模プロジェクトに耐えられるようなスタイルに変わってきています。SSReflectの使い方の本です。
  • Agda
  • Haskell
    • Dependent Type in Haskell
      • 依存型の書き方の本。途中まで読みやすいですが、後半はわかりにくいです。

各言語の状況

  • Coq
    • 歴史が長い分ドキュメントとエコシステムが充実(日本語のドキュメントは少ないです。)
    • パッケージマネージャー
      • ocamlと同じopam
    • 信頼の実績
      • 四色問題の証明など多数
  • Agda
    • ドキュメント少ないです。
    • ライブラリ管理機能が最近追加されたが、cabalとかに比べると貧弱
  • Haskell
    • 簡単な証明はできますが、私が勉強不足でrewriteとかどうやるのかどうやるのかわかっていません。