Basics: 関数プログラミングとプログラムの証明
再掲：
############################################################
### 誰もが見えるところに課題の解答を置かないでください！ ###
############################################################
（理由については Preface を参照)
関数型プログラミングスタイルは単純な数学的直観を基礎としています。
手続きやメソッドが副作用を持たなければ、（効率を無視すれば）理解に必要なのは入力をどの出力に割り当てるかだけです。
つまり、手続きやメソッドを、数学的な関数を計算する具体的な手法として理解することとも考えられます。
これが「関数型プログラミング(functional programming)」における「関数型(functional)」という語の意図の一つです。
プログラムと数学的な対象を直接関係づけることは、正当性の形式的証明やプログラムの挙動の健全な非形式的解釈という両面で役に立ちます。
もう一つの関数型プログラミングが「関数型」であるという意図は、関数（やメソッド）を「一級(first class)」値として扱うことから来ます。
ここで、一級値であるとは、関数の引数にしたり、関数の結果として返したり、データ構造に含めたり、といったことができることを意味します。
関数をデータとして取り扱えることで、有用かつ強力な表現が可能になります。
このほかの関数型言語に存在する機能としては、「代数的データ型(algebraic data type)」や「パターンマッチ(pattern matching)」があります。
これらは、データ構造の構成と操作を容易にしてくれます。
また、「多相型システム(polymorphic type system)」という、抽象化やコードの再利用に有用な機能もあります。
上に挙げた機能は全てCoqに含まれています。
本章の最初半分は Gallina と呼ばれるCoqの関数型プログラミング言語としての基本部分の紹介となります。
後ろ半分は、Coqのプログラムの性質を示すために使う、基本的な「タクティック(tactic)」を説明します。
Coqに組み込まれた機能は、「極限まで」小さいものです。
ブール値や自然数、文字列といった基本データ型を提供する代わりに、Coqには新しい型やそれを処理するための強力な機構が用意されています。
この機構により、よくあるデータ型は全て定義することができます。
当然、配布されているCoqにはブール値や数値、リストやハッシュテーブルといったよく使われるデータ構造を定義した大規模な標準ライブラリが付属しています。
しかし、このライブラリの定義には魔法や基底型のようなものは使われていません。
これを説明するために、この資料では、必要となる定義をライブラリから暗黙的に得るのではなく、明示的に再現します。
機構がどのように動くかを知るために、簡単な例から始めましょう。
次の宣言によって、Coqに新しいデータの集合である「型(type)」を定義します。
Definition next_weekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.
一つ注意しておかなければならないことがあります。
この関数の定義では、引数の型と戻り値の型が明示されていることです。
他の多くの関数型プログラミング言語と同様、Coqはこのように型を明示的に書かずともちゃんと動くようになっています。
つまりCoqは「型推論(type inference)」が可能なのですが、この講義ではプログラムを読みやすいように、常に型を明示することにします。
関数の定義ができたら、いくつかの例を挙げてそれが正しいものであることをチェックしなければなりません。
それを実現するために、Coqには三つの方法が用意されています。
一つ目は Compute コマンドを使って、関数next_weekdayを含んだ式を評価させることです。
（もし今手元にコンピュータがあるなら、CoqのIDEのうち好きなもの（CoqIdeやProofGeneralなど）を選んで起動し、実際に上のコマンドを入力し動かしてみるといいでしょう。
この本に付随するCoqのソースから Basics.v を開き、上のサンプルを探してCoqに読み込ませ、結果を観察してください。）
二番目の方法は、評価の結果として我々が期待しているものをCoqに対してあらかじめ以下のような形で例示しておくというものです。
この宣言は二つのことを行っています。
ひとつは、saturdayの次の次にあたる平日が、tuesdayであるということを確認する必要があるということを示すこと。
もう一つは、後で参照しやすいように、その確認事項にtest_next_weekdayという名前を与えていることです。
この確認事項を記述すれば、次のようなコマンドを流すだけで、Coqによって正しさを検証できます。
Proof. simpl. reflexivity. Qed.
この文について細かいことは今は置いておきますが（じきに戻ってきます）、本質的には以下のような意味になります。
「我々が作成した確認事項は等式の両辺が同じものに簡約されることで証明できます。」
三番目の方法は、Coqで（Definitionを使って）定義したものから、もう少し普通の言語（OCamlやScheme、Haskell）のプログラムを「抽出(extract)」してしまうことです。
この機能はGallinaで記述し、正しいと証明されたアルゴリズムを、効率的な機械語まで持っていくことができるという意味でとても興味深いものです。
（もちろん、OCaml、Haskell、Schemeなどのコンパイラや、抽出機能そのものを信頼すれば、というものではあります。
しかし、現在のソフトウェア開発からは大きな一歩であることには違いありません。）
これはCoqの開発動機の一つです。
この話については後の章で詳しく見ます。
「ソフトウェアの基礎」を講義で使用する場合、おそらく講師が宿題の採点用自動スクリプトを使うでしょう。
このスクリプトが正常に動くように（皆さんの解答が適切に採点されるように）、以下の規則を守ってください。
それぞれの章（例えばBasics.v）には「テストスクリプト」（BasicsTest.v）が付随しています。
これは各章の演習問題の採点を自動で行う物です（訳注：現在の翻訳バージョンにはこのスクリプトは含まれていません）。
このスクリプトは講師が採点を自動化するために使うのが主目的ですが、自分で規則を守っているかを確認するためにも使えます。
ターミナルを開いてmake BasicsTest.voと打つか、次の二つのコマンドを打ってください。
（訳注：ここには特定の課題提出システムの話がありますが、明らかに翻訳不要なので省略します）
- 採点スクリプトは、.vファイルのなかから、マークのついた箇所を抜き出して採点します。 演習問題についている「マーク付け」を変更しないでください。 マークは、演習問題のヘッダ、名前、末尾の「空の角括弧」などです。 これらのマークを編集したりしないでください。
- 演習問題自体を消さないでください。 もし（オプションとなっていたり、解けなかったりして）演習問題を飛ばしたとしても、そのまま.vのなかに残して問題ありません。 ただし、この場合は（Abortなどではなく）Admittedで終わるようにしてください。
- 解答に追加の定義（補助関数、補題、など）を書くのは全く問題ありません。 これらは課題の宣言から証明を書く場所の間に書いてください。
coqc -Q . LF Basics.v
coqc -Q . LF BasicsTest.v
BasicsTest.vを編集する必要はありません（Preface.vも不要です）。
このように我々は独自のbool型を一から作っていますが、もちろんCoqにはbool型が多くの有用な関数、補題と一緒に用意されています。
（もし興味があるなら、CoqライブラリドキュメントのCoq.Init.Datatypesを参照してください。）
ここでは可能な限り標準ライブラリと同じ機能をもつ関数や定理を、同じ名前で定義していくことにしましょう。
bool型を使用する関数は、Day型と同じように定義することができます。
Definition negb (b:bool) : bool :=
match b with
| true => false
| false => true
end.
Definition andb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => b2
| false => false
end.
Definition orb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => true
| false => b2
end.
後ろ二つでは、Coqでの引数を複数持つ関数の定義の仕方を例示しています。
対応する、複数の引数への関数適用は次の単体テスト(unit test)で示しています。
これら単体テストは、関数orbが取り得るすべての引数についての完全な仕様（真理値表）となっています。
Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. simpl. reflexivity. Qed.
これらのブール演算に見慣れた表記法を導入することができます。
Notationコマンドで、定義したものに記号表記を割り当てることができます。
Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).
Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.
記述方法について: .v ファイルのコメントの中に Coqのコード片を含める場合には、角括弧を使用してコメントと区切ります。
この慣習はcoqdocというドキュメント作成ツールでも利用されているのですが、コード片を周囲のコメントから視覚的に分離することができます。
CoqソースのHTML版では、ソースはコメントとは別のフォントで表示されます。
Admittedコマンドにより、定義や証明を不完全な状態でひとまず埋めておくことができます。
これは以降の練習問題で、課題として埋める箇所を示すのに使われます。
つまり、練習問題を解くということはAdmittedと書かれた部分をちゃんとした証明に書き直す作業になります。
練習問題: ★, standard (nandb)
Definition nandb (b1:bool) (b2:bool) : bool
. Admitted.
Example test_nandb1: (nandb true false) = true.
Admitted.
Example test_nandb2: (nandb false false) = true.
Admitted.
Example test_nandb3: (nandb false true) = true.
Admitted.
Example test_nandb4: (nandb true true) = false.
Admitted.
☐
練習問題: ★, standard (andb3)
Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool
. Admitted.
Example test_andb31: (andb3 true true true) = true.
Admitted.
Example test_andb32: (andb3 false true true) = false.
Admitted.
Example test_andb33: (andb3 true false true) = false.
Admitted.
Example test_andb34: (andb3 true true false) = false.
Admitted.
☐
Coqの全ての式は、どのような類のものかを表す型を持っています。
Checkコマンドを使うと、Coqに、指定した式の型を表示させることができます。
negb のような関数は、それ自身が true や false と同じように値であると考えることもできます。
そのようにとらえた場合の値の型を「関数型(function type)」と呼び、以下のように矢印を使った型として表します。
negbの型はbool -> boolと書き、「boolからbool」と読み、「bool型の引数をとってbool型の戻り値を返す関数」と解釈します。
同様に、andbの型はbool -> bool -> boolと書き、「二つのbool型の引数をとってbool型の戻り値を返す関数」と解釈します。
我々がここまでで定義してきた型は「列挙型」でした。
このような型は、有限の要素をすべて列挙することによって定義されます。
もう少し興味深い型定義として、コンストラクタが引数を取る場合を説明します。
Inductive rgb : Type :=
| red
| green
| blue.
Inductive color : Type :=
| black
| white
| primary (p : rgb).
この例を少し細かく見ていきましょう。
それぞれ帰納的に定義された型（day、 bool、 rgb、 color、などなど）はredやprimary、true、false、mondayなどの「コンストラクタ(constructor)」から作られる「コンストラクタ式(constructor expressions)」を含んでいます。
rgbやcolorの定義はそれぞれの型に含まれる式がどのように作られるかを表しています。
Definition monochrome (c : color) : bool :=
match c with
| black => true
| white => true
| primary q => false
end.
構築子の一つであるprimaryは引数を取るので、primaryに関するパターンマッチは変数（上記のqのように -- なお、名前は他の名前と重ならない限り自由につけられます）か、または適切な型の定数を含めなければなりません。
Definition isred (c : color) : bool :=
match c with
| black => false
| white => false
| primary red => true
| primary _ => false
end.
最後のパターンprimary _は「primaryをrgb型のred以外の構築子に適用していた場合」の略記です。
（ワイルドカードパターン _ は monochrome の定義にあるような使わない変数 p を書くことと同じです。）
Tuples
Inductive bit : Type :=
| B0
| B1.
Inductive nybble : Type :=
| bits (b0 b1 b2 b3 : bit).
Check (bits B1 B0 B1 B0).
The bits constructor acts as a wrapper for its contents.
Unwrapping can be done by pattern-matching, as in the all_zero
function which tests a nybble to see if all its bits are O.
Note that we are using underscore (_) as a wildcard pattern to
avoid inventing variable names that will not be used.
Definition all_zero (nb : nybble) : bool :=
match nb with
| (bits B0 B0 B0 B0) => true
| (bits _ _ _ _) => false
end.
Compute (all_zero (bits B1 B0 B1 B0)).
Compute (all_zero (bits B0 B0 B0 B0)).
Coqは大規模な開発を支援するために「モジュールシステム」を提供しています。
このコースではこれらはほとんど必要のないものですが、一つだけ有用な機能があります。
プログラムの中のいくつかの要素をModule XとEnd Xで囲んでおくと、End X以降の部分からは、囲まれた中でfooと定義したものをfooではなくX.fooという形で呼び出すようになります。
という訳で、今回はこの機能を使ってnatという型を内部モジュールに定義します。
そうすることで、標準ライブラリの同じ名前の定義に干渉せずに済みます。
（というのも、標準ライブラリのnatには便利な記法があるので、これを使うためです。）
数値
この定義の各句は、以下のように解釈できます。
同様のルールがdayやbool、colorなどにも当てはまります。
これらの条件によって、帰納的(Inductive)な宣言を厳格に定義しています。
条件から、式 O、式 S O、式 S (S O)、式 S (S (S O))...が全てnatに属する式であることがわかります。
また同時に、trueやandb true false、S (S false)、O (O (O S))がnatに属さないことも明確にされています。
重要な点は、ここでは数の「表現(representation)」、つまり書き下し方を定義したに過ぎないと言うことです。
OやSという名前は特別な意味があるわけではなく、なんでもよいのです。
これらは単に数を書くための異なる二つの記号でしかありません。
（それに付随して、SがOの前に並ぶことで任意のnatが記述されるという規則もありますが。）
望むなら、同じ定義を次のように書いても良いのです。
これらの記号の「解釈(interpretation)」は計算でどのように使用するかによって決まります。
自然数というのは非常に一般的な型なので、Coqは自然数を扱ったり表したりするときに若干特別な扱いをします。
SやOを使った「1進数(unary)」表記の代わりに一般的に使われる10進数表記を使うことができます。
実際、Coqは数値を表示する際、デフォルトでは10進数表記を用います。 訳注：1進数は記号を並べた長さで数の大きさを表します。ここではSの数がそれに当たります。
Check (S (S (S (S O)))).
Definition minustwo (n : nat) : nat :=
match n with
| O => O
| S O => O
| S (S n') => n'
end.
Compute (minustwo 4).
これらが表しているのは、いずれの関数も数を引数にとって数を生成できる、ということです。
しかしながら最初の一つと残り二つには根本的な違いがあります。
predやminustwoといった関数には「計算ルール(computation rule)」というものが定義されています。
例えば、predの定義は、pred 2が1に簡約されることを記述したものですが、一方Sにはそのような定義がありません。
コンストラクタは引数に適用するという面では関数と同様ではありますが、コンストラクタは「何も」しないのです！
コンストラクタは単に数を書くための手段でしかありません。
（10進数表記を思い浮かべてください。
1という数字は計算方法などを表すのではなく、ただのデータ片にすぎません。
111を百十一の意味で書いているとき、百十一の具体的な表現として1という数字を三回使っているだけなのです。）
（訳注：ここでは「数」と「数字」を明確に使い分けています。数字はただの文字であり値ではありません。）
数値を扱う多くの関数は、単なるパターンマッチだけでは記述できず、再帰が必要になってきます。
例えば、nが偶数かどうかを調べて返す関数evenbは、n-2が偶数であるかどうかを調べる、という再帰的な定義を必要とします。
そういう関数を定義する場合、Fixpointというキーワードを使用します。
Fixpoint evenb (n:nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.
同じようにFixpointを使って関数oddbを定義することもできますが、ここでは次のようにもっとシンプルな方法で作ります。
Definition oddb (n:nat) : bool := negb (evenb n).
Example test_oddb1: oddb 1 = true.
Proof. simpl. reflexivity. Qed.
Example test_oddb2: oddb 4 = false.
Proof. simpl. reflexivity. Qed.
（1ステップずつ実行していくと、ここではsimplがゴールに何も起こしていないことに気づくかもしれません。
実際のところ、この証明はreflexivityが全てを担っています。
なぜこうなるのかすぐ後で述べます。）
当然ながら、引数を複数持つ関数も再帰的に定義することができます。
Module NatPlayground2.
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
3に2を加えた結果は、5になるべきですね。
Coqがこの計算をどう進めて（簡約して）結論を導くかは以下のように表現できます。
plus (S (S (S O))) (S (S O))
==> S (plus (S (S O)) (S (S O)))
match の二つ目の節での置き換え
==> S (S (plus (S O) (S (S O))))
match の二つ目の節での置き換え
==> S (S (S (plus O (S (S O)))))
match の二つ目の節での置き換え
==> S (S (S (S (S O))))
match の一つ目の節での置き換え
Fixpoint mult (n m : nat) : nat :=
match n with
| O => O
| S n' => plus m (mult n' m)
end.
Example test_mult1: (mult 3 3) = 9.
Proof. simpl. reflexivity. Qed.
matchに引数を与える際、複数の引数を次のようにカンマで区切って一度に渡すことができます。
Fixpoint minus (n m:nat) : nat :=
match n, m with
| O , _ => O
| S _ , O => n
| S n', S m' => minus n' m'
end.
End NatPlayground2.
Fixpoint exp (base power : nat) : nat :=
match power with
| O => S O
| S p => mult base (exp base p)
end.
演習問題: ★, standard (factorial)
factorial(0) = 1
factorial(n) = n * factorial(n-1) (if n>0)
これをCoqでの定義に書き直しなさい。
Fixpoint factorial (n:nat) : nat
. Admitted.
Example test_factorial1: (factorial 3) = 6.
Admitted.
Example test_factorial2: (factorial 5) = (mult 10 12).
Admitted.
☐
表記法を利用して、加算、減算、乗算のような数値を扱う式をずっと読みやすく、書きやすくしておきます。
Notation "x + y" := (plus x y)
(at level 50, left associativity)
: nat_scope.
Notation "x - y" := (minus x y)
(at level 50, left associativity)
: nat_scope.
Notation "x * y" := (mult x y)
(at level 40, left associativity)
: nat_scope.
Check ((0 + 1) + 1).
（level、associativity、nat_scopeという記述は、Coqのパーザーにこれらの表記法をどう扱うかを指示するものです。
詳細は重要ではないのですが、もし興味があれば本章の末尾にある「表記法をより詳しく」の項を読んでください。）
これらは、これまで我々が定義してきたものを何ら変えるわけではありません。
NotationはCoqのパーサに対してx + yをplus x yと解釈させたり、逆にplus x yをx + yと表記させたりするためのものです。
最初の方で、Coqにはほとんど何も用意されていない、という話をしましたが、実際に、数値を比較する関数すら自分で作れる演算なのです！
では自然数を比較して等しい(equality)かをbool値で返すeqb関数を定義します。
入れ子になったmatchに気をつけて、以下のソースを読んでください。
（minus同様に、二つの変数を一度にmatchさせる方法でも書けます。）
Fixpoint eqb (n m : nat) : bool :=
match n with
| O => match m with
| O => true
| S m' => false
end
| S n' => match m with
| O => false
| S m' => eqb n' m'
end
end.
似たようにして、leb関数は一つ目の自然数が二つ目の自然数より小さい(less than)か等しい(equal)か、ということをbool値で返します。
Fixpoint leb (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => leb n' m'
end
end.
Example test_leb1: (leb 2 2) = true.
Proof. simpl. reflexivity. Qed.
Example test_leb2: (leb 2 4) = true.
Proof. simpl. reflexivity. Qed.
Example test_leb3: (leb 4 2) = false.
Proof. simpl. reflexivity. Qed.
Since we'll be using these (especially eqb) a lot, let's give
them infix notations.
Notation "x =? y" := (eqb x y) (at level 70) : nat_scope.
Notation "x <=? y" := (leb x y) (at level 70) : nat_scope.
Example test_leb3': (4 <=? 2) = false.
Proof. simpl. reflexivity. Qed.
練習問題: ★, standard (ltb)
Definition ltb (n m : nat) : bool
. Admitted.
Notation "x <? y" := (ltb x y) (at level 70) : nat_scope.
Example test_ltb1: (ltb 2 2) = false.
Admitted.
Example test_ltb2: (ltb 2 4) = true.
Admitted.
Example test_ltb3: (ltb 4 2) = false.
Admitted.
☐
ここまでに、いくつかの型や関数を定義してきました。
が、ここからは少し目先を変えて、こういった型や関数の特性や振る舞いをどうやって記述、証明していくかを考えてみることにしましょう。
実際には、すでにこれまでやってきたことでも、その一部に触れています。
例えば、これまでのセクションのExampleは、ある関数にある特定の値を入力した時の振る舞いについて、あらかじめ想定していたものと正確に一致していると主張してくれます。
それらの主張が証明しているものは、以下のものと同じです。
「=の両側の式を簡約した結果が一致しているかを調べるために、simplを使って両辺を簡単にして、reflexivityを使いなさい。」
このような「簡約を用いた証明」は、関数のさらに興味深い性質をうまく証明することができます。
例えば、0が自然数の加算における左単位元（左から加えても値が変わらない値）であることの証明は、nが何であっても0 + nを注意深く縮小（簡約）したものがnになることを、+という関数が「最初の引数を引き継いで再帰的に定義されている」ということを考慮した上で示せればいいということです。
（訳注：原文ではここでHTMLと.vファイルの見え方の違いが説明されているのですが、日本語訳ではHTML側での大きな表記の変更を行わないようにしています。
翻訳版の特徴として、HTMLには表示されませんが、.vファイルには、（begin hide/end hideというコメントで挟まれた）英語の原文と訳文が交互に記述されています。
もし訳文を読みづらい、内容が怪しいと感じた場合には、直前にある原文も参照してみてください。）
reflexivityはこれまでの使い方よりももっと強力です。
ここまでの例ではsimplを使っていましたが、実際にはこれは必要ではありません。
reflexivityは両辺が等しいかを確かめる際にある程度自動で簡約します。
simplは単に、証明終了前の簡約後の途中状態をみるために書いています。
以下は証明をより短く書いたものです。
reflexivityはsimplより多くの簡約を行います。
例えば、定義した項を定義の右辺に置き換える「展開(unfolding)」を行います。
こう言った差が発生する理由は、reflexivityが成功するなら、簡約結果がどうなっているかを出す必要がないからです。
simplの場合はこうは行かず、簡約した結果を画面に出すため、定義をむやみに展開したりしません。
この定理と証明の様式は、以前示した例とほとんど同じですが、いくつか違いがあります。
まず、Exampleの代わりにTheoremキーワードが使用されていることです。
これはほとんど単なるスタイルの違いで、ExampleとTheorem（他にもLemma、Fact、Remarkなど）はCoqから見るとすべてほぼ同じ意味です。
他に、量化子（forall n:nat）が加えられていることが挙げられます。
これにより、定理は「全ての」自然数nについて言及できます。
非形式的には、こういった定理の証明ではまず「ある数nが存在して...」と始めます。
形式的には、この動きはintros nによって実現できます。
実際には、これは量化子をゴールから仮定の「文脈(context)」に移動しています。
introsやsimpl、reflexivityは「タクティック(tactic)」の例です。
タクティックは、ProofとQedの間に記述され、示そうとしている言明を確かめる方法を表します。
本章の残りでは、まだ出てきていないタクティックのうちのいくつかを紹介していきましょう。
さらにその後の講義ではもっと色々出てきます。
似た定理も、同じパターンで証明できます。
Theorem plus_1_l : forall n:nat, 1 + n = S n.
Proof.
intros n. reflexivity. Qed.
Theorem mult_0_l : forall n:nat, 0 * n = 0.
Proof.
intros n. reflexivity. Qed.
定理の名前についている_lという接尾辞は、「左の」と読みます。
文脈やゴールがどのように変化していくかを見ていきましょう。
simplをreflexivityの前に呼ぶことで、等価かを判定する前に簡約できます。
ここまでの定理より、もう少し面白い定理を見てみましょう。
この定理は、あらゆるnやmについて成り立つと言っているわけではなく、n = mが成り立つときに限って成立する、というものです。
この矢印は"ならば"と読みます。
前と同じように、nとmをある数として仮定する必要があります。
また、n = mという仮定を置く必要もあります。
introsタクティックはこれら三つを全てゴールから仮定の文脈に移動します。
nとmが両方とも任意の数なのですから、これまでの証明でやってきたように簡約することはできません。
その代わりに、n = mならば、イコールの両側のnをmに書き換えても等しさは変わらない、というところに注目します。
このような書き換えをしてくれるのがrewriteタクティックです。
Proof.
intros n m.
intros H.
rewrite -> H.
reflexivity. Qed.
証明の1行目は、全称量化子（forall）がついた、つまり「あらゆるn,mについて」の部分をコンテキストに移しています。
2行目は、n = mならば、という仮定をコンテキストに移し、Hという名前をこれに与えています。
3行目は、ゴールになっている式(n + n = m + m)に仮定Hの左側を右側にするような書き換えを施しています。
（rewriteの矢印は含意とは関係ありません。
左側を右側に置き換えよ、という指示を出しているだけです。
逆に右側を左側に置き換えたい場合は、rewrite <-と書きます。
この逆の置き換えも上の証明で試して、どのように変わるかを観察してください。）
☐
Admittedコマンドは、Coqに対して「この証明はあきらめたので、この定理はこれでいいことにしてください」と指示するものです。
この機能は、より長い証明をする際に便利です。
何か大きな論証を構築しているときには、今のところ信用している補足的な命題を示したいことがあります。
そんな時、Admittedを使用すると、その命題を一時的に信用できることにして、主としている論証がうまくいくまで続けられます。
そしてそれが完成したのち、あらためて保留していた命題の証明を埋めればいいのです。
ただし注意して下さい。
Admittedを使用することは、一時的にドアを開けて、「全て形式的なチェックを受け証明済みの、信用するに足るCoqの世界」から、信用に値しない下界へ足を踏み出していることに他なりません。
rewriteタクティックを使うときには、仮定の代わりに、前もって証明された定理も利用できます。
以下のように、利用する定理の言明が量化子付きの場合、Coqがゴールに合う形に具体化しようとします。
Theorem mult_0_plus : forall n m : nat,
(0 + n) * m = n * m.
Proof.
intros n m.
rewrite -> plus_O_n.
reflexivity. Qed.
（注意：この証明はrewrite以外のタクティックでできますが、ここでは課題のためと思ってrewriteを使ってください。）
☐
もちろん、どんな命題でも簡単な計算や書き換えだけで証明できるという訳ではありません。
一般に、未知だったり仮定の値（任意の自然数、bool値、リストなど）は、簡単化を止めてしまいます。
例えば、下の命題をsimplタクティックだけで証明しようとすると、すぐに行き詰まってしまいます。
（そういう場合は諦めたことを表すためにAbortコマンドを使います。）
Theorem plus_1_neq_0_firsttry : forall n : nat,
(n + 1) =? 0 = false.
Proof.
intros n.
simpl. Abort.
その原因は、eqbと+の定義で、共に最初の引数がmatchに渡されていることです。
つまり、+に渡す最初の引数はnという未知数な上に、eqbの引数はn + 1という複合式になっているため、そのまま簡約できないのです。
証明を進めるには、nを何らかの条件に分割できないかの検討が必要です。
もしnがOなら、(n + 1) =? 0の結果を得ることはできます。
もちろん結果はfalseです。
もしnが何かのn'を使ってn = S n'と表せる場合、我々はn + 1の値を得ることはできません。
ただ、少なくともその式が一つのSで始まることはわかります。
これが分かれば、(n + 1) =? 0の結果がfalseになることまでは計算できます。
このことから、求められるタクティックはCoqにn = Oの場合とn = S n'の場合に分けて考えるように求めるもので、これを実現するのがdestructタクティックです。
Theorem plus_1_neq_0 : forall n : nat,
(n + 1) =? 0 = false.
Proof.
intros n. destruct n as [| n'] eqn:E.
- reflexivity.
- reflexivity. Qed.
この証明では、destructタクティックは二つのサブゴールを作っています。
その両方を別々に証明することで、全体が定理として認められます。
destructについている注釈"as [| n']"は、「イントロパターン(intro pattern)」と呼ばれるものです。
これはCoqに対して、サブゴール毎に出てくる変数をどんな変数名で扱うかを指示するものです。
一般的に[]の間にあるものは | によって区切った「名前のリスト」のリストです。
今回のリストの最初の要素は空ですが、これはnatの最初のコンストラクタであるOが引数をとらないからです。
二つ目のコンストラクタSは引数を一つ取りますので、二つ目の要素では変数名を一つ、n'を指定しています。
それぞれのサブゴールで、Coqはnがn = 0だったか、それともあるn'に対してn = S n'と表されるのだったかを覚えています。
eqn:Eという注釈はこの等式をEという名前で覚えておくようにdestructに要求します。
（eqn:Eを書かない場合、Coqはこれらの等式を覚えておきません。
もしこの等式を使わないのであれば覚えないのは合理的なのですが、実際にはサブゴールで何を示そうとしているのかを明記するために覚えさせた方がよいでしょう。）
二行目と三行目にある-という記号は「バレット(bullet)」と呼ばれるもので、ある時点で存在したサブゴールそれぞれの証明の開始を表しています。
バレットの後ろに続く証明スクリプトは、あるサブゴールの一連の証明になります。
この例では、どちらのサブゴールも単にreflexivityによる簡単化と比較で証明できています。
例えば、二つ目は (S n' + 1) を S (n' + 1) に書き換え、 eqb の定義を展開し、最後に match を簡単化することで、 (S n' + 1) ?= 0 全体を false に簡単化します。
バレットを付けるのは必須ではありません。
もしバレットがないと、Coqは単に、順に次々とサブゴールの証明を求めます。
しかし、バレットを使っておくと、証明の構成がはっきり見え、読みやすくなります。
また、バレットによって、次のサブゴールに行く前に、一つ前のサブゴールが証明完了していることを確かめることができ、証明が混ざったりすることを防げます。
大規模になると、証明が壊れたときのデバッグが非常に難しくなるため、こういった要素が重要になります。
Coqでの証明の書き方の、厳格なルールというものはありません。
特に、どこで行を折り返すか、証明のネストを表すための字下げをどの単位で行うか、などは全く決まっていません。
しかし、複数のゴールができたときにバレットを明示すれば、他の部分をどうしても大体読みやすくなるでしょう。
一行の長さについて少し語っておきます。
Coq初心者の中には極端な人がいて、一行に一つのタクティックしか書かない人や、一行に全ての証明を詰め込む人がいます。
好い加減というのは、大体その間にあります。
一行を80文字に押さえるというのは扱いやすい慣習の一つです。
destructタクティックは帰納的に定義された型に対して使用できます。
例として、bool値の否定が対合(involutive)であること、つまり否定の否定が元と同じになることを証明してみましょう。
Theorem negb_involutive : forall b : bool,
negb (negb b) = b.
Proof.
intros b. destruct b eqn:E.
- reflexivity.
- reflexivity. Qed.
ここで使われているdestructにはas句がありませんが、ここで展開しているbの型boolの二つのコンストラクタが両方とも引数をとらないため、名前を指定する必要がないのです。
このような場合、"as [|]"や"as []"のように書くこともできます。
実は、destructのas句はどんなときでも省略可能です。
その際はCoqの側で自動的に変数名をつけてくれます。
しかし、これはあまりよくない書き方でもあります。
Coqに任せておくと、しばしば混乱しやすい名前を付けるからです。
destructを、まだ他のサブゴールが残っている状態で使うこともあります。
このとき、バレットを使うときは異なる「レベル」を表すために異なる記号をバレットとして使います。
Theorem andb_commutative : forall b c, andb b c = andb c b.
Proof.
intros b c. destruct b eqn:Eb.
- destruct c eqn:Ec.
+ reflexivity.
+ reflexivity.
- destruct c eqn:Ec.
+ reflexivity.
+ reflexivity.
Qed.
バレットとしては、-や+の他に* （アスタリスク）が使用できます。
また、証明のブロックを波括弧（{}）で囲むこともできます。
これは、3つ以上のレベルでサブゴールが出来てしまった場合に有用です。
Theorem andb_commutative' : forall b c, andb b c = andb c b.
Proof.
intros b c. destruct b eqn:Eb.
{ destruct c eqn:Ec.
{ reflexivity. }
{ reflexivity. } }
{ destruct c eqn:Ec.
{ reflexivity. }
{ reflexivity. } }
Qed.
この例のように、波括弧で証明の始めと終わりを囲むことで、ネストしてレベルを表現することができます。
また、波括弧で囲むことで、既にバレットとして使ってしまった記号を再利用することができます。
Theorem andb3_exchange :
forall b c d, andb (andb b c) d = andb (andb b d) c.
Proof.
intros b c d. destruct b eqn:Eb.
- destruct c eqn:Ec.
{ destruct d eqn:Ed.
- reflexivity.
- reflexivity. }
{ destruct d eqn:Ed.
- reflexivity.
- reflexivity. }
- destruct c eqn:Ec.
{ destruct d eqn:Ed.
- reflexivity.
- reflexivity. }
{ destruct d eqn:Ed.
- reflexivity.
- reflexivity. }
Qed.
この章を締めくくる前に、便利な記法を一つ挙げておきます。
既に気づいたかもしれませんが、変数の場合分けは、以下のように変数の導入直後に行われることが多々あります。
intros x y. destruct y as [|y] eqn:E.
この書き方があまりに多いので、Coqではこの簡略版として、導入する変数を、名前の代わりにイントロパターンによって導入することができます。
例えば上で証明した plus_1_neq_0 にその略記法を使うと以下のようになります。
（ただし欠点もあります。
この略記法では、これまで eqn:E を使って覚えていた等式が残らなくなってしまいます。）
intros x y. destruct y as [|y] eqn:E.
Theorem plus_1_neq_0' : forall n : nat,
(n + 1) =? 0 = false.
Proof.
intros [|n].
- reflexivity.
- reflexivity. Qed.
もし全ての場合で名前を付ける必要がないのなら、[]と書くことができます。
Theorem andb_commutative'' :
forall b c, andb b c = andb c b.
Proof.
intros [] [].
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.
☐
☐
（「オプション」と付けた節は、他の章で同じく「オプション」と付いている節以外には必須ではありません。
初めて読むときは、今後のために軽く目を通すくらいにしておくと良いでしょう。）
中置記法の加算と乗算の記法の定義を再掲します。
Notation "x + y" := (plus x y)
(at level 50, left associativity)
: nat_scope.
Notation "x * y" := (mult x y)
(at level 40, left associativity)
: nat_scope.
Coqで表記法を定義する際、「優先度(precedence level)」と「結合性(associativity)」を定義できます。
優先度に n を割り当てる際にはat level nのように書きます。
優先度は、Coqが複雑な式を解釈するのに使います。
結合性は同じ表記法が複数回現れたときの解釈を定めるために付けます。
例えば、この章では+と*を定義しましたので、1+2*3*4を(1+((2*3)*4))の略記版として利用できます。
Coqでは優先度として0から100のレベルを、また結合性として「左結合(left)」「右結合(right)」または「結合性なし(no)」を指定できます。
これ以降、例えばListsの章などで、これらの宣言が多数使われます。
Coqでの表記法は、それぞれが「表記スコープ(notation scope)」と関連します。
今どの表記スコープで書かれているかは、Coqが自動で判定しようとします。
例えばS(O*O)と書いていればnat_scopeだと判定し、デカルト積（タプル）型（後の章で出ます）であるbool*boolという記述からはtype_scopeと判定します。
判定を誤ることもあるので、パーセント記号を使って、(x*y)%natのように明示しないといけないこともあります。
また、Coqが特定の表記スコープでの表記法であることを明示するために%natという記法を使うこともあります。
表記スコープは3,4,5などの数の表記法にも使われます。
例えば0%natと書くと本章で使っている自然数（nat）のOを意味しますが、0%Zと書くと標準ライブラリで提供されている整数（Z）のゼロを意味します。
プロ向け情報：Coqの表記法の記法はそれほど強力ではありません。
過剰な期待はやめましょう。
加算の定義をそのまま持ってきました。
上の定義をCoqが検査すると、plus'が「第一引数が減少している（"decreasing on 1st argument"）」というメッセージを出します。
これは引数nに関する「構造的再帰(structural recursion)」を行っていることを意味します。
つまり、再帰呼び出しの際には、必ずnが厳密に小さくなっているということです。
これにより、どんな引数でもplus'の呼び出しが必ずいつか終了することを保証できます。
CoqはFixpointでの定義で、ある特定の引数が「減少している」ことを求めます。
この要求はCoqの設計の基礎部分から来ています。
この要求により、Coqで定義できる関数が、どんな入力に対しても終了することを保証できます。
しかし、Coqの「減少性解析」はそれほど洗練されていないため、場合によっては関数を不自然な形で書かなければならないこともあります。
練習問題: ★★, standard, optional (decreasing)
発展課題
Theorem identity_fn_applied_twice :
forall (f : bool -> bool),
(forall (x : bool), f x = x) ->
forall (b : bool), f (f b) = b.
Proof.
Admitted.
☐
Exercise: ★, standard (negation_fn_applied_twice)
From Coq Require Export String.
Definition manual_grade_for_negation_fn_applied_twice : option (nat*string) := None.
☐
練習問題: ★★★, standard, optional (andb_eq_orb)
☐
練習問題: ★★★, standard (binary)
10進数 2進数 1進数
0 Z O
1 B Z S O
2 A (B Z) S (S O)
3 B (B Z) S (S (S O))
4 A (A (B Z)) S (S (S (S O)))
5 B (A (B Z)) S (S (S (S (S O))))
6 A (B (B Z)) S (S (S (S (S (S O)))))
7 B (B (B Z)) S (S (S (S (S (S (S O))))))
8 A (A (A (B Z))) S (S (S (S (S (S (S (S O)))))))
一般的な2進数表記とは逆に、この表現では、下位ビットが左に、上位ビットが右に来るようになっています。
この方がCoqでは扱いやすくなります。
(a) 以下の2進数用のインクリメント関数incrと、2進数から1進数へ変換する関数bin_to_natを完成させなさい。
(b) test_bin_incr1やtest_bin_incr2といった名前でincrやbin_to_natに関する5つの単体テストを書きなさい。
（ここまでやってきたとおり、Coqでの「単体テスト」とはExampleで書かれた、reflexivityだけで証明できるものです。）
2進数をインクリメントして1進数に変換したものは、1進数に変換して1加えたものと一致するということに注意してください。
☐