列挙型

プログラミング言語Coqには、ほとんど何も（ブール型や数値型すら）ビルトインされていません。その代わりCoqには、新しい型やそれを処理するための強力なツールが用意されています。

曜日の表し方

まず最初はとても簡単なサンプルから始めましょう。次の定義は、Coqに対して、新しいデータ型のセット（集合）である'型'を定義しています。その型はdayで、要素はmonday、tuesday...などです。その定義の1行は以下のようにも読めます。"mondayはday。tuesdayはday"といった具合です。

"day"が何かを定義できれば、それを利用して関数を書くこともできるでしょう。

一つ注意しておかなければならないことがあります。この関数の定義では、引数の型と戻り値の型が明示されていることです。他の多くの関数型プログラミング言語と同様、Coqはこのように型を明示的に書かずともちゃんと動くようになっています。それはいわゆる「型推論」という機構によって実現されていますが、型を明示した方がプログラムを読みやすくできると判断するなら、いつでもそうしてかまいません。

関数の定義ができたら、いくつかの例を挙げてそれが正しいものであることをチェックしなければなりません。それを実現するために、Coqには三つの方法が用意されています。一つ目は「Eval Simpl」コマンドを使って、関数next_weekdayを含んだ式を評価させることです。次のコマンドをよく見て、何をしているかを考えてみてください。

もし今手元にコンピュータがあるなら、CoqのIDEのうち好きなもの（CoqIDEやProofGeneralなどから）を選んで起動し、実際に上のコマンドを入力し動かしてみるといいでしょう。付録の「Basic.v」ファイルから上のサンプルを探してCoqに読み込ませ、結果を観察してください。

「simpl（simplify）」というキーワードは、Coqに対して「我々が与えた式を正確に評価せよ」という命令です。しばらくの間、「simpl」コマンドは我々にとって必要な唯一のコマンドになるでしょう。この後でもう少し使い出のある別のコマンドを覚えるまでの間ですが。

二番目の方法は、評価の結果として我々が期待しているものをCoqに対してあらかじめ以下のような形で例示しておくというものです。

この宣言は二つのことを行っています。ひとつは、saturdayの次の次にあたる平日が、tuesdayであるということを確認する必要があるということを示すこと。もう一つは、後で参照しやすいように、その確認事項にtest_next_weekdayという名前を与えていることです。 この確認事項を定義すれば、次のようなコマンドを流すだけで、Coqによって正しさを検証できます。

この文について細かいことは今は置いておきますが（じきに戻ってきます）、本質的には以下のような意味になります「我々が作成した確認事項は簡約後の同値チェックによって証明されました。」

三番目の方法は、Coqで定義したものから、他のより一般的な言語（OcamlやScheme、Haskellといった）のプログラムを抽出してしまうことです。この機能は今主流の言語で完全に確認されたプログラムを実現できる道を開いたという意味でとても興味深いものです。ここではこの件について深入りすることはしませんが、もしより深く知りたいという場合はCoq'Art book（Bertot and Casteran著）か、Coqリファレンスマニュアルを参照してください。

ブール型

同様にして、trueとfalseを値としてとる「bool型」を定義することができます。

このようにして、我々は独自のbool型を一から作りあげることもできるのですが、もちろんCoqには標準ライブラリとしてbool型が多くの有用な関数、補助定理と一緒に用意されています。（もし興味があるなら、CoqライブラリドキュメントのCoq.Init.Datatypesを参照してください。）ここでは可能な限り標準ライブラリと正確に同じ機能を、我々独自の名前で定義していくことにしましょう。

後半の二つは、引数を複数持つ関数を定義する方法を示しています。

次の四つの単体テストは、関数orbが取り得るすべての引数についての完全な仕様（真理値表）となっています。

記述方法について: Coqのコード中にコメントを含める場合には、大括弧を使用してコードと区切ります。この慣習はcoqdocというドキュメント作成ツールでも利用されているのですが、ソース中のコメントをコードから視覚的に分離することができます。CoqソースのHTML版では、コメントはソースとは別のフォントで表示されます。

次にCoqでのちょっとトリッキーな定義（admit）を紹介しましょう。このadmitは、定義や証明にある不完全な部分を「とりあえず今は無いこと」にしてくれるものです。これを次のnandbでの練習問題に使ってみることにしましょう。ここからしばらく、練習問題を解くということはadmitやAdmittedと書かれた部分をちゃんとした定義や証明に書き直す作業になります。

練習問題: ★ (nandb)

次の定義を完成させ、Exampleで記述された確認内容がCoqのチェックをすべて通過することを確認しなさい。

この関数はどちらか、もしくは両方がfalseになったときにtrueを返すものである。

下の定義からAdmitted.を取り去り、代わりに"Proof. simpl. reflexivity. Qed."で検証できるようなコードを記述しなさい。

☐

練習問題: ★ (andb3)

☐

関数の型

