始める前に、前の章の定義をここに持ってきます。

Require Exportを動かすには、Basics.vをコンパイルしてできるBasics.voを、LFという名称と結びついたフォルダに配置する必要があります。 ちょうど .java のファイルから .class を作ったり、 .c のファイルから .o を作ったりするのと同じです。 まず、_CoqProjectという名前のファイルの最初に、次の一行を追加します。 （もしこの「論理の基礎」全体を持っているならば、_CoqProjectは存在するはずですので、この手順は飛ばしてかまいません。）

      -Q . LF

この記述で今いるフォルダ（Basics.vやInduction.vなどが入っている"."）を"LF"と関連付けます。 PG（Proof General）やCoqIDEは_CoqProjectを自動で読み取るので、LF.BasicsというライブラリについてBasics.voをどこから探せばよいかがわかるようになります。 一度_CoqProjectを作っておけば、様々な方法でBasics.voを作成できます。

• Proof Generalで：Emacsの変数coq-compile-before-requireをtに設定することで、RequireをPGに読み込ませたときに自動的に作成されます。
• CoqIDEで：Basics.vを開き、メニューの"Compile"から"Compile Buffer"を選びます。
• コマンドラインで：まずCoqに付随するツールcoq_makefileを使って以下のようにしてMakefileを作ります。 （「論理の基礎」全体を持っているならば既に存在するはずですので、この手順は飛ばしてかまいません。） （訳注：翻訳版ではcoq_makefileが作るMakefileをカスタマイズしているので、この手順を行うと挙動が変わってしまいます。）
  coq_makefile -f _CoqProject *.v -o Makefile
  メモ：自分でファイルを追加したり削除したりする場合は上のコマンドを再実行してMakefileを更新しなければなりません。
  あとはBasic.voを作るためにmakeコマンドのターゲットとして指定します。
  make Basics.vo
  全てのファイルをコンパイルしたければ、何も引数を入れずにmakeコマンドを使います。
  make
  内部ではmakeコマンドはCoqのコンパイラであるcoqcを使います。 直接coqcを使って、次のようにコンパイルすることもできます。
  coqc -Q . LF Basics.v
  しかし、makeはコンパイルする以外にもソースファイルの依存関係を解析して必要なファイルを適切な順序でコンパイルしてくれるので、coqcを直接使うよりmakeコマンドの方がよいでしょう。

もし識別子が見つからないなどのエラーが出たりしたら、Coqの"load path"が正しく設定されていないせいかもしれません。 Print LoadPath.というコマンドで正しく設定されているか確認してみてください。 特に、 Compiled library Foo makes inconsistent assumptions over library Bar というメッセージが表示される場合、Coqが複数インストールされていないか確認してください。 入っていた場合、ターミナルからコマンドとして使っているCoq（coqcなど）とProof GeneralやCoqIDEが使っているCoqが異なる可能性があります。

• もう一つ、Fooを再コンパイルせずにBarが変更されてコンパイルされた場合などにも発生します。 Fooを再コンパイルするか、いろんなファイルが影響するようなら全体を再コンパイルしてください。 （3つ目の方法であるmakeを使って make clean; make を実行します。）

もう一点CoqIDEユーザへ： もしError: Unable to locate library Basics というメッセージが表示される場合、「CoqIDE内」のコンパイルと「ターミナル上のcoqc」のコンパイルによる不整合が考えられます。 よくある原因としては、互換性のない二つのバージョンのcoqc（一方はCoqIDEから使われ、もう一方はターミナルから使用されている）が存在するというものです。 この場合、常にコンパイルをCoqIDEからのみ（例えば"make"をメニューから選んで）コンパイルし、ターミナルから呼び出さないようにしましょう。

帰納法による証明

前の章では、0が+に対する左単位元であることを証明しました。 実際には、0は「右(right)」単位元でもあるのですが...

... しかし、これは左単位元ほど簡単には示せません。 reflexivityを使ってもうまくいきません。 というのも、n + 0にあるnはよく分からない数なので、+の定義におけるmatchは簡約されないのです。

