数のペア

Inductive による型定義では、各構成子は任意の個数の引数を取ることができました。 true や O のように引数のないもの、 S のようにひとつのもの、また、ふたつ以上取るものも nybble や以下のように定義することができます。

この定義は以下のように読めます。 「数のペアを構成する方法がただひとつある。それは、構成子 pair を nat 型のふたつの引数に適用することである。」

ペアの第一要素と第二要素を取り出す関数を定義します。

ペアはよく使うので、 pair x y ではなく、数学の標準的な記法で (x, y) と書けるとよいでしょう。 このような記法を使うためには Notation 宣言を使います。

こうして定義したペアの新しい記法（notation）は、式だけでなくパターンマッチに使うこともできます。

Note that pattern-matching on a pair (with parentheses: (x, y)) is not to be confused with the "multiple pattern" syntax (with no parentheses: x, y) that we have seen previously. The above examples illustrate pattern matching on a pair with elements x and y, whereas minus below (taken from Basics) performs pattern matching on the values n and m. Fixpoint minus (n m : nat) : nat := match n, m with | O , _ => O | S _ , O => n | S n', S m' => minus n' m' end. The distinction is minor, but it is worth knowing that they are not the same. For instance, the following definitions are ill-formed: Definition bad_fst (p : natprod) : nat := match p with | x, y => x end. Definition bad_minus (n m : nat) : nat := match n, m with | (O , _ ) => O | (S _ , O ) => n | (S n', S m') => bad_minus n' m' end.

それでは、数のペアに関する簡単な事実をいくつか証明してみましょう。 一定の形式で書いておくと、単に reflexivity（と組み込みの簡約）だけで証明できます。

しかし、補題を以下のようにより自然な書き方をした場合、reflexivityでは足りません。

simpl で fst や snd の中のパターンマッチを実行できるよう、 p の構造を明らかにする必要があります。 これには destruct を使います。

2つのサブゴールを生成していた nat の場合と異なり、 destruct でサブゴールが増えることはありません。 これは、 natprod の構成法がひとつしかないからです。

練習問題: ★, standard (snd_fst_is_swap)

☐

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

☐

数のリスト

ペアの定義を一般化することで、数の「リスト(list)」は次のように表すことができます。 「リストは、空のリストであるか、または数と他のリストをペアにしたものである。」

たとえば、次の定義は要素が三つのリストです

ペアの場合と同じく、リストをプログラミング言語で馴染んだ記法で書くことができると便利でしょう。 次の宣言では :: を中置の cons 演算子として使えるようにし、角括弧をリストを構成するための外置（outfix）記法として使えるようにしています。

この宣言を詳細まで理解する必要はありませんが、興味のある読者のために簡単に説明しておきます。 right associativity アノテーションは複数の :: を使った式にどのように括弧を付けるか指示するものです。 例えば、次の三つの宣言はすべて同じ意味に解釈されます。

at level 60 の部分は :: を他の中置演算子といっしょに使っている式にどのように括弧を付けるかを指示するものです。 例えば、 + を plus に対する level 50 の中置記法として定義したので、
  Notation "x + y" := (plus x y)
                      (at level 50, left associativity).

+ は :: よりも強く結合し、 1 + 2 :: [3] は期待通り、 1 + (2 :: [3]) ではなく (1 + 2) :: [3] と構文解析されます。 （.v ファイルを読んでいるときには "1 + 2 :: [3]" のような書き方は少し読みにくいように感じるでしょう。 内側の 3 の左右の角括弧はリストを表すものですが、外側の括弧は "coqdoc" 用の命令で、角括弧内の部分をそのままのテキストではなく Coq のコードとして表示するよう指示するものです。 この角括弧は生成された HTML には現れません。） 上の二番目と三番目の Notation 宣言は標準的なリストの記法を導入するためのものです。 三番目の Notation の右辺は、 n 引数の記法を二項構成子の入れ子に変換する記法を定義するための Coq の構文の例です。