Checkコマンドを使うと、Coqに、指定した式の型を表示させることができます。例えば、（negb true）という式の全体の型はboolである、という具合です。

negbのような関数は、それ自身がtrueやfalseと同じように値であると考えることもできます。そのようにとらえた場合の値の型を「関数型」と呼び、以下のように矢印を使った型として表します。

negbの型はbool→boolと書き、「boolからbool」と読み、bool型の引数をとってbool型の戻り値を返す関数と理解することができます。同様に、andbの型はbool → bool → boolと書き、「二つのbool型の値を引数としてbool型の値を作成して戻す」と解釈します。

数値

ちょっと技術的な話：Coqは大規模な開発を支援するためにちょっと大げさにも見えるモジュールシステムを提供しています。このコースではこれらはほとんど必要のないものですが、一つだけ有用なものがあります。プログラムの中のいくつかの要素をModule XとEnd Xで囲んでおくと、End X以降の部分から、囲まれた中の定義をX.fooという風に呼び出すことができます。このことは、新しくfooという名前で関数を定義しても問題ないということです。逆に、同じスコープの中では、同じ名前での定義はエラーとなります。という訳で、今回我々はこの機能を使ってnatという型を内部モジュールとして定義します。そうすることで、標準ライブラリの同じ名前の定義を覆い隠してしまわずに済みます。

我々がここまでで定義してきた型は「列挙型」の型定義でした。このような型は、有限の要素をすべて列挙することによって定義されます。型を定義するもう一つの方法は、「帰納的な記述」を並べることで要素を記述する方法です。例えば、自然数は（全て並べるわけにはいきませんが）以下のような方法で定義できます。

この定義の各句は、以下のように解釈できます。

• Oは自然数である（0（ゼロ）ではなく"O"（オー）であることに注意）
• Sは自然数を引数にとり、別の自然数を生成する「コンストラクタ」である。このことは、nが自然数ならS nも自然数であることを示している。

この定義にして、もう少し詳しく見ていきましょう。

これまでに定義してきた帰納的な型（weekday、nat、boolなど）は、実際には式の集合とでも言うべきものです。natの定義は、natの要素となる式がどのように構築されるかを表しています。

• 式O（オー）は、natに属する。
• もしnがnatに属するならば、S nもまたnatに属する。
• これら二つの方法で表された式のみがnatに属するものの全てである。

これら三つの条件によって、natが帰納的(Inductive)な方法で厳格に定義されています。この定義によって、式 O、式 S O、式 S (S O)、式 S (S (S O))...が全てnatに属する式であることが表されています。また同時に、trueやandb true false、S (S false)がnatに属さないことも明確にされています。

こうして定義された自然数natをマターンマッチにかけることで、簡単な関数を書いてみましょう。例えば、一つ前のnatを返す関数は以下のよう書けます。

この２番目の句は「もしnが何らかのn'を用いてS n'と表せるなら、n'を返す」と読めます。

自然数というのは非常に一般的な型なので、Coqは自然数を扱ったり表したりするときに若干特別な扱いをします。SやOを使った式の代わりに一般的に使われるアラビア数字を使うことができます。実際、Coqは数値を表示する際、デフォルトではアラビア数字を用います。

natのコンストラクタSは、nat → nat型の関数でminustwoやpredも同様です。

これらが表しているのは、いずれの関数も数を引数にとって数を生成できる、ということです。しかしながらこれらの関数には根本的な違いがあります。predやminustwoといった関数には「計算ルール」というものが定義されています。predの定義は、pred nがmatch n with | O => O | S m' => m' endのように簡約されることを記述したものですが、一方Sにはそのような定義がありません。しかし両方とも関数には違いなく、引数を元に評価されるということについては同じで、それ以上のものではないのです。

数値を扱う多くの関数は、単なるパターンマッチだけでは記述できず、再帰的な定義が必要になってきます。例えば、nが偶数かどうかを調べて返す関数evenbは、n-2が偶数であるかどうかを調べる、という再帰的な定義を必要とします。そういう関数を定義する場合、Fixpointというキーワードを使用します。

Coqがこの定義をチェックする際、evenbが再帰的に呼ばれるとき、最初の引数が減少しているかに注目します。これは、ここでいう再帰がnについて構造的再帰（もしくは原始的再帰）であること、つまりnについて常により少ない値で再帰呼び出しを行っているか、ということです。これはevenbが最終的に停止するということを意味しています。CoqはFixpointキーワードで定義される関数が常にこの「減少性」を持つことを要求します。

同じようにFixpointを使って関数oddbを定義することもできますが、ここでは次のようにもっとシンプルな用法で簡単に作ってみましょう。

当然ながら、引数を複数持つ関数も再帰的に定義することができます。

ネームスペースを汚さないようにするため、別のモジュールに定義することにしましょう。

3に2を加えた結果は、5になるべきですね。

Coqがこの計算をどう進めて（簡約して）結論を導くかは以下のように表現できます。

plus (S (S (S O))) (S (S O))

