概要

『Software Foundations』（『ソフトウェアの基礎』）という無料のオンライン教科書があります。大学院の学生を想定している4巻構成のテキストで、Coqを使って、プログラムやアルゴリズムの形式的に証明をしながら、ボトムアップでソフトウェアの各種構成部品を作っていくものです。

Coqの勉強資材としてもすぐれているので、Coqの勉強がてら Vol1.の練習問題を一通り終わらせたので、アウトプットをします。具体的には、Vol1. における発展的な課題のうち、興味深いものを紹介するとともに、考え方の概略を記載します。

参考リンク:

SoftwareFoundations 公式

#01. 1進数と2進数

出典 Basic.v:

「O は nat型で、 nat に後者関数記号 S をくっつけてできたものも nat型」というように型natを構成できます。ペアノ公理における構成法であり、数の1進数表現とみなせます。

一方「Zは bin型で、bin型に A もしくは B をくっつけてできたものもbin型」という形で構成する型binは、自然数の2進数表現とみなせます。なぜなら「構成子Aでつくる」＝「元の数を２倍する」、「構成子Bでつくる」＝「元の数を2倍して1を足す」というように意味付けをすると、例えば
A (B (B Z) は 0b110 という自然数に対応しますし、任意の自然数はこのような意味付けの下で表現できるからです。

上記を考慮すると、bin->nat な関数 bin_to_nat やその逆である nat_to_bin という関数を再帰的に実装できます。そして「任意の nat型の値を nat_to_bin で bin にして、その結果を bin_to_nat で nat型に戻してあげると元に戻る」ことも、形式的に証明できます。

一方、その逆は成り立ちません。Z, A Z, A (A Z), ...は、bin_to_nat の実装ではすべて 0 に評価されるからです。別の言い方をすると、bin_to_nat は単射ではありません。そこでこれらを正規化する normalize: bin->bin をFixpointとして実装してあげると、「任意の bin型の値を bin_to_nat で nat にして、その結果を nat_to_bin で bin型に戻してあげると、元の値をnormalizeした値に戻る」を形式的に証明できます。

#02. 書き換えの妥当性(map/rev)

出典: Poly.v

多相型であるリスト型は「nilはリスト型である。リスト型に cons で要素をつないだものもリスト型である」というように Inductive で定義できます。

リストが定義できれば、それに対する map や fold を Fixpointとして実装できます。また、よく知られているように、map をそのように実装するのではなく fold を使って実装することができることも知られています。このようにして作られた fold_map と、冒頭の map の同一性を外延公理の下で（任意の入力で同じ出力がでるなら二つの関数は同じとみなす）証明できます。

同様にリストを反転させる Fixpoint であるrevも直観的に実装できますが末尾再帰ではありません。そこで末尾再帰版のtr_revという実装も考え、外延公理の下でrevとtr_revの同値性を証明できます。

#03. 排中律の扱い方

出典: Logic.v

Coqは直観主義的/構成主義的な道具立てなので、常に「Pまたは~P」が成り立つわけではありません（特定の述語に関しては成り立つような場合もあり、その時は決定可能といい、リフレクションという便利な道具立てが使えます）。

一方、通常の数学・論理学は古典論理的に展開されるので、Coq上で数学等を行うときには、追加の道具立てが必要になります。具体的には「直観主義論理に、排中律を公理として付け加えると古典論理と同じ証明能力になる」としられているので、排中律に相当する論理式を証明済みと仮定すれば、Coq上で古典論理的な議論ができます。Axiomという構文でclassicという排中律に相当する論理式を加えたものが Classical ライブラリです。

「Coq+classic」という選択をしたわけですが、他の選択肢もあります。二重否定除去, や含意の書き換えやパースの法則といった論理式を代わりに公理に仕立て上げても同じです。つまり、直観主義論理の導出関係において、排中律と二重否定除去等の論理式は同値です。これらを証明することができます。

参考: Qiita: 直観主義論理五つの定理の同値性

#04. 述語・関係の扱い

出典: IndProp.v, Rel.v

偶数性などの述語は様々な方法で定義できます「∃y(y+y=x) を内包とする集合」「0は偶数、偶数に2を足したものは偶数」「0と2は偶数、偶数に2を足したものは偶数」「奇数の前者」などなど。

特に、Inductive で定義されたプロパティ(≒パラメータ化された命題)の方法は便利に使われます（人間はそのような傾向性を持ちますし、そのように構成されれば曖昧さを排除できます）。特に「induction: 証拠に基づく帰納/induction on evidence」や、証拠の由来を探る「inversion」という道具立ては構成的な観点では強力な道具となり、例えば、induction を使うことで「Inductiveに構成されたプロパティ even に対し、even n -> exists m, n = m + m を証明できます。

述語を上述のようにアリティ1のパラメータ化された命題とみなすと、述語と関係の違いはアリティの違いに過ぎないため、Coq上では述語と関係に違いはありません（関係を扱うために特別な道具立てを必要としません）。関係で重要な「反射性・対称性・反対称性・推移性・閉包」といった各種概念はCoq上でプロパティに付随する仕様として記述できます。例えば帰納的に定義したプロパティ <= に対して反射性と推移性を証明できます。

#05. 状態マシン不要の正規表現マッチャ

出典: IndProp.v

文字列型stringをlist asciiとしましょう(asciiは標準ライブラリに同梱されておりBoolの8つ組で定義されています)。文字列型と正規表現を入力としたときにマッチ可否を返す Fixpoint regex_match を実装できます。以下その概略です。

正規表現型reg_exp: Inductiveに正規表現型を構成します。（何にもマッチさせないことを意図した）EmptySetと（空文字列にマッチさせることを意図した）EmptyStr および（1文字にマッチさせることを意図した）Char: ascii->regexp は正規表現です。正規表現に、（正規表現の結合を意図した）App や (正規表現の|を意図した) Union をしたもの、(正規表現の*を意図した) Star したものも正規表現で、そしてそれで全てです。例えば正規表現 abc* は上記の描像では App (Char a) (App (Char b) (Star (Char c))) が対応します(注: この例における a などは正確には ascii_of_nat 97などと書くべきです)。

プロパティexp_match: 上記のように正規表現型を定義すれば、「文字列sと正規表現reはマッチ関係にある」というようなパラメータ化された命題＝プロパティも、帰納的に直観的に実装可能です。よくつかうので s =~ re というNotationも導入します。これにより、正規表現とマッチ関係に関する様々な定理が証明できるようになります。特に、ポンプの補題と呼ばれる有名な定理を形式化・証明できます。

二つのFixpoint: 上記結果は有用ですが、プロパティに関する定理であり当初の目的と一致しません。つまり、プロパティexp_match: string -> reg_exp -> Propと（目的である）Fixpoint regex_match: string-> reg_exp ->boolが違うのです。これをリフレクションでつなぐことを考えます。それを掛け渡しするためのFixpointであるmatch_eps: reg_exp -> bool と derive: ascii -> reg_exp -> reg_exp を導入します。前者であるところのmatch_epsは与えられた正規表現が空文字列にマッチするかのテスト関数です。「・・・は空文字列にマッチする」は決定可能な述語なので（これは証明できます）、リフレクションの道具立てが使えるというわけです。後者であるところの derive は文字列と正規表現が与えられたときにそのderivation(日本語訳を知らない)である正規表現を返す関数です。この二つのFixpointを使うと、目的のFixpointは簡単に実装でき、それが正しいことを証明できます。

Fixpoint regex_match (s:string) (re:reg_exp): bool :=
  match s with
  | [] => match_eps re
  | hd :: tl => regex_match tl (derive hd re)
  end.

#06. リスト版鳩ノ巣原理

出典: IndProp.v

「4羽の鳩を3つの箱に詰めると、複数匹の鳩が詰まった箱がある」やそれに類似する論法を鳩ノ巣原理といいます。鳩ノ巣原理は集合論にルーツをもつ言明ですがCoqで証明できます。

形式化しましょう。二つのリスト l1, l2 を用意します。l1 を鳩の集合に対応させ l2 は巣の集合に対応させます。すると鳩ノ巣原理は以下の言明として表現してよいでしょう:

Theorem pigeonhole_principle: forall (X:Type) (l1  l2:list X),
   excluded_middle ->
   (forall x, In x l1 -> In x l2) ->
   length l2 < length l1 ->
   repeats l1.

ここで、excluded_middleは排中律です。なくても証明ができるそうですが私には無理でした。Inはリストにその要素が入っているかを表すプロパティです。lengthはリストの長さを表すfixpointで、repeatsは要素に重複があることを表すプロパティです。

#07. 含意は全称量化で表現できる

出典: ProofObjects.v

初めてみたときはびっくりしましたが、含意 -> は量化子 forall で書ける、つまり、Coqにおいて P->Q は forall (_:P), Qの糖衣構文として理解されるということです。

具体例を考えるとわかりやすいです。even n -> even (n+2)は ∀(E : even n), even (n+2) つまり「even n の任意の証拠Eが与えられたときには　even (n+2)の証拠がある」と書き換えできるのはカリーハワード対応から納得いきますが、その記述にはEという識別子は不要なのでアンダースコアーでプレースホルダにできて ∀(_ : even n), even (n+2)と書けます。

#08. 形式証明の自動化

出典: Auto.v

形式証明にはある種のテンプレートがあって、上手く使うことが大事です。tautoは論理結合子関連の自動化に, ring は数項関連の自動化に, omega はプレスバーガー算術の自動化に使えます。それ以外にも、Goalに現れない一次変数を推論させる eapply やrewrite の対象を選んでもらう rewrite ... in *というタクティックも有用です。

もう少し細かい粒度では、inversion X;subst;clear X という一連のタクティック（本文ではinvと表記し）や、rewriteすればdiscriminateですぐ証明できるときにつかるようなタクティック(本文ではrwinvと表記)、全称量化されたコンテキストをspecializeさせ、証明を進めるようなタクティック(本文ではfind_eqn)などなどを押さえると証明が非常に短くなります。

#09. プログラミング言語の作り方

出典: Imp.v ImpCEvalFun.v

C言語に代表される手続き型のプログラミング言語を作り、その正しさを証明するにはどうすればいいかを記述します。ただ、Vol1. では基本的な部分のみであり、Vol2.以降で発展的なことをやるようです。

3つの構成部品: 字句解析と構文解析を考えずに、抽象構文木から話を始めましょう。大まかに以下の順序で部品を構成していくと出来上がります。それ以外に最適化の例も実習しました。

Step1: 式の評価器（変数無し）
- 例: (Plus 1 2) を 3に評価する
- 例: (Le 3 5) を true に評価する
Step2: 式の評価器（変数あり＝状態も入力とする評価）
- 例: 状態 {X: 10}と式(Plus X 2)を入力として12と評価する
Step3: コマンド(≒文)の評価器
- 例: 状態 {X: 2}とコマンド(X ::= 10)を入力として状態を {X: 10}に更新する
- 例: 状態 {X: 2, Y: 3}とコマンド X ::= X + 1;; Y ::= X + Y を入力として状態を {X: 3, Y: 6}に更新する

評価器は関数にするかプロパティにするか？: 普通に考えると評価器は関数として、つまり Fixpoint として実装します。一方プロパティとして実装する方法もあり、それぞれ一長一短で、どちらがよいのか、というのは一概に決められないようです（形式証明の観点では後者が本流だと思います）。

Fixpointでの評価器: state -> command -> state
- Computational な定義方法とみなせます。Coqが簡約を自動的にやってくれるので、対話的に証明をするときにはとても便利です。また、Haskell等にエクスポートすることができます。
- ただし実装不可の場合があります。関数として実装するということは、全域性や、再帰における引数の減少性（Coqの整合性のためにシステムに組み込まれています）が要求され、評価の値が未確定な項が存在するような場合（乱数など）など懸念が多くあります。対処法もあるにはあるのですが（主にImpCEvalFun.v）、複雑になりがちです。
プロパティでの評価器: state -> command -> state -> Prop
- 関係としての定義方法とみなせます。（上述の関数との対比という文脈ではグラフとしての定義方法といったほうがわかりやすいかもしれません。）
- 操作論的意味論という考え方と親和性が高いです。見た目を論理学の推論規則に対応させた図式で記述できたり（カリーハワード対応）、state0 =[cmd]=> state1 のように、状態の変換を行うものとしてプログラムを捉えることが可能になります。部分関数も表現できるので、こちらの評価器の方が表現力は高いです。
- ただし、Fixpointでの実装では、各種の形式証明は煩雑になりがちです。

プログラミング言語についての証明: Coq上でプログラミング言語を実装する時にうれしいのはどのようなことでしょうか？以下に実例を記述します:

評価における決定性の証明: 入力となる状態とコマンドが一致していれば、評価された値が一意に決まることを形式的に証明できます
最適化導入の正しさを証明できる: AST をいじくり回して（効率の良い）評価器を作った時に、本当にその最適化が正しいのかを形式的に証明できます

最後に

Vol1. における練習問題のうち、一つだけどうしても解けない問題がありました。ネットで調べてもやはり難しいという評判でした。答えを知っている人は教えてくれるとうれしいです。問題は rev_palつまり、「リストが自身の逆順と等しい時そのリストは回文である」の証明です。一つ前でなく二つ前の仮定を利用する帰納法です。

というか、Coqの帰納法において k<=n（自然数の場合）の証拠を使う方法全般がわからない・・・fixを使うらしいですが・・・