Repeat

リストを操作するために便利な関数がいくつかあります。 例えば、 repeat 関数は数 n と count を取り、各要素が n で長さ count のリストを返します。

Length

length 関数はリストの長さを計算します。

Append

app 関数はふたつのリストを連結(append)します。

app はこの後でよく使うので、中置演算子を用意しておくと便利でしょう。

先頭（デフォルト値付き）と後ろ

もうふたつリストを使った例を見てみましょう。 hd 関数はリストの最初の要素（先頭—— head）を返し、 tl は最初の要素を除いたもの（後ろ―― tail）を返します。 空のリストには最初の要素はありませんから、その場合に返す値を引数として渡しておかなければなりません。

練習問題

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

以下の nonzeros、 oddmembers、 countoddmembers の定義を完成させなさい。 どのように動くかは続くテストから考えてください。

☐

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

alternate の定義を完成させなさい。 この関数は、ふたつのリストから交互に要素を取り出しひとつにまとめる関数です。 具体的な例は下のテストを見てください。 （注意: alternate の自然な定義のひとつは、 Coq の要求する「Fixpoint による定義は『明らかに停止する』ものでなければならない」という性質を満たすことができません。 このパターンにはまってしまったようであれば、両方のリストの要素を同時に見ていくような少し冗長な方法を探してみてください。 新しい対を定義する必要のある解法もありますが、それ以外にもあります。）

☐

リストを使ったバッグ

バッグ（bag、または多重集合—— multiset）は集合のようなものですが、それぞれの要素が一度きりではなく複数回現れることのできるようなものを言います。 数のバッグの表現としては数のリストがありえます。

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

バッグに対する count、 sum、 add、 member 関数の定義を完成させなさい。

下の証明はすべて reflexivity だけでできます。

多重集合の sum （直和、または非交和）は集合の union （和）と同じようなものです。 sum a b は a と b の両方の要素を持つ多重集合です。 （数学者は通常、多重集合の union に少し異なる定義として、和(sum)を使う代わりに最大(max)を使ったものを与えます。 それが、この関数の名前を union にしなかった理由です。） sum のヘッダには引数の名前を与えませんでした。 さらに、 Fixpoint ではなく Definition を使っています。 ですから、引数に名前がついていたとしても再帰的な処理はできません。 問題をこのように設定したのは、 sum を（定義済みの関数を使うといった）別の方法で定義できないか考えさせるためです。

☐

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

練習として、さらに以下のbag用の関数を作成しなさい。

remove_one を削除しようとしている数の入っていないバッグに適用した場合は、同じバッグを変更せずに返す。 （この練習問題はオプション問題ですが、後ろの発展問題で remove_one の定義を必要とするものがあります。）

☐

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

count や add を使ったバッグに関する面白い定理を書き、それを証明しなさい。 この問題はいわゆる自由課題で、真であっても、証明にまだ習っていない技法を使わなければならない定理を思いついてしまうかもしれません。 証明に行き詰まってしまったら気軽に質問してください。

リストに関する推論

数の場合と同じく、リスト処理関数についての簡単な事実はもっぱら簡約のみで証明できることがあります。 たとえば、次の定理は reflexivity で行われる簡約だけで証明できます。

これは、 [] が app の定義における「被検査体(scrutinee)」（パターンマッチでその値が「検査(scrutinize)」される式 / 訳注：matchとwithの間に書いた式）に代入され、パターンマッチが簡約できるようになるからです。

またこれも数の場合と同じように、未知のリストの形（空であるかどうか）に応じた場合分けも有効です。

ここで、 nil の場合がうまく行くのは、 tl nil = nil と定義したからです。 ここでは、 destruct タクティックの as で n と l' のふたつの名前を導入しました。 これは、リストの cons 構成子が引数をふたつ（構成するリストの頭部と尾部）取ることに対応しています。