==> S (plus (S (S O)) (S (S O))) by the second clause of the match

==> S (S (plus (S O) (S (S O)))) by the second clause of the match

==> S (S (S (plus O (S (S O))))) by the second clause of the match

==> S (S (S (S (S O)))) by the first clause of the match

表記を簡便にするため、複数の引数が同じ型を持つときは、型の記述をまとめることができます。 (n m : nat)は(n : nat) (m : nat)と書いたのとまったく同じ意味になります。

matchに引数を与える際、複数の引数を次のようにカンマで区切って一度に渡すことができます。

minusのmatchの行に現れる( _ )は、ワイルドカードパターンと呼ばれるものです。パターンの中に _ を書くと、それはその部分が何であってもマッチし、その値が使用されないことを意味します。この _ は、このような場合に無意味な名前をつける必要をなくしてくれます。

演習問題: ★ (factorial)

再帰を使用した、一般的なfactorical（階乗）の定義を思い出してください :

    factorial(0)  =  1
    factorial(n)  =  n * factorial(n-1)     (if n>0)

これをCoqでの定義に書き直しなさい。

☐

ここで紹介する"notation"（表記法）という機能を使うことで、加算、減算、乗算のような数値を扱う式をずっと読みやすく、書きやすくすることができます。

これらは、これまで我々が定義してきたものを何ら変えるわけではありません。NotationはCoqのパーサに対してx + yをplus x yと解釈させたり、逆にplus x yをx + yと表記させたりするためのものです。

各表記法のシンボルは、表記法のスコープ内でのみ有効です。Coqはどのスコープであるかを推測しようとします。S(O*O)と書かれていた場合は、それをnat_scopeであると推測しますし、ソースにデカルト積（タプル）型bool*boolと書かれていたら、type_scopeであると推測します。時には(x*y)%natといった風に、nat]というような形でCoqからフィードバックされてくることもあります。

表記のスコープは、多くの場合数値に適用されます。ですので0%natという表記をO（オー）や0%Z（数値のゼロ）という意味で見ることがあります。

最初の方で、Coqにはほとんど何も用意されていない、という話をしましたが、本当のところ、数値を比較する関数すら自分で作らなければならないのです！!

beq_nat関数は自然数を比較してbool値を返すものです。入れ子になったmatchに気をつけて、以下のソースを読んでください。（二つの変数を一度にmatchさせる場合の書き方は、minusのところですでに登場しています）

同様に、ble_nat関数は自然数を比較して小さいか等しい、ということを調べてbool値を生成し返します。

練習問題: ★★ (blt_nat)

blt_nat関数は、自然数を比較して小さい、ということを調べてbool値を生成します（ natural numbers for less-than）。Fixpointを使用して１から作成するのではなく、すでにこれまで定義した関数を利用して定義しなさい。

注：simplタクティックを使ってうまくいかない場合は、代わりにcomputeを試してください。それはよりうまく作られたsimplと言えるものですが、そもそもシンプルでエレガントな解が書けていれば、simplで十分に評価できるはずです。

☐

簡約を用いた証明

ここまでに、いくつかの型や関数を定義してきました。が、ここからは少し目先を変えて、こういった型や関数の特性や振る舞いをどうやって知り、証明していくかを考えてみることにしましょう。実際には、すでにこれまでやってきたことでも、その一部に触れています。。例えば、前のセクションのExampleは、ある関数にある特定の値を入力した時の振る舞いについて、あらかじめ想定していたものと正確に一致していると主張してくれます。それらの主張が証明しているものは、以下のものと同じです。

=の両側の式を定義に基づいて簡約した結果は、一致している。

このような「簡約を用いた証明」は、関数のさらに興味深い性質をうまく証明することができます。例えば、0が自然数の加算における左単位元（0が、左から加えても値が変わらない値であること）であることの証明は、nが何であっても0 + nを注意深く縮小(簡約)したものがnになることを、+という関数が「最初の引数を引き継いで再帰的に定義されている」ということを考慮した上で示せればいいということです。

reflexivityコマンドは暗黙的に＝の両辺を簡約してから等しいかどうかを調べてくれます。そのため、上の証明はもう少し短くすることができます。

実際、reflexivityはsimplよりいくぶん多くのことをやってくれるので、覚えておくと後々便利でしょう。例えば、reflexivity は定義された句を展開したり、右辺と置き換えるといったことを試みます。この違いから、reflexivity が向いているのは、「reflexivity によって全てのゴールが自動的に証明され、reflexivity が見つけて展開した式をあえて見なくてもよい」という場合で、逆にsimplは、我々自身が新しいゴールを読んで理解すべき時（勝手に定義を展開し解釈して欲しくない時）に向いているということになります。

この定理と証明の様式は、以前示した例とほとんど同じですが、唯一の違いは、量化子が加えられている（∀ n:nat）ことと、Exampleの代わりにTheoremキーワードが使用されていることです。後者の違いは単なるスタイルの違いで、ExampleとTheorem（他にもLemma、Fact、Remarkなど）はCoqから見るとすべて同じ意味を持ちます。

