定理証明支援の紹介

目的

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

定理証明支援とは

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

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

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

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

• 数学的帰納法
• 命題論理
  • 演繹定理
  • 数学記号の表
  • シークエント計算
• ペアノ数に代表される帰納的な変数
  • 下記のcoqの例のように自然数を0と+1（S)のように帰納的に定義し、プログラムで容易に条件を網羅できる変数を扱う。自然数の場合は2つのケースしかない。
  • 実数の取り扱いは難しく、デフォルトでサポートされないケースが多い。
• カリー＝ハワード同型対応

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
  • Programming Language Foundations in Agda
    • 最近(2018)に作られた参考書
  • Verified Functional Programming in Agda
    • 高い本ですがわかりやすいです。
    • ただ、agda-stdlibでなくioa libraryで記述されているのがネックです。
• Haskell
  • Dependent Type in Haskell
    • 依存型の書き方の本。途中まで読みやすいですが、後半はわかりにくいです。

各言語の状況

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