ただし、リストに関する興味深い定理の証明には、帰納法が必要になるのが普通です。

お小言

単にスクリプトを「読んでいる」だけでは大きな進歩は望めません！ 各スクリプトを実際に Coq で一歩一歩進め、各ステップがその証明にどのようにかかわっているか考えることが大切です。 そうしなければ、演習に取り組んでも何の意味もありません。 もうおわかりですよね？

リスト上の帰納法

natlist のようなデータ型に対して帰納法で証明をするのは、普通の自然数に対する帰納法よりも馴染みにくさを感じたことでしょう。 しかし、考え方は同様に単純です。 Inductive 宣言では、宣言した構成子を使って構築できる値の集合を定義しています。 例えば、ブール値では true と false のいずれかであり、数では O か数に対する S のいずれか、リストであれば nil か数とリストに対する cons のいずれかです。 さらに言えば、帰納的に定義された集合の要素になるのは、宣言した構成子を互いに適用したものだけです。 このことがそのまま帰納的に定義された集合に関する推論の方法になります。 すなわち、数は O であるか、より小さい数に S を適用したものであるかのいずれかです。 リストは nil であるか、何らかの数とより小さいリストに cons を適用したものです。 他のものも同様です。 ですから、あるリスト l に関する命題 P があり、 P がすべてのリストに対して成り立つことを示したい場合には、次のように推論します。

• まず、 l が nil のとき P が l について成り立つことを示す。
• それから、 l が cons n l' であるとき、ある数 n とより小さいリスト l' に対して、 P が l' について成り立つと仮定すれば P が l についても成り立つことを示す。

大きなリストはそれより小さなリストからのみ作り出され、少しずつ nil に近付いて行きます。 よって、このふたつの言明からすべてのリスト l に関して P が真であることが言えます。 具体的な例で説明しましょう。

自然数上の帰納法と同様に、inductionタクティックでのas ...節はconsの場合の残りのリストにl1'と名前を付けるために使われています。 蒸し返すようですが、この Coq の証明はこうして単に静的なテキストとして読んでいる限り、さほど明白で分かりやすいものではありません。 Coq の証明は、 Coq を対話的に動かしながらポイントごとに「現在のゴールは何か」「コンテキストに何が出ているか」を見て、証明が今どうなっているかを読み下していくことで理解されるようになっています。 しかし、このような証明の途中経過は、全てが証明結果として書き出されるわけではありません。 だからこそ、人間向けの自然言語での証明には証明の筋道がわかるように証明の指針を書いておく必要があるのです。 特に、読者が流れを見失わないよう、ふたつめの場合分けで使う帰納法の仮定が何だったのかわかるようにしておくのは有益なはずです。

比較するために、この定理の非形式的証明を以下に載せます。

定理: 任意のリスト l1、 l2、 l3 について、 (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3) が成り立つ。 証明: l1 についての帰納法で証明する

• まず、 l1 = [] と仮定して
         ([] ++ l2) ++ l3 = [] ++ (l2 ++ l3)
  を示す。これは ++ の定義から自明である。
• 次に l1 = n::l1' かつ
         (l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3)
  （帰納法の仮定）と仮定して
         ((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3)
  を示す。 ++ の定義から、この式は以下のように変形できる。
         n :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3))
  これは帰納法の仮定から直接導かれる。 ☐

リストの反転

より入り組んだリストに関する帰納法による証明の例として、リストを反転させる関数revを使います。 revの定義にはappを使うことにします。

rev の性質

ここまで見てきたものよりも難易度の高いものですが、リストを反転しても長さの変わらないことを証明します。 下の方法では、ふたつめの場合分けで行き詰まってしまいます。

++ と length に関する等式が成り立つことを示せれば証明が先に進むはずです。 この等式を別個の補題として記述してみましょう。