simplやreflexivityはタクティックの例です。タクティックは、ProofとQedの間に記述され、Coqに対して、我々がしようとしている主張の正当性をどのようにチェックすべきかを指示するためのコマンドです。この講義の残りでは、まだ出てきていないタクティックのうちのいくつかを紹介していきましょう。さらにその後の講義ではもっと色々出てくるのですが。

練習問題: ★, optional (simpl_plus)

この問い合わせの結果、Coqが返す応答はなにか？

また次のものの場合はどうか？

この二つの違いを示せ。 ☐

introsタクティック

単体テストの際には対象の関数に対して特定の引数を渡すわけですが、プログラムの証明を行う上で注意を払うべきポイントは、それが量化子（任意のnについて、など）や仮定（m=nと仮定すると）で始まるか、ということです。そのような状況で求められるのは「仮定をたてて証明できる」ことです。例えば「よし、nを任意の数値としよう」「よし、仮にm=nと仮定してみよう」といった具合です。

introsタクティックは、このようなことを量化子や仮定をゴールから前提条件にき上げることで実現してくれます。

例えば、以下は同じ定理を少し異なるやり方で証明したものです。

次の証明をCoq上で逐次実行し、どのように状況が変化してゴールが導かれるのかをよく観察してください。

定理の名前についている_lという接尾辞は、「左の」と読みます。

書き換え（Rewriting）による証明

少しばかり興味深い定理を見てみましょう。

この定理は、あらゆるnやmについて完全に成り立つと言っているわけではなく、n = mが成り立つときに限って成立する、というもので、この矢印は"ならば"と一般的に読みます。

nとmが両方とも任意の数なのですから、これをこれまでの証明でやってきたように簡約することはできません。その代わりに、n = mならば、イコールの両側のnやmを互いに書き換えても等しさは変わらない、というところに注目します。このような書き換えをしてくれるのがrewriteタクティックです。

証明の1行目は、∀（forall）がついた、つまり「あらゆるn,mについて」の部分をコンテキストに移しています。2行目は、n = mならば、という仮定をコンテキストに写し、Hという名前をこれに与えています。3行目は、ゴールになっている式(n + n = m + m)に仮定Hの左側を右側にするような書き換えを施しています。

（rewriteの矢印は特に論理に関与していません。単に左側を右側に置き換えているだけです。逆に右側を左側に置き換えたい場合は、rewrite ←と書くこともできます。この逆の置き換えも上の証明で試して、Coqの振る舞いがどのように変わるかを観察してください。）

練習問題: ★ (plus_id_exercise)

Admitted.を削除し、証明を完成させなさい。

☐

Admittedコマンドは、Coqに対して「この証明はあきらめたので、この定理はこれでいいことにしてください」と指示するものです。この機能は、より長い証明をする際に便利です。何か大きな論証をしようとする時、今のところ信用している補足的な命題を示したい時があります。そんな時、Admittedを使用すると、その命題を一時的に信用できることにして、それを踏み台にしてより大きな論証を進めることができるのです。そしてそれが完成したのち、あらためて保留していた命題の証明を埋めればいいのです。ただし注意して下さい。admitやAdmittedを使用することは、一時的にドアを開けて、「全て形式的なチェックを受け証明済みの、信用するに足るCoqの世界」から、信用に値しない下界へ足を踏み出していることに他なりません。いつかは戻ってドアを閉めることがお約束です。

仮定の代わりに、前もって証明された定理を使ってもrewriteタクティックは同じように利用することができます。

練習問題: ★★, recommended (mult_1_plus)

☐

Case分析

もちろん、どんな命題でも簡単な計算だけで証明できるという訳ではありません。一般に、未知だったり仮定の（任意のbool、自然数、リストなど）値は、我々が検証しようとしている関数の先頭に記述され、それが簡約の邪魔をしてくれます。例えば、下のような命題をsimplタクティックだけで証明しようとすると、すぐに行き詰まってしまうでしょう。

その原因は、beq_natと+の定義で、共に最初の引数がmatchに渡されていることです。つまり、+に渡す最初の引数はnという未知数な上に、beq_natの引数はn + 1という複合式になっているため、そのまま簡約できないのです。

今求められていることは、nを何らかの条件に分割し、先に進めそうな形にすることができないかを検討することです。もしnがOなら、beq_nat (n + 1) 0の結果を得ることはできます。もちろん結果はfalseです。しかしもしnが何かのn'を使ってn = S n'と表せると考えても、我々はn + 1の値を得ることはできません。ただ、その式が一つのSで始まる（始まらないものはOにマッチする）ことに着目すると、beq_natの結果を計算して値を求めることができます。その結果結果beq_nat (n + 1) 0は、やはりfalseになるでしょう。

このことから、求められるタクティックはCoqにn = Oの場合とn = S n'の場合に分けて考えるように求めるようなもので、これを実現するのがdestructタクティックです。