destruct nを使った場合分けもやはり先には進められません。 n = 0のときはいいのですが、n = S n'のときは同じ理由で詰まってしまいます。

destruct n'を使って進められますが、nがいくらでも大きくなりうるので、このやり方ではいつまで経っても終わりません。

これらの、大体の数やリストなどの帰納的に定義された集合に関する性質を示すには、より強力な道具、「帰納法(induction)」が必要になります。 高校や離散数学の講義などで習ったと思いますが、「自然数に関する帰納法（数学的帰納法）の原理」をおさらいしておきましょう。 もしP(n)が自然数nに関する命題だったとすると、任意の数nに対しPが成り立つことを、次のように示すのでした。

• P(O)が成り立つことを示す。
• どんなn'についても、P(n')が成り立つならば、P(S n')が成り立つことを示す。
• 以上から、任意のnについてP(n)が成り立つと言える。

Coqではこれを同じようにします。 任意のnでP(n)が成り立つことをゴールとして示すときに、それを（inductionタクティックを使うことで）、二つのサブゴールに分けます。 一つ目はP(O)の証明、そして次はP(n') -> P(S n')の証明です。 どのようになるのかを例を使って見ていきましょう。

destructタクティックと同様に、inductionタクティックには、サブゴールで使う変数を指定するas...節を使うことができます。 二つに分かれているので、as...節も|で二つに分かれています。 （厳密に言うと、ここではas...節は省略できて、その場合Coqが名前を付けてくれます。 ただし、実際には、これはあまりいい方法ではありません。 というのも、Coqが自動で付ける名前では混乱しがちだからです。） 一つ目のサブゴールでは、nは0に置き換えられています。 新しい変数は特に導入されていません（そのためas...の一つ目は空になっています）。 ゴールは0 = 0 + 0となっていて、これは簡約すれば示せます。 二つ目のサブゴールでは、nはS n'に置き換えられ、仮定としてIHn'という名前（つまりn'に関する帰納法の仮定(Induction Hypothesis)）でn' = n' + 0が文脈に追加されます。 n'とIHn'という二つの名前はas...節の二つ目で指定しています。 ゴールはS n' = (S n') + 0となっていますが、簡約するとS n' = S (n' + 0)になります。 これは帰納法の仮定であるIHn'から示せます。

（実のところ、上の証明ではintrosタクティクは冗長です。 量化変数を持つゴールに対してinductionタクティクを適用すると、これらの変数は必要に応じて文脈に移動されます。）

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

以下の定理を帰納法で証明しなさい。 証明には、前に示した内容を使う必要があるかもしれません。

☐

練習問題: ★★, standard (double_plus)

次のように、引数を二倍にする関数を定義します。

帰納法を使って、doubleに関する以下の性質を証明しなさい。

☐

練習問題: ★★, standard, optional (evenb_S)

evenb nの定義の不便な点は、再帰呼び出しがn - 2に対して行われているというものです。 これにより、evenb nに関する性質の証明をnに基づく帰納法で行う場合に、再帰呼び出しに関する性質を得るにはn - 2に対する仮定が必要となります。 このため、そのままでは帰納法で示すことが難しくなっています。 次の補題はevenb (S n)の特徴付けを行っています。 これを用いることで、帰納法での扱いが容易になります。

☐

練習問題: ★, standard (destruct_induction)

destructとinductionの違いについて大まかに説明しなさい。

☐

証明の中の証明

Coqでは、通常の数学のように、大きな証明を複数の定理の列に分割して、後ろの証明で前の定理を利用する、ということをします。 しかし、このように分割した定理の中には、内容が自明だったり全く一般的でなかったりするため、全体に見える名前を付けるのが面倒になるものも現れます。 こういう場合、その場所でだけ使うように「副定理」を記述、証明できると便利です。 これを可能にするのがassertタクティックです。 例えば、前に証明したmult_0_plusという定理ではplus_O_nという名前の定理を使っていました。 これをassertを使い、plus_O_nの記述と証明を書くと次のようになります。

assertタクティックは二つのサブゴールを作ります。 一つ目は表明したものそのものです。 H:という記述は、表明したものをHと名付けることを意味します。 （destructやinduction同様に、asを使ってassert (0 + n = n) as Hと書くこともできます。） ここで、表明の証明を波括弧{ ... }で囲ったのは、可読性のためという理由の他に、Coqの対話環境では、この部分の証明が終わったことがわかりやすくなるという理由もあります。 二つ目のゴールはassertを実行したものと同じですが、文脈にHという名前で0 + n = nの仮定が入っています。 つまり、assertは一つのサブゴールで表明した内容を証明させ、二つ目のサブゴールで元の場所に戻り、表明した内容を使って証明を進めさせるのです。

assertの他の使用例です。

例えば、(n + m) + (p + q) = (m + n) + (p + q)を示す必要があったとします。 =の左右での差はmとnの位置が+の間で入れ替わっているだけですから、加算の可換律（plus_comm）で書き換えれば簡単に示せるはずです。 ただ、rewriteタクティックは「どこを」書き換えるかに関してはあまり賢くないので、今回はrewrite -> plus_commを実行しても、3箇所存在する+のうち「外側」のものを書き換えてしまいます。

plus_commを必要な場所に使うために、n + m = m + n（ただしmとnは今の文脈にある変数）をassertを使って補題として作る方法があります。 この補題をplus_commで示し、それを使って意図通りに式を書き換えるのです。

形式的証明　対　非形式的証明

「非形式的証明はアルゴリズムで、形式的証明はコードだ。」

数学的な言明に対して「よい証明」とは一体何でしょうか？この 問いは、数千年に渡り議論されていますが、大まかに合意されている定義は次のようになります。 「数学的命題Pに対する証明とは、読み手（聞き手）が確かにPは正しいと信じるに足るような記述（発言）、すなわちPの正しさを否定できないような議論である。」 つまり、証明とはコミュニケーションであるということです。 コミュニケーションは、様々な「読み手」と行われます。 あるときには、この「読み手」はCoqのようなプログラムでしょう。 この場合、信じさせるための「信条」はPが形式的に定義された論理規則から導出できるということであり、証明はこれを確かめるためにプログラムを案内するレシピということになります。 このレシピを「形式的(formal)」証明といいます。 また別のときには、「読み手」が人間であることもあるでしょう。 この場合、証明は英語や日本語などの自然言語で書かれることになり、結果として「非形式的(informal)」になります。 こちらは、コミュニケーション時の戦略はそこまではっきりとはしません。 「妥当な」証明ならば、読み手がPを信じるでしょう。 しかし、読み手には、ある特定の書き方でないと信じない人もいれば、その書き方では信じられない人もいます。 もしその読み手が、特別融通が利かなかったり、過度に未熟だったり、頭の回転が非常に鈍い人だったりすると、信じさせるには綿密に詳細を記述しなければならないでしょう。 一方で、その分野に詳しい人がその証明を読んだ場合、あまりの詳細の記述に全体の流れを追えなくなってしまうでしょう。 そのような読み手が知りたいのは証明における主なアイディアです。 なぜなら、その人にとっては、ひたすら書かれた記述を理解するよりも、細部を自分で埋める方が楽なのです。 究極的には、証明の記述方法の普遍的標準などありません。 あり得る読み手全員が信じるに足るような非形式的証明の記述方法が存在しないからです。 ただし実際には、複雑な内容を記述するための、多彩な慣習や慣用表現が作られています。 これらを用いることで、少なくとも特定のコミュニティの中では、コミュニケーションをかなり円滑に進めることができます。 こう言った慣習は、かなり明確に証明の良し悪しを判定する基準があります。 この講義ではCoqを使っていますので、かなり形式的証明を扱うことになります。 しかし、だからといって非形式的証明を忘れていいわけではありません！ 形式的証明は様々な点で有用なのですが、他の人とアイディアを交わしたりといったことには全くもって非効率的です。

例えば、次の証明は加算が結合的であることを示しています。

この証明はCoqにとっては完璧です。 しかし人間からすると、直観的に理解することは難しいものです。 コメントやbulletを使って証明の構成を記述すれば、少し読みやすくなります。

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の証明上には全く現れませんが、非形式的証明では現状確認のために明示されています）。

練習問題: ★★, advanced, recommended (plus_comm_informal)

plus_commの（課題として解いた）証明を非形式的証明で書きなさい。 定理： 加算は可換律を満たす。 証明：

☐

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

plus_assocの非形式的証明を参考に、次の定理の非形式的証明を書きなさい。 Coqのタクティックを日本語に変換するだけではだめです！ 定理： 任意のnについて、true = n =? nが成立する。 証明： ☐

発展課題

練習問題: ★★★, standard, recommended (mult_comm)

assertを使い、次の定理を示しなさい。 ここではplus_swapに対してinductionを使ってはいけません。

次に乗算の可換律を示しなさい。 （補助定理を一つ示す必要があるでしょう。 plus_swapを使うといいかもしれません。）

☐

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

紙を準備し、以下の定理のそれぞれに対して、 (a)簡約と書き換えだけで示せるか、 (b)場合分け（destruct）が必要か、 (c)帰納法が必要か、 を考え、その予想を書きなさい。 それが終わったら、実際に証明しなさい。 （紙に書いた予想をコード中に書いたりしなくて構いません。 手を動かす前に一度考えてもらうために使ったのです。）

☐

練習問題: ★★, standard, optional (eqb_refl)

次の定理を示しなさい。 （trueを等号の左辺に置くのは奇妙に見えるかもしれませんが、これは標準ライブラリにある定理に合わせたためです。 書き換えは両方向で可能なので、どちらで記述しても問題はありません。）

☐

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

replaceタクティックは、特定の部分式を指定した別の式に書き換えるのに使います。 replace (t) with (u)の形で、ゴールに存在するtを全てuに書き換え、サブゴールとしてt = uを作ります。 rewriteでの書き換えが意図通りに行えないときに便利です。 replaceを使って次のplus_swap'を証明しなさい。 証明はほとんどplus_swapと同じですが、assert (n + m = m + n)を書かないようにしなさい。

☐

練習問題: ★★★, standard, recommended (binary_commute)

Basicsの章のbinaryという課題で書いた、incrementとbin_to_nat関数に関してです。 以下の図が可換であることを示しなさい。

                            incr 
              bin ----------------------> bin 
               |                           | 
    bin_to_nat |                           |  bin_to_nat 
               |                           | 
               v                           v 
              nat ----------------------> nat 
                             S 

つまり、2進数を1増やしてから（1進の）自然数に変換した結果と、変換を先にしてから1増やした結果が一致するということです。 名前はbin_to_nat_pres_incrとします（presは保存(preserve)です）。 始める前に、binaryに書いた定義から証明しやすい形に変更しても構いません。

☐

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

この課題は2進数に関する課題の続きで、場合によっては前の定義を変更しなければいけないかもしれません。 (a) まず、自然数から2進数へ変換する関数を書きなさい。

そして、natから2進数に変換し、逆に変換した結果が元のnatと一致することを示しなさい。 （ヒント：もしnat_to_binの定義に別の関数を利用しているならば、その関数がどのようにnat_to_binと関係しているかの補題を示すひつようがあるでしょう。）

(b) 逆方向も示した方がいいのでは？と思うでしょう。 逆とはつまり、2進数を自然数に変換し、それをまた2進数に戻すと、元の2進数になる、というものです。 しかし、これは正しくありません。 なぜそうなるのかを（コメントとして）説明しなさい。

(c) 2進数を「直接」正規化するnormalize関数を定義しなさい。 normalize関数はbinからbinへの関数であり、自然数に変換せずに2進数のまま計算を行う関数です。 2進数bを自然数に変換してそれを2進数に逆変換すると、normalize bと一致しなければなりません。 これを示しなさい。 （注意：証明はトリッキーです。 いくつかの補題を示す必要があるでしょう。 手順としては、求められた性質について直接証明してみて、詰まった状況を確認し、必要そうな補題を定めて証明を進められることを確認していく、という流れがよいでしょう。 もちろんその補題を示すには別途帰納法が必要になるでしょう。） normalizeを定義するのに nat_to_bin や bin_to_nat を使ってはいけません！

☐