補題をできる限り一般的なものにするため、revの定義で出てくるような結果に対してではなく、「全ての」natlistに対するものとして形式化しました。 目的としたゴールは明らかにリストの反転という状態に全く依存していないという点で、この一般化は自然なものでしょう。 さらに、この一般的な性質の方がより簡単に証明できます。

これで、元々の証明ができるようになりました。

対比として、この二つの定理の非形式的な証明を見てみましょう 定理: 二つのリスト l1 と l2 について、 length (l1 ++ l2) = length l1 + length l2 が成り立つ。 証明: l1 についての帰納法で証明する。

• まず、 l1 = [] と仮定して
          length ([] ++ l2) = length [] + length l2
  を示す。これは length と ++ の定義から直接導かれる。
• 次に、 l1 = n::l1' かつ
          length (l1' ++ l2) = length l1' + length l2
  と仮定して、
          length ((n::l1') ++ l2) = length (n::l1') + length l2)
  を示す。これは length と ++ の定義および帰納法の仮定から明らかである。 ☐

定理: 任意のリスト l について length (rev l) = length l が成り立つ。 証明: l についての帰納法で証明する。

• まず、 l = [] と仮定して
            length (rev []) = length []
  を示す。これは length と rev の定義から直接導かれる
• 次に、 l = n::l' かつ
            length (rev l') = length l'
  と仮定して、
            length (rev (n :: l')) = length (n :: l')
  を示す。 rev の定義から次のように変形できる。
            length ((rev l') ++ [n]) = S (length l')
  これは、先程の補題から、次のものと同じである。
            length (rev l') + length [n] = S (length l')
  これは、length の定義および帰納法の仮定から明らかである。 ☐

こういった証明のスタイルは、長ったらしく杓子定規な感じがします。 最初の何回かは別にして、それ以後は、細かいところは省略してしまって（必要なら頭の中や紙の上で追うのは簡単ですから）、自明でないところにだけ注目した方がわかりやすいでしょう。 そのように省略がちに書けば、上の証明は次のようになります。

定理: 任意のリスト l について length (rev l) = length l が成り立つ。 証明: まず、任意の l について length (l ++ [n]) = S (length l) であることに注目する（これは l についての帰納法から自明である）。 もとの性質については、 l についての帰納法から示し、 l = n'::l' の場合については、上の性質と帰納法の仮定から導かれる。 ☐

どちらのスタイルの方が好ましいかは、読み手の証明への馴れや、彼らが今まで触れてきた証明がどちらに近いかに依ります。 本書の目的としては冗長なスタイルの方が無難でしょう。

Search

これまで見てきたように、定理を証明するには既に証明した定理を、例えばrewriteを通じて、使うことができます。 しかし、定理を使うためにはその名前を知らなければなりません！ 使えそうな定理の名前をすべて覚えておくのはとても大変です。 今まで証明した定理を覚えておくだけでも大変なのに、その名前となったら尚更です。 Coq の Search コマンドはこのような場合にとても便利です。 スクリプトファイルに Search foo と書いて評価させると、 foo に関する証明がすべて表示されます。 例えば、次の部分のコメントを外せば、これまで rev に関して証明した定理が表示されます。

続く練習問題に取り組む際や読み進める際には、常に Search コマンドのことを頭の隅に置いておくといいでしょう。 そうすることでずいぶん時間の節約ができるはずです。 もし ProofGeneral を使っているのなら、 C-c C-a C-a とキー入力をすることで Search コマンドを使うことができます。 その結果をエディタに貼り付けるには C-c C-; を使うことができます。

リストについての練習問題 (1)

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

リストについてさらに練習しましょう。

次の問題には簡単な解法があります。 こんがらがってしまったようであれば、少し戻って単純な方法を探してみましょう。

前に書いた nonzeros 関数に関する練習問題です。

☐

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

次のeqblistは数のリストの等しさを計算するものです。 定義を埋めなさい。 また、どんなリストlに対してもeqblist l lがtrueを返すことを示しなさい。

☐

リストについての練習問題 (2)

上で見たバッグについて、いくつかの定理を証明します。

練習問題: ★, standard (count_member_nonzero)

☐

以下の leb に関する補題は、この次の課題に使えるかもしれません。

次の練習問題を解く前に、remove_one の定義ができあがっていることを確認してください。

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

☐

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

バッグについて count と sum を使った定理 bag_count_sum を考え、それをCoqを使って証明しなさい。 （countの定義によって証明の難易度が変わるかもしれません。）

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

rev 関数が単射である、すなわち
    forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2

であることを証明しなさい。 （この練習問題には簡単な解法と難しい解法があります。）

☐

オプション

リストからn番目を取り出す関数を定義するとします。 もし関数の型をnat -> natlist -> natにすると、リストが短すぎる（つまりnilだけの場合）何かの数値を選ばなければなりません。

この方法はあまり良くありません。 もしnth_badが42を返したとしても、別の処理なしにはそれが実際にリストにあった値なのかを判断できません。 より良い方法としては、nth_badの返し値の型を変更して、エラー値を扱えるようにするというものです。 この型をnatoptionと呼ぶことにします。

We can then change the above definition of nth_bad to return None when the list is too short and Some a when the list has enough members and a appears at position n. We call this new function nth_error to indicate that it may result in an error.

（HTML版では上の例での証明部分の常套句が消えています。 もし見たければ直後の四角をクリックしてください。） この機会に、 Coq のプログラミング言語としての機能として、条件式を紹介しておきましょう。

Coq の条件式（if式）は他の言語に見られるものとほとんど同じですが、少しだけ一般化されています。 Coq には 組み込みのブーリアン型がないため、 Coq の条件式では、実際には、構成子のふたつある任意の帰納型に対する分岐ができます。 条件部の式が Inductive の定義の最初の構成子に評価された場合には真、ふたつめの構成子に評価された場合には偽と見做されます。

次の関数は、 natoption 型から nat の値を取り出し、 None の場合には与えられたデフォルト値を返します。

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

同じ考え方で、以前定義した hd 関数を修正し、 nil の場合に返す値を渡さなくて済むようにしなさい。

☐

Exercise: 1 star, standard, optional (option_elim_hd)

This exercise relates your new hd_error to the old hd.

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

新しい hd_error と古い hd の関係についての練習問題です。

☐

Partial Maps

As a final illustration of how data structures can be defined in Coq, here is a simple partial map data type, analogous to the map or dictionary data structures found in most programming languages. First, we define a new inductive datatype id to serve as the "keys" of our partial maps.

Internally, an id is just a number. Introducing a separate type by wrapping each nat with the tag Id makes definitions more readable and gives us the flexibility to change representations later if we wish. We'll also need an equality test for ids:

Exercise: 1 star, standard (eqb_id_refl)

☐ Now we define the type of partial maps:

この宣言は次のように読めます。 「partial_map を構成する方法はふたつある。 構成子 empty で空の部分写像を表現するか、構成子 record をキーと値と既存の partial_map に適用してキーと値の対応を追加した partial_map を構成するかのいずれかである。」 The update function overrides the entry for a given key in a partial map by shadowing it with a new one (or simply adds a new entry if the given key is not already present).

最後に、 find 関数は、 partial_map から与えられたキーに対応する値を探し出すものです。 キーが見つからなかった場合には None を返し、キーが val に結び付けられていた場合には Some val を返します。 同じキーが複数の値に結び付けられている場合には、最初に見つけた値を返します。

Exercise: 1 star, standard (update_eq)

☐

Exercise: 1 star, standard (update_neq)

☐

Exercise: 2 stars, standard (baz_num_elts)

Consider the following inductive definition:

How many elements does the type baz have? (Explain in words, in a comment.)

☐