destructタクティックは二つのサブゴールを作ります。その両方を別々に、Coqを使って定理として証明していくことになります。一つのサブゴールからもう一つへ移動するための特別なコマンドは必要ありません。一つ目のサブゴールが証明されれば、それは消えて自動的にもう一つのサブゴールにフォーカスが移ります。この証明では、二つに分かれたサブゴールのいずれもreflexivityを1回使うだけで簡単に証明できます。

destructについている注釈"as [| n']"は、"イントロパターン"と呼ばれるものです。これはCoqに対して、両方のサブゴールに元nだった変数をどのような変数名を使って取り入れるかを指示するものです。一般的に[]の間にあるものは"名前のリスト"で、"|"によって区切られます。このリストの最初の要素は空ですが、これはnatの最初のコンストラクタであるOが引数をとらないからです。二つ目のコンストラクタSは引数を一つ取りますので、リストの二つ目の要素であるn'を名前に使用します。

destructタクティックは帰納的に定義された型に対して使用できます。例えば、bool値の否定が反射的であること・・・つまり否定の否定が元と同じになることを証明してみましょう。

ここで使われているdestructにはas句がありませんが、ここで展開しているbの型boolの二つのコンストラクタが両方とも引数をとらないため、名前を指定する必要がないのです。このような場合、"as [|]"や"as []"のように書くこともできます。実際のところほとんどの場合destructのas句は省略可能です。その際はCoqの側で自動的に変数名をつけてくれます。これは確かに便利なのですが、よくない書き方とも言えます。Coqはしばしば名前付けに混乱して望ましくない結果を出す場合があります。

練習問題: ★ (zero_nbeq_plus_1)

☐

Caseへのネーミング

caseのサブゴールからサブゴールへ明示的に移動するためのコマンドがないことは、証明の過程と結果を表すスクリプトを読みにくくしていることも事実です。さらに大掛かりな証明では、caseの分析も階層化し、Coqを使って証明を進めていくことが苦痛に感じられるかもしれません（あるCaseが五つのサブゴールを持ち、残りの七つのCaseも他のCaseの内部にあるような状況を想像してみてください･･･）。インデントやコメントを上手に使うと多少は改善しますが、最もよい解決方法は"Case"タクティックを定義して使用することです。

CaseタクティックはCoqにビルトインされていませんので、自分で定義する必要があります。それがどのような仕組みで動いているかを理解する必要はありませんので、ここでは定義は跳ばして使用例から見ていくことにします。このサンプルは、Coqの機能のうちまだ解説していないstringライブラリとLtacコマンドを使用します。これらはカスタムタクティックを定義するときに使うもので、Aaron Bohannon の業績によるものです。

以下はCaseをどのように使うかのサンプルです。証明を順次実行して、コンテキストがどのように変わっていくかを観察しなさい。

Caseが行っていることは実はとても簡単です。Caseは、続けて指定されたタグ名を、今証明しようとしているゴールへのコンテキストに文字列として追加しているだけなのです。証明がサブゴールに到達し、証明されると、次のトップレベル（今しがた解決したゴールと兄弟関係にある）ゴールがアクティブになります。するとさっきCaseで指定した文字列がすでに証明を終えたcaseとしてコンテキストに現れます。これは健全性のチェックにもなります。もし今の証明が完了しておらず、コンテキストに残ったまま次のCaseタックティクを実行すると、エラーメッセージが表示されます。

ネストしたcaseの分析（今destructで解決しようとしているゴール自体が、他のdestructの産物であるような場合）のために、SCase("subcase")が用意されています。

練習問題: ★★ (andb_true_elim2)

destructを使い、case（もしくはsubcase）を作成して、以下の証明andb_true_elim2を完成させなさい。

☐

Coq上に証明の経過を記述する際、それをどのようにフォーマットするべきか、ということについてちゃんとしたルールというものはありません。行が分割され、証明の各段階が階層を持ち、それをインデントで表現するような場合は特にそうです。しかしながら、複数のサブゴールが作成された部分が明示的にCaseタクティックでマークされた場合は、それを行頭から記述することにします。そうしておけば、証明は読みやすくなり、それ以外でどんな方針のレイアウトが選ばれても、あまり問題になりません。

ここで、１行の長さをどれくらいにしておくべきか、ということにも触れておきましょう。始めたばかりのCoqユーザーは、証明全体を１行に収めようと、複数のタクティックを同じ行に書き、非常に長い行を書いてしまいがちです。よいスタイルというものは「ほどほど」のところにあります。特にあげるなら、一連の流れを１行に書くにしても1行80字程度にとどめておくべきでしょう。これ以上長くなると読むのも大変になりますし、印刷や画面表示もうまくいかない場合が多くなります。多くのエディタがこのような制限をかける機能を持っていますのでそれを使ってもいいでしょう。

帰納法

我々は以前、0が加法+の左単位元（左から加えても値が値が変わらない値）であることを引数を分解し評価することで証明しました。右から加える場合でも同じように証明できるのでしょうか？

･･･同じぐらい簡単、というわけにはいかないようです。reflexivityを使ってみても同じです。n + 0のn は任意の未知数であり、+の定義にあるmatchのせいで簡約できません。destruct nを使い、caseごとに推論するのも難しそうです。caseごとに考えるとn = 0のときはうまくいきますが、n = S n'のほうではn'で同じように詰まってしまいます。destruct n'でさらに一歩踏み込んでみたところで、nは任意の大きい数のまま動きません。どうやらまだ来たことがないところに迷い込んでしまったようです。

Caseによる解析は少しだけうまくいきそうに思えますが、やはり行き詰まります。

このような命題を証明する場合 － 実際、数値やリストや、その他の帰納的な定義を持つ型にまつわる証明の多くはそうなのですが － もっとずっと強力な推論規則が必要になります。それが「帰納法」です。

高校で習った帰納法の仕組みを思い出して、自然数を考えてみましょう。もしP(n)が自然数nに対する命題であるとすると、Pがどんなnに対しても成り立つことは、以下のような方法で証明できます。

• P(O)が成り立つことを示す;
• どんなn'に対しても、もしP(n')が成り立つならP(S n')も成り立つことを示す;
• これによって、P(n)がどんなnでも成り立つと結論される

Coqでは、それぞれのステップは同じですが順序は逆向きに考えます。まず、ゴールの証明である「任意のnについてP(n)が成り立つ」からはじめ、それを二つの独立したサブゴールに分割します（ここでinductionタクティックを使います）。その結果、一つ目のサブゴールはP(O)、二つ目はP(n') → P(S n')となるはずです。以下は、実際にinductionタクティックが先ほど証明しようとしていた定理にどう作用するかを示したものです。

destructのように、inductionタクティックもas...句を取り、サブゴールに導入する際の変数の名前を指定することができます。最初のブランチではnは0に置き換えられ、ゴールは0 + 0 = 0となり、簡約できる状態になります。二つ目のブランチでは、nはS n'に置き換えられ、n' + 0 = n'が前提としてコンテキストに付け加えられます。（この際、仮定にIHn'という名前がつけられます。これは「Induction Hypothesys for n'（n'についての帰納法の仮定）」というような意味です。二番目のゴールは(S n') + 0 = S n'となり、S (n' + 0) = S n'に簡約されます。ここから、帰納法の仮定n' + 0 = n'を使って証明の残りを完成させます。

練習問題: ★★, recommended (basic_induction)

☐

練習問題: ★★ (double_plus)

☐

練習問題: ★ (destruct_induction)

destructとinductionの違いを短く説明しなさい。

☐

形式的証明と非形式的証明

"非形式的な証明はアルゴリズムであり、形式的な証明はコードである"

数学的に厳格な証明を構成するとはどういうことなのか、という問題は、千年もの間哲学者を悩ませてきました。しかし少々雑な定義でよければ次のように書くこともができます。数学的な命題Pの証明とは、それを読む（あるいは聞く）人をして、Pがtrueであることを納得せしめる文章を書く（語る）ことである、と。このことから、証明はコミュニケーション行為であると言えるでしょう。

さて、このコミュニケーションの相手は、二種類に分けることができます。一方は、Coqのプログラムのように振る舞うような場合で、このケースでの「信用に値する」というのは、Pが形式的論理のルールに基づく確実な論理から導かれたもので、その証明が、このチェックを行うプログラムをガイドする秘訣になっているようなものです。そんな秘訣が「形式的証明」です。

一方、読者が人間的な存在で、証明が英語などの自然言語で書かれているようなケースは「非形式的証明」であると言えます。こんなケースでの成功の条件は「あまりきちんと明示しないこと」です。とにかく、読んでいる人に納得させてしまえる証明こそが「よい証明」なのです。しかしひとつの証明を複数の読者が見るような場合、ある論点について、ある人は特定の言い回しによって核心に至るかもしれませんが、人によってはそうではないかもしれません。もっと極端な人は、ただ知ったかぶりをする割りに経験は浅い、単なる「頭でっかち」であるかもしれません。そういった人たちを押しなべて納得させる唯一の方法は、ただ骨身を惜しまず細かいところまで論じることなのです。逆にある読者はこういったことに精通しているあまり、細かいことにこだわりすぎて全体的な流れを見失う、ということもあります。多くの人が望んでいることは総論としてどうなのか、ということを知ることで、細かいことを考えていくことは面倒なものです。結局のところ、非形式的な証明でみんなを納得させる標準的な方法はなさそうです。なぜなら、非形式的な書き方で想定される読者全員を納得させる方法はないからです。しかし実際のところ、数学者は複雑な数学的事柄についてたくさんの表記規則のおかげで、証明が正しいか否かを判断するための標準的かつ公正な方法がもたらされたのです。

我々はこのコースでCoqを使用しているのですから、それだけできちんと形式化された証明に乗っていると言えます。しかしこのことは、非形式的な表現を無視していい、ということではありません。形式的証明は多くの場合有効ですが、人と人との間で考えを伝えあう際には必ずしも効率的とは言えないものです。

例えば、下の例は加法が結合的であることを示すものです。

Coqはこのような証明を完璧にこなしてくれますが、上の証明は人間にとってはいささかのみこみにくいと言わざるを得ません。もしあなたがCoqに十分慣れていて、タクティックを次々と適用しながら証明を進めていき、コンテキストやゴールがどう変化していくかを頭の中だけでイメージしていくことができるようなレベルの人でも、上の証明はかなり複雑で、ほとんど理解不能に思えるかもしれません。それを横目に、数学者はサラサラとこんな風に書くでしょう。

• 定理：任意のn,m,pについて、以下が成り立つ
        n + (m + p) = (n + m) + p.
  
  証明：nについて帰納法を適用する。
  
  
  • まずn = 0と置くと、以下のようになる
            0 + (m + p) = (0 + m) + p.
    
    これは、+の定義から直接導くことができる。
    
    
  • 次にn = S n'と置き、帰納法の仮定を
            n' + (m + p) = (n' + m) + p.
    
    とすると、以下のような式が立つ。
            (S n') + (m + p) = ((S n') + m) + p.
    
    ここで、+の定義より、以下のように変形できる。
            S (n' + (m + p)) = S ((n' + m) + p),
    
    これは、直後の値について帰納法の仮定が成り立つことを示している。 ☐

どちらの表現も、やっていることは基本的に同じことです。これはもちろん偶然ではなく、Coqのinductionタクティックが、数学者が考えるのと同じ目標を、同じサブゴールとして、同じ順番で作成するように作られているだけです。しかしこの二つをよく見ると、重要な違いがあります。形式的証明は、ある部分（reflexivityを使っている部分など）ではより明示的ですが、それ以外のところはあまり明示的ではありません。特にあるポイントにおける証明の状態が、Coqの証明では明示されていません。一方、非形式的証明は、途中で何度も「今どのあたりで、どのようになっているか」を思い出させてくれるような書き方になっています。

形式的証明も、以下のように書けば構造が分かりすくなります。

練習問題: ★★ (plus_comm_informal)

plus_commの証明を、非形式的な証明に書き換えなさい。

定理：加法は可換である。

Proof: ☐

練習問題: ★★, optional (beq_nat_refl_informal)

次の証明を、plus_assoc の非形式的な証明を参考に書き換えなさい。Coqのタクティックを単に言い換えただけにならないように！

定理：true=beq_nat n n forany n.（任意のnについて、nはnと等しいという命題がtrueとなる）

Proof: ☐

練習問題: ★, optional (beq_nat_refl)

☐

証明の中で行う証明

Coqでは（非形式的な数学と同様に）大きな証明は高い頻度で、後に出てきた証明が前に出ている証明を参照するような定理の列に分割されます。しかし時折、証明がいくつかの自明で雑他な事実を必要とし、それがまたトップレベルの名前をつけるほどでもなかったりします。こういう場合、状態を単純化し、すでに使われている定理の右に出現するサブ定理を証明することができれば便利です。assertタクティックはこれを可能にしてくれます。例えば、最初の方でやった証明mult_0_plusは、plus_O_nと名付けられた定理の証明から参照されています。assertを使うとplus_O_nの証明をこんな風に行うことができます。

assertタクティックは、二つのサブゴールを取り込みます。最初のものはH:という接頭辞をつけているように、それ自身を主張するもので、Assertion Hと呼びます。 （まず注意が必要なのは、上で使用したdestructやinductionにas句をつけることで、assert (0 + n = n) as Hというようにassertionに名前をつけられることです。 もう一つ、証明に出てくるassertionに、Caseを使ってマーキングしている事も注目です。その理由は、読みやすさのため、というだけでなく、例えばCoqをインタラクティブに使っているとき、証明を進めている間にコンテキストから"Proof of assertion"という文字列が消える瞬間を観察することで、証明の完了を知ることができます。）二つ目のゴールは、assertを呼び出した場合と、コンテキストに0 + n = n : Hという仮定が得られることを除けば同じです。このことから、assertは、我々が証明しなければならない事実そのものとなるサブゴールと、その最初のサブゴールの証明がどのような値でも成り立つことを使って証明される事実となる二つ目のサブゴールを作成することが分かります。

実際assertは多くのシチュエーションで便利に使えるでしょう。例えば、(n + m) + (p + q) = (m + n) + (p + q)であることを証明するとしましょう。=の両側で異なるのは最初のカッコの中の+の両側のnとmが入れ替わっているだけで、このことは加法の交換法則(plus_comm）があるものを別のものに書き換えることに使用できることを示しています。しかしながら、rewriteタクティックは「どこに適用するか」を考える必要がある場合には少々おばかさんです。ここでは+が3箇所で使われていますがrewrite → plus_commは一番外側（つまり中央）の+にしか適用されません。

plus_commを、適用したいポイントに対して使用するには、まずn + m = m + nで始まるような補助定理（ここでは何とかしようとしているmとnを特定するため）を導き、それを望むrewriteに使用します。

練習問題: ★★★★ (mult_comm)

assertを使用して以下の証明を完成させなさい。ただしinduction（帰納法）を使用しないこと。

では、乗法が可換であることを証明しましょう。おそらく、補助的な定理を定義し、それを使って全体を証明することになると思います。先ほど証明したplus_swapが便利に使えるでしょう。

☐

練習問題: ★★, optional (evenb_n__oddb_Sn)

☐

さらなる練習問題

練習問題: ★★★, optional (more_exercises)

紙を何枚か用意して、下に続く定理が(a)簡約と書き換えだけで証明可能か、(b)destructを使ったcase分割が必要になるか、(c)帰納法が必要となるか、のいずれに属すかを、紙の上だけで考えなさい。予測を紙に書いたら、実際に証明を完成させなさい。証明にはCoqを用いてかまいません。最初に紙を使ったのは「初心忘れるべからず」といった理由です。

☐

練習問題: ★★, optional (plus_swap')

replaceタクティックは、特定のサブタームを置き換えたいものと置き換えることができます。もう少し正確に言うと、replace (t) with (u)は、ゴールにあるtという式を全てuにかきかえ、t = uというサブゴールを追加します。この機能は、通常のrewriteがゴールの思い通りの場所に作用してくれない場合に有効です。

replaceタクティックを使用してplus_swap'の証明をしなさい。ただしplus_swapのようにassert (n + m = m + n)を使用しないで証明を完成させなさい。

☐

練習問題: ★★★★, recommended (binary)

これまでとは異なる、通常表記の自然数ではなく2進のシステムで、自然数のより効率的な表現を考えなさい。それは自然数をゼロとゼロに1を加える加算器からなるものを定義する代わりに、以下のような2進の形で表すものです。2進数とは、

• ゼロであるか,
• 2進数を2倍したものか,
• 2進数を2倍したものに1を加えたもの.

(a) まず、以下のnatの定義に対応するような2進型binの帰納的な定義を完成させなさい。 (ヒント: nat型の定義を思い出してください。
    Inductive nat : Type :=
      | O : nat
      | S : nat → nat.

nat型の定義OやSの意味が何かを語るものではなく、（Oが実際に何であろうが）Oがnatであって、nがnatならSが何であろうとS nはnatである、ということを示しているだけです。「Oがゼロで、Sは1を加える」という実装がそれを自然数としてみて実際に関数を書き、実行したり証明したりしてみてはじめて実際に意識されます。ここで定義するbinも同様で、次に書く関数が書かれてはじめて型binに実際の数学的な意味が与えられます。)

(b) 先に定義したbin型の値をインクリメントする関数を作成しなさい。また、bin型をnat型に変換する関数も作成しなさい。

(c) 最後にbで作成したインクリメント関数と、2進→自然数関数が可換であることを証明しなさい。これを証明するには、bin値をまずインクリメントしたものを自然数に変換したものが、先に自然数変換した後にインクリメントしたものの値と等しいことを証明すればよい。

☐

練習問題: ★★★★★ (binary_inverse)

この練習問題は前の問題の続きで、2進数に関するものである。前の問題で作成された定義や定理をここで用いてもよい。

(a) まず自然数を2進数に変換する関数を書きなさい。そして「任意の自然数からスタートし、それを2進数にコンバートし、それをさらに自然数にコンバートすると、スタート時の自然数に戻ることを証明しなさい。

(b) あなたはきっと、逆方向についての証明をしたほうがいいのでは、と考えているでしょう。それは、任意の2進数から始まり、それを自然数にコンバートしてから、また2進数にコンバートし直したものが、元の自然数と一致する、という証明です。しかしながら、この結果はtrueにはなりません。！！その原因を説明しなさい。

(c) 2進数を引数として取り、それを一度自然数に変換した後、また2進数に変換したものを返すnormalize関数を作成し、証明しなさい。

練習問題: ★★, optional (decreasing)

各関数の引数のいくつかが"減少的"でなければならない、という要求仕様は、Coqのデザインにおいて基礎となっているものです。特に、そのことによって、Coq上で作成された関数が、どんな入力を与えられても必ずいつか終了する、ということが保障されています。しかし、Coqの"減少的な解析"が「とても洗練されているとまではいえない」ため、時には不自然な書き方で関数を定義しなければならない、ということもあります。

これを具体的に感じるため、Fixpointで定義された、より「微妙な」関数の書き方を考えてみましょう（自然数に関する簡単な関数でかまいません）。それが全ての入力で停止することと、Coqがそれを、この制限のため受け入れてくれないことを確認しなさい。

☐