Poly_J:多相性と高階関数

Require Export Lists_J.

ポリモルフィズム（多相性）

多相的なリスト

ここまでは、数値のリストについて学んできました。もちろん、数値以外の、文字列、ブール値、リストといったものを要素として持つリストを扱えるプログラムは、より興味深いものとなるでしょう。これまで学んできたことだけでも、実は新しい帰納的なデータ型を作ることはできるのです。例えば次のように...

Inductive boollist : Type :=
  | bool_nil : boollist
  | bool_cons : bool -> boollist -> boollist.

... しかし、こんなことをやっていると、すぐに嫌になってしまうでしょう。その理由の一つは、データ型ごとに違ったコンストラクタの名前をつけなければならないことですが、もっと大変なのは、こういったリストを扱う関数（length、revなど）を、新しく対応した型ごとに作る必要が出てくることです。

この無駄な繰り返し作業を無くすため、Coqは多相的な帰納的データ型の定義をサポートしています。これを使うと、多相的なリストは以下のように書くことができます。

Inductive list (X:Type) : Type :=
  | nil : list X
  | cons : X -> list X -> list X.

これは、前の章にあるnatlistの定義とほとんどそっくりですが、コンストラクタconsの引数の型がnatであったのに対し、任意の型を表すXがそれに変わっています。このXはヘッダに加えられたXと結びつけられ、さらにnatlistであったものがlist Xに置き換わっています（ここで、コンストラクタにnilやconsといった名前を付けられるのは、最初に定義したnatlistがModuleの中で定義されていて、ここからはスコープの外になっているからです）。

それでは、listとはいったい何なのか、ということを正確に考えて見ましょう。これを考える一つの手がかりは、リストが「型を引数にとり、帰納的な定義を返す関数である」と考えることです。あるいは「型を引数にとり、型を返す関数」と考えてもいいかもしれません。任意の型Xについて、list Xという型は、帰納的に定義されたリストの集合で、その要素の型がXとなっているものと考えることもできます。

この定義の下で、コンストラクタnilやconsを使う際には、今作ろうとしているリストの要素の型を指定してやる必要があります。なぜなら、今やnilもconsも多相的なコンストラクタとなっているからです。

Check nil.

Check cons.

ここで出てきた”forall X“というのは、コンストラクタに追加された引数で、後に続く引数で型を特定させるものです。nilやconsが使われる際、例えば2と1を要素に持つリストは、以下のように表されます。

Check (cons nat 2 (cons nat 1 (nil nat))).

（ここではnilやconsを明示的に記述していますが、それは我々がまだ[]や::の表記法（Notation）をまだ記述していないからです。この後でやります）

それでは少し話を戻して、以前書いたリスト処理関数を多相版に作り直していきましょう。length関数は以下のようになります。

Fixpoint length (X:Type) (l:list X) : nat :=
  match l with
  | nil      => 0
  | cons h t => S (length X t)
  end.

ここで、matchに使われているnilやconsに型修飾がついていないことに注意してください。我々はすでにリストlが型Xの要素を持っていることを知っていますが、それはパターンマッチにXを含める理由になりません。さらに形式的には、Xはリスト定義全体での型であって、個々のコンストラクタの型ではないのです。

nilやconsと同様に、lengthも与えるリストと同じ型を最初に適用すれば使えます。

Example test_length1 :
    length nat (cons nat 1 (cons nat 2 (nil nat))) = 2.
Proof. reflexivity.  Qed.

このlengthを別の型のリストに使いたい場合は、適切な型を与えるだけで済みます。

Example test_length2 :
    length bool (cons bool true (nil bool)) = 1.
Proof. reflexivity.  Qed.

では、このサブセクションの終わりに、他の標準的なリスト処理関数を多相的に書き直しましょう。

Fixpoint app (X : Type) (l1 l2 : list X)
                : (list X) :=
  match l1 with
  | nil      => l2
  | cons h t => cons X h (app X t l2)
  end.

Fixpoint snoc (X:Type) (l:list X) (v:X) : (list X) :=
  match l with
  | nil      => cons X v (nil X)
  | cons h t => cons X h (snoc X t v)
  end.

Fixpoint rev (X:Type) (l:list X) : list X :=
  match l with
  | nil      => nil X
  | cons h t => snoc X (rev X t) h
  end.

Example test_rev1 :
    rev nat (cons nat 1 (cons nat 2 (nil nat)))
  = (cons nat 2 (cons nat 1 (nil nat))).
Proof. reflexivity.  Qed.

Example test_rev2:
  rev bool (nil bool) = nil bool.
Proof. reflexivity.  Qed.

型推論

それでは、app関数の定義をもう一度書いてみましょう。ただし今回は、引数の型を指定しないでおきます。Coqはこれを受け入れてくれるでしょうか？

Fixpoint app' X l1 l2 : list X :=
  match l1 with
  | nil      => l2
  | cons h t => cons X h (app' X t l2)
  end.

うまくいったようです。Coqがapp'にどのような型を設定したのか確認してみましょう。

Check app'.
Check app.

両者は全く同じ型であることが分かります。Coqは型推論という機構を持っていて、これを使い、Xとl1とl2の型が何であるべきかを、その使われ方から導き出します。例えば、Xがconsの引数として使われたことがあれば、それは型に違いなく、さらにconsの最初に引数で型が指定されていて、l1がnilやconsとマッチされているなら、それはlistに違いなかろう、といった具合です。

このパワフルな機構の存在は、型情報を常にそこら中に書かなければならないわけではない、ということを意味します。とはいえ、型を明示的に書くことは、ドキュメント作成やプログラムの健全性をチェックする際に大いに意味はあるのですが。とにかく、これからは自分の書くコードで、型指定を書くところ、書かないところのバランスを考えていく必要があります（多すぎれば、コードが目障りな型指定で読みにくくなりますし、少なすぎると、プログラムを読む人に型推論の結果をいちいち推測させなければならなくなります）。

引数の同化（Synthesis）

多相的な関数を使うときはいつも、通常の引数に加えて型を一つ以上渡さなければなりません。例えば、length関数で自分を再帰している部分には、型Xとして渡されたものをそのまま渡すことになります。しかしこのように、そこらじゅうに明示的に型を書かなければならないとなると、これはとても面倒で冗長な作業です。lengthの二つ目の引数がX型のリストなら、最初の引数はX以外になり得ないのは明らかなのではないか・・・・ならなぜわざわざそれを書く必要があるのでしょう。

幸いなことに、Coqではこの種の冗長性を避けることができます。型を引数に渡すところではどこでも同化した引数”_“を書くことができるのです。これは「ここをあるべき型に解釈してください」という意味です。もう少し正確に言うと、Coqが_を見つけると、手近に集められる情報を集めます。それは、適用されている関数の型や、その適用が現れている文脈から予想される型などですが、それを使って_と置き換えるべき具体的な型を決定するのです。

これを聞くと、型推論と同じじゃないかと思われるかもしれません。実際、この二つの機能は水面下にあるメカニズムではつながっています。次のように単に引数の型を省略する代わりに

app' X l1 l2 : list X :=

このように、型を_で書くことができるということです。

app' (X : _) (l1 l2 : _) : list X :=

いずれも、Coqに、欠落している情報を推論させるもので、これを引数の同化といいます。

引数の同化を使うと、length関数は以下のように書けます。

Fixpoint length' (X:Type) (l:list X) : nat :=
  match l with
  | nil      => 0
  | cons h t => S (length' _ t)
  end.

この例では、Xを_に省略することをあまりしていません。しかし多くの場合、この違いは重要です。例えば、1,2,3といった数値を保持するリストを書きたい場合、以下のように書く代わりに...

Definition list123 :=
  cons nat 1 (cons nat 2 (cons nat 3 (nil nat))).

...引数同化を使って以下のように書くこともできます。

Definition list123' := cons _ 1 (cons _ 2 (cons _ 3 (nil _))).

暗黙の引数

さらに先に進みましょう。プログラム全体が_まみれになることを避けるため、特定の関数の引数については常に型推論するよう指定できます。

Implicit Arguments nil [[X]].
Implicit Arguments cons [[X]].
Implicit Arguments length [[X]].
Implicit Arguments app [[X]].
Implicit Arguments rev [[X]].
Implicit Arguments snoc [[X]].


Definition list123'' := cons 1 (cons 2 (cons 3 nil)).
Check (length list123'').

また、関数定義の中で、引数を暗黙のものにすることもできます。その際は、次のように引数を中カッコで囲みます。

Fixpoint length'' {X:Type} (l:list X) : nat :=
  match l with
  | nil      => 0
  | cons h t => S (length'' t)
  end.

（ここで注意してほしいのは、再帰呼び出しのlength''ではもうすでに型を引数で指定していない、ということです）これからは、この書き方をできるだけ使っていくことにします。ただし、Inductive宣言のコンストラクタではImplicit Argumentsを明示的に書くようにします。

引数を暗黙的に宣言することには、小さな問題が一つあります。時折、Coqが型を特定するために必要な情報を十分に集められない時があるのです。そういう場合には、その時だけ明示してやります。たとえそれがグローバルにはImplicitと宣言されていたとしてもです。例えば、もし次のように書きたかったとします。

この定義のコメントをはずすと、Coqはエラーを出します。nilが何の型のnilなのか分からないからです。このようなときは、型宣言を明示的に行うことができます（これによってnilを何に適用できるか、という情報が与えられます）。

Definition mynil : list nat := nil.

それとは別に、関数名の前に@を付けることで暗黙的に宣言された関数に対して型を明示的に与えることができます。

Check @nil.

Definition mynil' := @nil nat.

引数同化と暗黙的な引数をつかうことで、リストのノーテーション（表記法）をより便利に記述できます。コンストラクタの型引数を暗黙的に記述すれば、Coqはその表記法を使ったときに型を自動的に推論してくれます。

Notation "x :: y" := (cons x y)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x , .. , y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y)
                     (at level 60, right associativity).

これで、我々の望む書き方ができるようになりました。

Definition list123''' := [1, 2, 3].

練習問題:多相的なリスト

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

ここにあるいくつかの練習問題は、List_J.vにあったものと同じですが、多相性の練習になります。以下の定義を行い、証明を完成させなさい。

Fixpoint repeat (X : Type) (n : X) (count : nat) : list X :=
  (* FILL IN HERE *) admit.

Example test_repeat1:
  repeat bool true 2 = cons true (cons true nil).
 (* FILL IN HERE *) Admitted.

Theorem nil_app : forall X:Type, forall l:list X,
  app [] l = l.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem rev_snoc : forall X : Type,
                     forall v : X,
                     forall s : list X,
  rev (snoc s v) = v :: (rev s).
Proof.
  (* FILL IN HERE *) Admitted.

Theorem snoc_with_append : forall X : Type,
                         forall l1 l2 : list X,
                         forall v : X,
  snoc (l1 ++ l2) v = l1 ++ (snoc l2 v).
Proof.
  (* FILL IN HERE *) Admitted.

☐

多相的なペア

次も同様に、前の章で作った数値のペアを多相的にすることを考えます。

Inductive prod (X Y : Type) : Type :=
  pair : X -> Y -> prod X Y.

Implicit Arguments pair [[X] [Y]].

リストと同様、型引数を暗黙にし、その表記法を定義します。

Notation "( x , y )" := (pair x y).

また、「ペア型」の、より標準的な表記法も登録しておきます。

Notation "X * Y" := (prod X Y) : type_scope.

（type_scopeというアノテーションは、この省略形が、型を解析する際に使われるものであることを示しています。これによって、*が乗算の演算子と衝突することを避けています。

注意：最初のうちは、(x,y)とX*Yの違いに混乱するかもしれません。覚えてほしいのは、(x,y)が値のペアを構成するもので、X*Yは型のペアを構成するものだということです。値xがX型で、値yがY型なら、値(x,y)はX*Y型となります。

ペアの最初の要素、２番目の要素を返す射影関数は他のプログラミング言語で書いたものと比べると若干長くなります。

Definition fst {X Y : Type} (p : X * Y) : X :=
  match p with (x,y) => x end.

Definition snd {X Y : Type} (p : X * Y) : Y :=
  match p with (x,y) => y end.

次の関数は二つのリストを引数にとり、一つの”ペアのリスト”を作成します。多くの関数型言語でzip関数と呼ばれているものです。Coqの標準ライブラリとぶつからないよう、ここではcombineと呼ぶことにします。

ペアの表記法は、式だけではなくパターンマッチにも使えることに注目してください。

Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y)
           : list (X*Y) :=
  match (lx,ly) with
  | ([],_) => []
  | (_,[]) => []
  | (x::tx, y::ty) => (x,y) :: (combine tx ty)
  end.

また、あいまいさがない場合は、matchを囲む括弧を取る事もできます。

Fixpoint combine' {X Y : Type} (lx : list X) (ly : list Y)
           : list (X*Y) :=
  match lx,ly with
  | [],_ => []
  | _,[] => []
  | x::tx, y::ty => (x,y) :: (combine' tx ty)
  end.

次の質問の答えを紙に書いた後で、Coqの出した答えと同じかチェックしなさい。

• 関数combineの型は何でしょう (Check @combineの出力結果は？

• それでは

  Eval simpl in (combine [1,2] [false,false,true,true]).
  

は何を出力する？☐

split関数はcombineと全く逆で、ペアのリストを引数に受け取り、リストのペアを返します。多くの関数型言語とでunzipと呼ばれているものです。次の段落のコメントをはずし、split関数の定義を完成させなさい。続くテストを通過することも確認しなさい。

Example test_split:
  split [(1,false),(2,false)] = ([1,2],[false,false]).
Proof. reflexivity.  Qed.
*)

☐

多相的なオプション

最後に、多相的なオプションに取り組みます。この型は、前の章のnatoptionを多相化して定義することにします。

Inductive option (X:Type) : Type :=
  | Some : X -> option X
  | None : option X.

Implicit Arguments Some [[X]].
Implicit Arguments None [[X]].

また、index関数も、色々な型のリストで使えるように定義し直しましょう。

Fixpoint index {X : Type} (n : nat)
               (l : list X) : option X :=
  match l with
  | [] => None
  | a :: l' => if beq_nat n O then Some a else index (pred n) l'
  end.

Example test_index1 :    index 0 [4,5,6,7]  = Some 4.
Proof. reflexivity.  Qed.
Example test_index2 :    index  1 [[1],[2]]  = Some [2].
Proof. reflexivity.  Qed.
Example test_index3 :    index  2 [true]  = None.
Proof. reflexivity.  Qed.

前の章に出てきたhd_opt関数の多相版を定義しなさい。。次の単体テストでの確認も忘れずに。

Definition hd_opt {X : Type} (l : list X)  : option X :=
  (* FILL IN HERE *) admit.

再び、暗黙的に定義された引数を明示的に指定してみましょう。関数名の前に@をつければいいのでしたね。

Check @hd_opt.

Example test_hd_opt1 :  hd_opt [1,2] = Some 1.
 (* FILL IN HERE *) Admitted.
Example test_hd_opt2 :   hd_opt  [[1],[2]]  = Some [1].
 (* FILL IN HERE *) Admitted.

☐

データとしての関数

高階関数

他の多くの近代的なプログラミング言語（全ての関数型言語を含む）同様、Coqは関数をファーストクラスに属するものとして取り扱います。つまりそれは、関数を他の関数の引数として渡したり、結果として関数を返したり、データ構造の中に関数を含めたりすることができるということです。

関数を操作する関数を、一般に「高階関数」と呼びます。例えば次のようなものです。

Definition doit3times {X:Type} (f:X->X) (n:X) : X :=
  f (f (f n)).

ここで引数fは関数です。doit3timesの内容は、値nに対して関数fを3回適用するものです。

Check @doit3times.


Example test_doit3times: doit3times minustwo 9 = 3.
Proof. reflexivity.  Qed.

Example test_doit3times': doit3times negb true = false.
Proof. reflexivity.  Qed.

部分適用

実は、我々がすでに見た、複数の引数を持つ関数は、関数を引数に渡すサンプルになっているのです。どういうことかは、plus関数の型を思い出せば分かります。それはnat -> nat -> natでした。

Check plus.

->は、型同士の二項演算子ですが、このことはCoqが基本的に引数一つの関数しかサポートしていないことを意味します。さらに、この演算子は右結合であるため、plus関数の型はnat -> (nat -> nat)の省略であると言えます。これをよく読むと”plusはnat型の引数を一つ取り、引数がnat型一つでnat型を返す関数を返す”と読むことができます。以前の例ではplusに二つの引数を一緒に与えていましたが、もし望むなら最初の一つだけを与えることもできます。これを部分適用といいます。

Definition plus3 := plus 3.
Check plus3.

Example test_plus3 :    plus3 4 = 7.
Proof. reflexivity.  Qed.
Example test_plus3' :   doit3times plus3 0 = 9.
Proof. reflexivity.  Qed.
Example test_plus3'' :  doit3times (plus 3) 0 = 9.
Proof. reflexivity.  Qed.

余談： カリー化

Coqでは、f : A -> B -> Cという型の関数はA -> (B -> C)型と同じです。このことは、もし上の関数fに値Aを与えると、f' : B -> Cという型の関数が戻り値として返ってくるということです。これは部分適用のplus3でやりましたが、このように、複数の引数から戻り値の型のリストを、関数を返す関数として捉えなおすことを、論理学者ハスケル・カリーにちなんでカリー化、と呼んでいます。

逆に、A -> B -> C型の関数を(A * B) -> C型の関数に変換することもできます。これをアンカリー化（非カリー化）といいます。アンカリー化された二項演算は、二つの引数を同時にペアの形で与える必要があり、部分適用はできません。

カリー化は以下のように定義できます。

Definition prod_curry {X Y Z : Type}
  (f : X * Y -> Z) (x : X) (y : Y) : Z := f (x, y).

練習問題として、その逆のprod_uncurryを定義し、二つの関数が互いに逆関数であることを証明しなさい。

Definition prod_uncurry {X Y Z : Type}
  (f : X -> Y -> Z) (p : X * Y) : Z :=
  (* FILL IN HERE *) admit.

(考える練習: 次のコマンドを実行する前に、prod_curryとprod_uncurryの型を考えなさい。)

Check @prod_curry.
Check @prod_uncurry.

Theorem uncurry_curry : forall (X Y Z : Type) (f : X -> Y -> Z) x y,
  prod_curry (prod_uncurry f) x y = f x y.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem curry_uncurry : forall (X Y Z : Type)
                               (f : (X * Y) -> Z) (p : X * Y),
  prod_uncurry (prod_curry f) p = f p.
Proof.
  (* FILL IN HERE *) Admitted.

☐

フィルター (Filter)関数

次に紹介するのは、とても有用な高階関数です。これは、X型のリストと、Xについての述語（Xを引数にとり、boolを返す関数）を引数にとり、リストの要素にフィルターをかけて、述語として与えられた関数の結果がtrueとなった要素だけのリストを返す関数です。

Fixpoint filter {X:Type} (test: X->bool) (l:list X)
                : (list X) :=
  match l with
  | []     => []
  | h :: t => if test h then h :: (filter test t)
                        else       filter test t
  end.

例えば、このfilter関数に述語としてevenbと数値のリストlを与えると、リストlの要素の中で偶数の要素だけがリストとなって帰ります。

Example test_filter1: filter evenb [1,2,3,4] = [2,4].
Proof. reflexivity.  Qed.

Definition length_is_1 {X : Type} (l : list X) : bool :=
  beq_nat (length l) 1.

Example test_filter2:
    filter length_is_1
           [ [1, 2], [3], [4], [5,6,7], [], [8] ]
  = [ [3], [4], [8] ].
Proof. reflexivity.  Qed.

このfilterを使うことで、Lists.vにあるcountoddmembers関数をもっと簡潔に書くことができます。

Definition countoddmembers' (l:list nat) : nat :=
  length (filter oddb l).

Example test_countoddmembers'1:   countoddmembers' [1,0,3,1,4,5] = 4.
Proof. reflexivity.  Qed.
Example test_countoddmembers'2:   countoddmembers' [0,2,4] = 0.
Proof. reflexivity.  Qed.
Example test_countoddmembers'3:   countoddmembers' nil = 0.
Proof. reflexivity.  Qed.

無名（匿名）関数

filter関数に渡すためだけに、二度と使われないlength_is_1といった関数を定義して、それにわざわざ名前を付けるというのは、少しわずらわしく感じます。このようなことは、この例だけの問題ではありません。高階関数を使うときは、引数として”一度しか使わない関数”を渡すことがよくあります。こういう関数にいちいち名前を考えるのは、退屈以外の何物でもありません。

幸いなことに、いい方法があります。一時的な関数を、名前を付けることも、トップレベルで宣言することもなく作成することができるのです。これは定数のリストや、数値定数と同じようなものだと考えられます。

Example test_anon_fun':
  doit3times (fun n => n * n) 2 = 256.
Proof. reflexivity.  Qed.

次は無名関数を使った書き換えのもう少しいい例です。

Example test_filter2':
    filter (fun l => beq_nat (length l) 1)
           [ [1, 2], [3], [4], [5,6,7], [], [8] ]
  = [ [3], [4], [8] ].
Proof. reflexivity.  Qed.

filter関数を使い、数値のリストを入力すると、そのうち偶数でなおかつ7より大きい要素だけを取り出すfilter_even_gt7関数を書きなさい。

Definition filter_even_gt7 (l : list nat) : list nat :=
  (* FILL IN HERE *) admit.

Example test_filter_even_gt7_1 :
  filter_even_gt7 [1,2,6,9,10,3,12,8] = [10,12,8].
 (* FILL IN HERE *) Admitted.

Example test_filter_even_gt7_2 :
  filter_even_gt7 [5,2,6,19,129] = [].
 (* FILL IN HERE *) Admitted.

☐

filter関数を使って、partition関数を書きなさい。:

partition : forall X : Type,
            (X -> bool) -> list X -> list X * list X

型Xについて、X型の値がある条件を満たすかを調べる述語X -> boolとXのリストlist Xを引数に与えると、partition関数はリストのペアを返します。ペアの最初の要素は、与えられたリストのうち、条件を満たす要素だけのリストで、二番目の要素は、条件を満たさないもののリストです。二つのリストの要素の順番は、元のリストの順と同じでなければなりません。

Definition partition {X : Type} (test : X -> bool) (l : list X)
                     : list X * list X :=
(* FILL IN HERE *) admit.

Example test_partition1: partition oddb [1,2,3,4,5] = ([1,3,5], [2,4]).
(* FILL IN HERE *) Admitted.
Example test_partition2: partition (fun x => false) [5,9,0] = ([], [5,9,0]).
(* FILL IN HERE *) Admitted.

☐

マップ（Map）関数

もう一つ、便利な高階関数としてmapを挙げます。

Fixpoint map {X Y:Type} (f:X->Y) (l:list X)
             : (list Y) :=
  match l with
  | []     => []
  | h :: t => (f h) :: (map f t)
  end.

これは、関数fとリストl = [n1, n2, n3, ...]を引数にとり、関数fをlの各要素に適用した[f n1, f n2, f n3,...]というリストを返します。例えばこのようなものです。

Example test_map1: map (plus 3) [2,0,2] = [5,3,5].
Proof. reflexivity.  Qed.

入力されるリストの要素の型と、出力されるリストの要素の型は同じである必要はありません（mapは、XとY二種類の型変数を取ります）。次の例は、数値のリストと、数値を受け取りbool値を返す関数から、bool型のリストを返します。

Example test_map2: map oddb [2,1,2,5] = [false,true,false,true].
Proof. reflexivity.  Qed.

同じ関数が、数値のリストと、「数値からbool型のリストへの関数」を引数にとり、「bool型のリストのリスト」を返すような関数にも使えます。

Example test_map3:
    map (fun n => [evenb n,oddb n]) [2,1,2,5]
  = [[true,false],[false,true],[true,false],[false,true]].
Proof. reflexivity.  Qed.

mapとrevが可換であることを示しなさい。証明には補題をたてて証明する必要があるでしょう。

Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
  map f (rev l) = rev (map f l).
Proof.
  (* FILL IN HERE *) Admitted.

☐

map関数は、list Xからlist Yへのマップを、型X -> Yの関数を使って実現しています。同じような関数flat_mapを定義しましょう。これはlist Xからlist Yへのマップですが、X -> list Yとなる関数fを使用できます。このため、次のように要素ごとの関数fの結果を平坦化してやる必要があります。

        flat_map (fun n => [n,n+1,n+2]) [1,5,10]
      = [1, 2, 3, 5, 6, 7, 10, 11, 12].

Fixpoint flat_map {X Y:Type} (f:X -> list Y) (l:list X)
                   : (list Y) :=
  (* FILL IN HERE *) admit.

Example test_flat_map1:
  flat_map (fun n => [n,n,n]) [1,5,4]
  = [1, 1, 1, 5, 5, 5, 4, 4, 4].
 (* FILL IN HERE *) Admitted.

☐

リストは、map関数のような関数に渡すことができる、帰納的に定義された唯一の型、というわけではありません。次の定義は、option型のためにmap関数を定義したものです。

Definition option_map {X Y : Type} (f : X -> Y) (xo : option X)
                      : option Y :=
  match xo with
    | None => None
    | Some x => Some (f x)
  end.

filterやmap関数を定義したり使ったりするケースでは、多くの場合暗黙的な型引数が使われます。暗黙の型引数定義に使われている中括弧を普通の括弧に置き換え、必要なところに型引数を明示的に書くようにして、それが正しいかどうかをCoqでチェックしなさい。☐

畳み込み（Fold）関数

さらにパワフルな高階関数foldに話を移します。この関数はGoogleの分散フレームワーク”map/reduce”でいうところの”reduce”オペレーションに根ざしています。

Fixpoint fold {X Y:Type} (f: X->Y->Y) (l:list X) (b:Y) : Y :=
  match l with
  | nil => b
  | h :: t => f h (fold f t b)
  end.

直感的にfoldは、与えられたリストの各要素の間に、与えられた二項演算子fを挟み込むように挿入していくような操作です。 例えば、fold plus [1,2,3,4]は、直感的に1+2+3+4と同じ意味です。ただし正確には、二番めの引数に、fに最初に与える”初期値”が必要になります。例えば

fold plus [1,2,3,4] 0

は、次のように解釈されます。

1 + (2 + (3 + (4 + 0))).

もう少しサンプルを見てください。

Check (fold plus).
Eval simpl in (fold plus [1,2,3,4] 0).

Example fold_example1 : fold mult [1,2,3,4] 1 = 24.
Proof. reflexivity. Qed.

Example fold_example2 : fold andb [true,true,false,true] true = false.
Proof. reflexivity. Qed.

Example fold_example3 : fold app  [[1],[],[2,3],[4]] [] = [1,2,3,4].
Proof. reflexivity. Qed.

fold関数がXとY二つの型引数をとっていて、関数fが型Xを引数にとり型Yを返すようになっていることに注目してください。XとYが別々の型となっていることで、どのような場合に便利であるかを考えてください。

関数を作成する関数

これまで見てきた高階関数は、ほとんどが関数を引数にとるものでした。ここでは、関数が別の関数の戻り値になるような例を見ていきましょう。

まず、値x（型X）を引数としてとり、「nat型の引数からX型の戻り値を返す関数」を返す関数を考えます。戻る関数は、引数に関係なく、生成時に与えられた値｢x｣を常に返すものです。

Definition constfun {X: Type} (x: X) : nat->X :=
  fun (k:nat) => x.

Definition ftrue := constfun true.

Example constfun_example1 : ftrue 0 = true.
Proof. reflexivity. Qed.

Example constfun_example2 : (constfun 5) 99 = 5.
Proof. reflexivity. Qed.

もう少し面白い例を挙げます。次の関数は、数値から型Xを戻す関数fと、数値k、型Xの値xを引数にとり、fにkと同じ引数が与えられた場合だけ値xを返し、それ以外のときはfにkを渡した戻り値を返します。

Definition override {X: Type} (f: nat->X) (k:nat) (x:X) : nat->X:=
  fun (k':nat) => if beq_nat k k' then x else f k'.

たとえば、このoverride関数を数値からbool型への関数に以下のように２回適用すると、値が1と3のときだけfalseを返し、それ以外はtrueを返すようにすることができます。

Definition fmostlytrue := override (override ftrue 1 false) 3 false.

Example override_example1 : fmostlytrue 0 = true.
Proof. reflexivity. Qed.

Example override_example2 : fmostlytrue 1 = false.
Proof. reflexivity. Qed.

Example override_example3 : fmostlytrue 2 = true.
Proof. reflexivity. Qed.

Example override_example4 : fmostlytrue 3 = false.
Proof. reflexivity. Qed.

次の証明にとりかかる前に、あなたがこの証明の意味することを理解しているか確認するため、証明内容を別の言葉で言い換えてください。証明自体は単純なものです。

Theorem override_example : forall (b:bool),
  (override (constfun b) 3 true) 2 = b.
Proof.
  (* FILL IN HERE *) Admitted.

☐

このコースでこれ以降、関数のオーバーライド（上書き）がよく登場しますが、この性質について多くを知る必要はありません。しかし、これらの性質を証明するには、さらにいくつかのCoqのタクティックを知らなければなりません。それが、この章の残りの部分の主なトピックになります。

さらにCoqについて

unfoldタクティック

時折、Coqが関数を自動的に展開してくれないために証明が行き詰まってしまうことがあります（これは仕様であって、バグではありません。Coqがもし可能な展開を全て自動でやってしまったら、証明のゴールはたちまち巨大化して、読むこともCoqで操作することもできなくなってしまいます）。

Theorem unfold_example_bad : forall m n,
  3 + n = m ->
  plus3 n + 1 = m + 1.
Proof.
  intros m n H.

  Admitted.

unfoldタクティックは、定義された名前を、その定義の右側の記述に置き換えてくれるものです。

Theorem unfold_example : forall m n,
  3 + n = m ->
  plus3 n + 1 = m + 1.
Proof.
  intros m n H.
  unfold plus3.
  rewrite -> H.
  reflexivity.  Qed.

今我々は、overrideの最初の性質を証明することができるようになりました。もしある関数の引数のある値kをオーバーライドしてから引数kを与えると、オーバーライドされた値が帰る、というものです。

Theorem override_eq : forall {X:Type} x k (f:nat->X),
  (override f k x) k = x.
Proof.
  intros X x k f.
  unfold override.
  rewrite <- beq_nat_refl.
  reflexivity.  Qed.

この証明はストレートなものですが、override関数の展開にunfoldを必要としている点だけ注意してください。

Theorem override_neq : forall {X:Type} x1 x2 k1 k2 (f : nat->X),
  f k1 = x1 ->
  beq_nat k2 k1 = false ->
  (override f k2 x2) k1 = x1.
Proof.
  (* FILL IN HERE *) Admitted.

☐

unfoldの逆の機能として、Coqにはfoldというタクティックも用意されています。これは、展開された定義を元に戻してくれますが、あまり使われることはありません。

反転（Inversion）

自然数の定義を思い出してください。

Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

この定義から、全ての数は二つの形式、コンストラクタOで作られたか、コンストラクタSに他の数値を与えて作られたかのどちらかであることは明白です。しかし両目を見開いてよく見ると、この定義（と、他のプログラミング言語で、データ型の定義がどのように働くか、という非形式的な理解）から、二つの暗黙的な事実が見つかります。

• コンストラクタSが単射であること。つまり、S n = S mとなるためのただ一つの方法はn = mであること。
• コンストラクタOとコンストラクタSは、互いに素であること。つまり、OはどんなnについてもS nと等しくないということ。

同じ原理が、全ての帰納的に定義された型にあてはまります。全てのコンストラクタは単射で、コンストラクタが違えば同じ値は生まれません。リストについて言えばconsコンストラクタは単射で、nilは全ての空でないリストと異なっています。bool型では、trueとfalseは異なるものです（ただ、trueもfalseも引数を取らないため、単射かどうか、という議論には意味がありません）。

Coqには、この性質を証明に利用するinversionというタクティックが用意されています。

inversionタクティックは、次のような場合に使います。コンテキストに以下のような形の仮定H（や過去に定義された補助定理）がある場合、

c a1 a2 ... an = d b1 b2 ... bm

これは、あるコンストラクタcとdに、ある引数a1 ... anとb1 ... bmを与えて評価したものが等しいことを示していますが、このような時、inversion Hとすることで、この等式を”反転”し、そこに含まれている情報を以下のようなやり方で引き出します。

• もしcとdが同じコンストラクタの場合、すでに分かっているように、コンストラクタの単射性から、a1 = b1,a2 = b2をが導かれます。 また、inversion Hはこの事実をコンテキストに追加し、ゴールの置き換えに使えないかを試します。
• もしcとdが違うコンストラクタの場合、仮定Hは矛盾していることになります。つまり、偽である前提がコンテキストに紛れ込んでいるということになり、これはどんなゴールも証明できてしまうことを意味します。このような場合、inversion Hは現在のゴールが解決されたものとして、ゴールの一覧から取り除きます。

inversionタクティックは、このような一般的な説明を読むより、その動きを実際に見てもらったほうが簡単に理解できるでしょう。以下はinversionの使い方を見てもらい、理解するための練習を兼ねた定理の例です。

Theorem eq_add_S : forall (n m : nat),
     S n = S m ->
     n = m.
Proof.
  intros n m eq. inversion eq. reflexivity.  Qed.

Theorem silly4 : forall (n m : nat),
     [n] = [m] ->
     n = m.
Proof.
  intros n o eq. inversion eq. reflexivity.  Qed.

便利なように、inversionタクティックは、等式でつながった複合値を展開して、それぞれを対応する相手に結び付けてくれます。

Theorem silly5 : forall (n m o : nat),
     [n,m] = [o,o] ->
     [n] = [m].
Proof.
  intros n m o eq. inversion eq. reflexivity. Qed.

Example sillyex1 : forall (X : Type) (x y z : X) (l j : list X),
     x :: y :: l = z :: j ->
     y :: l = x :: j ->
     x = y.
Proof.
  (* FILL IN HERE *) Admitted.

☐

Theorem silly6 : forall (n : nat),
     S n = O ->
     2 + 2 = 5.
Proof.
  intros n contra. inversion contra. Qed.

Theorem silly7 : forall (n m : nat),
     false = true ->
     [n] = [m].
Proof.
  intros n m contra. inversion contra.  Qed.

Example sillyex2 : forall (X : Type) (x y z : X) (l j : list X),
     x :: y :: l = [] ->
     y :: l = z :: j ->
     x = z.
Proof.
  (* FILL IN HERE *) Admitted.

☐

コンストラクタの単射性が、forall (n m : nat), S n = S m -> n = mを示している一方で、これを逆に適用することで、普通の等式の証明をすることができれば、これまで出てきたいくつかのケースにも使えるでしょう。

Lemma eq_remove_S : forall n m,
  n = m -> S n = S m.
Proof. intros n m eq. rewrite -> eq. reflexivity. Qed.

これはinversionの、もっと現実的な使い方です。ここで示された性質は、この後でもよく使うことになります。

Theorem beq_nat_eq : forall n m,
  true = beq_nat n m -> n = m.
Proof.
  intros n. induction n as [| n'].
  Case "n = 0".
    intros m. destruct m as [| m'].
    SCase "m = 0". reflexivity.
    SCase "m = S m'". simpl. intros contra. inversion contra.
  Case "n = S n'".
    intros m. destruct m as [| m'].
    SCase "m = 0". simpl. intros contra. inversion contra.
    SCase "m = S m'". simpl. intros H.
      apply eq_remove_S. apply IHn'. apply H. Qed.

beq_nat_eqの、非形式的な証明を示しなさい。

(* FILL IN HERE *)

☐

beq_nat_eqは、mについて帰納法をつかうことで証明することができました。しかし我々は、もう少し変数を導入する順序に注意を払うべきです。なぜなら、我々は一般に、十分な帰納法の仮定を得ているからです。このことを次に示します。次の証明を完成させなさい。この練習問題の効果を最大にするため、とりあえずは先にやった証明を見ないで取り組んでください。

Theorem beq_nat_eq' : forall m n,
  beq_nat n m = true -> n = m.
Proof.
  intros m. induction m as [| m'].
  (* FILL IN HERE *) Admitted.

☐

inversionのもう一つの側面を見てみましょう。以前にすでに証明済みのものですが、少し遠回りな書き方になっています。新しく追加された等号のせいで、少し等式に関する証明を追加する必要がありますし、これまでに出てきたタクティックを使う練習にもなります。

Theorem length_snoc' : forall (X : Type) (v : X)
                              (l : list X) (n : nat),
     length l = n ->
     length (snoc l v) = S n.
Proof.
  intros X v l. induction l as [| v' l'].
  Case "l = []". intros n eq. rewrite <- eq. reflexivity.
  Case "l = v' :: l'". intros n eq. simpl. destruct n as [| n'].
    SCase "n = 0". inversion eq.
    SCase "n = S n'".
      apply eq_remove_S. apply IHl'. inversion eq. reflexivity. Qed.

練習問題

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

同じところに分類され、相互に関連するような、自明でもないが複雑というほどでもない証明をいくつか練習問題としましょう。このうち、いくつかは過去のレクチャーや練習問題に出てきた補題を使用します。

Theorem beq_nat_0_l : forall n,
  true = beq_nat 0 n -> 0 = n.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem beq_nat_0_r : forall n,
  true = beq_nat n 0 -> 0 = n.
Proof.
  (* FILL IN HERE *) Admitted.

☐

Theorem double_injective : forall n m,
     double n = double m ->
     n = m.
Proof.
  intros n. induction n as [| n'].

    Case "n = 0". simpl. intros m eq. destruct m as [| m'].
      SCase "m = 0". reflexivity.
      SCase "m = S m'". inversion eq.
    Case "n = S n'". intros m eq. destruct m as [| m'].
      SCase "m = 0". inversion eq.
      SCase "m = S m'".
        apply eq_remove_S. apply IHn'. inversion eq. reflexivity. Qed.

タクティックを仮定に使用する

デフォルトでは、ほとんどのタクティックはゴールの式に作用するだけで、コンテキストの内容には手を付けません。しかしながら、ほとんどのタクティックは変数を付けることで同じ操作をコンテキストの式に行うことができます。

例えば、simpl in Hというタクティックは、コンテキストの中のHと名前のついた仮定に対して簡約をします。

Theorem S_inj : forall (n m : nat) (b : bool),
     beq_nat (S n) (S m) = b  ->
     beq_nat n m = b.
Proof.
  intros n m b H. simpl in H. apply H.  Qed.

同様に、apply L in Hというタクティックは、ある条件式L(L1 -> L2といった形の)を、コンテキストにある仮定Hに適用します。しかし普通のapplyと異なるのは、apply L in Hが、HがL1とマッチすることを調べ、それに成功したらそれをL2に書き換えることです。

言い換えると、apply L in Hは、”前向きの証明”の形をとっているといえます。それは、L1 -> L2が与えられ、仮定とL1がマッチしたら、仮定はL2と同じと考えてよい、ということです。逆に、apply Lは”逆向きの証明”であると言えます。それは、L1->L2であることが分かっていて、今証明しようとしているものがL2なら、L1を証明すればよいとすることです。

以前やった証明の変種を挙げておきます。逆向きの証明ではなく、前向きの証明を進めましょう。

Theorem silly3' : forall (n : nat),
  (beq_nat n 5 = true -> beq_nat (S (S n)) 7 = true) ->
     true = beq_nat n 5  ->
     true = beq_nat (S (S n)) 7.
Proof.
  intros n eq H.
  symmetry in H. apply eq in H. symmetry in H.
  apply H.  Qed.

前向きの証明は、与えられたもの（前提や、すでに証明された定理）からスタートして、そのゴールを次々につなげていき、ゴールに達するまでそれを続けます。逆向きの証明は、ゴールからスタートし、そのゴールが結論となる前提を調べ、それを前提や証明済みの定理にたどりつくまで繰り返します。皆さんがこれまで（数学やコンピュータサイエンスの分野で）見てきた非形式的な証明は、おそらく前向きの証明であったのではないかと思います。一般にCoqでの証明は逆向きの証明となる傾向があります。しかし、状況によっては前向きの証明のほうが簡単で考えやすい、ということもあります。

先に述べた”in”を使って次の証明をしなさい。

Theorem plus_n_n_injective : forall n m,
     n + n = m + m ->
     n = m.
Proof.
  intros n. induction n as [| n'].

    (* FILL IN HERE *) Admitted.

☐

destructを複合式で使う

ここまでdestructタクティックがいくつかの変数の値についてケース分析を行う例をたくさん見てきました。しかし時には、ある式の結果についてケース分析をすることで証明を行う必要があります。このような場合にもdestructタクティックが使えます。.

例を見てください。

Definition sillyfun (n : nat) : bool :=
  if beq_nat n 3 then false
  else if beq_nat n 5 then false
  else false.

Theorem sillyfun_false : forall (n : nat),
  sillyfun n = false.
Proof.
  intros n. unfold sillyfun.
  destruct (beq_nat n 3).
    Case "beq_nat n 3 = true". reflexivity.
    Case "beq_nat n 3 = false". destruct (beq_nat n 5).
      SCase "beq_nat n 5 = true". reflexivity.
      SCase "beq_nat n 5 = false". reflexivity.  Qed.

上の証明でsillyfunを展開すると、if (beq_nat n 3) then ... else ...で行き詰まることがわかります。そこで、nが3である場合とそうでない場合とにdestruct (beq_nat n 3)を使って二つのケースに分け、証明を行います。

Theorem override_shadow : forall {X:Type} x1 x2 k1 k2 (f : nat->X),
  (override (override f k1 x2) k1 x1) k2 = (override f k1 x1) k2.
Proof.
  (* FILL IN HERE *) Admitted.

☐

Admitted.
*)

☐

思考練習: 我々はすでに、全ての型のリストのペアでcombineがsplitの逆関数であることを証明しました。ではその逆の「splitはcombineの逆関数である」を示すことはできるでしょうか？

ヒント:split combine l1 l2 = (l1,l2)がtrueとなるl1、l2の条件は何でしょう？

この定理をCoqで証明しなさい（なるべくintrosを使うタイミングを遅らせ、帰納法の仮定を一般化させておくといいでしょう。

(* FILL IN HERE *)

☐

rememberタクティック

(注:rememberタクティックは、今必ず読んでおかないといけないほどのものではありません。必要になるまでこの項はとばしておいて、必要になってから読んでもいいでしょう。 )

前の項では、destructを使えば任意の演算対象の評価結果についてケース分析できることを見てきました。eが何らかの帰納的な型Tであれば、destruct eは型Tのコンストラクタそれぞれにサブゴールを作成し、起こりえる全ての（ゴールやコンテキストにある）eの状態をコンストラクタcで網羅的に置き換えます。

しかし時折、この置き換えのプロセスで、証明に必要な情報が失われてしまうことがあります。例えば、関数sillyfun1を次のように定義したとします。

Definition sillyfun1 (n : nat) : bool :=
  if beq_nat n 3 then true
  else if beq_nat n 5 then true
  else false.

そしてCoqを使いよく観察することで、sillyfun1 nが、nが奇数のときだけtrueとなりうることを示したいとします。先ほどsillyfunでやった証明を参考に類推すると、証明はこんな風に始まるのが自然に思えます。

Theorem sillyfun1_odd_FAILED : forall (n : nat),
     sillyfun1 n = true ->
     oddb n = true.
Proof.
  intros n eq. unfold sillyfun1 in eq.
  destruct (beq_nat n 3).

Admitted.

しかし証明はここで手詰まりになってしまいます。なぜなら、destructを使ったことで、コンテキストからゴールまでたどりつくのに必要な情報がなくなってしまったからです。destructはbeq_nat n 3の結果起こる事象を全て投げ捨ててしまいますが、我々はそのうち少なくとも一つは残してもらわないと証明が進みません。このケースで必要なのはbeq_nat n 3 = trueで、ここからn = 3は明らかで、ここからnが奇数であることが導かれます。

実際のところやりたいことはdestructをbeq_nat n 3に直接使ってこの式の結果起こることを全て置き換えてしまうことではなく、destructをbeq_nat n 3と同じような何か別のものに適用することです。例えばbeq_nat n 3と同じ値になる変数が分かっているなら、代わりにその値に対してdestructする、といったことです。

rememberタクティックは、そういう変数を導きたいときに使えます。

Theorem sillyfun1_odd : forall (n : nat),
     sillyfun1 n = true ->
     oddb n = true.
Proof.
  intros n eq. unfold sillyfun1 in eq.
   remember (beq_nat n 3) as e3.

   destruct e3.

     Case "e3 = true". apply beq_nat_eq in Heqe3.
       rewrite -> Heqe3. reflexivity.
     Case "e3 = false".

       remember (beq_nat n 5) as e5. destruct e5.
         SCase "e5 = true".
           apply beq_nat_eq in Heqe5.
           rewrite -> Heqe5. reflexivity.
         SCase "e5 = false". inversion eq.  Qed.

Theorem override_same : forall {X:Type} x1 k1 k2 (f : nat->X),
  f k1 = x1 ->
  (override f k1 x1) k2 = f k2.
Proof.
  (* FILL IN HERE *) Admitted.

☐

この問題はやや難しいかもしれません。最初にintrosを使うと、帰納法を適用するための変数まで上に上げてしまうので気をつけてください。

Theorem filter_exercise : forall (X : Type) (test : X -> bool)
                             (x : X) (l lf : list X),
     filter test l = x :: lf ->
     test x = true.
Proof.
  (* FILL IN HERE *) Admitted.

☐

apply ... with ...タクティック

次の例は、[a,b]から[e,f]を得るためにrewriteを二回も使っており、少し要領が悪く思われます。

Example trans_eq_example : forall (a b c d e f : nat),
     [a,b] = [c,d] ->
     [c,d] = [e,f] ->
     [a,b] = [e,f].
Proof.
  intros a b c d e f eq1 eq2.
  rewrite -> eq1. rewrite -> eq2. reflexivity.  Qed.

このようなことがよくあるため、等式が推移的である事実を補題としておきます。

Theorem trans_eq : forall {X:Type} (n m o : X),
  n = m -> m = o -> n = o.
Proof.
  intros X n m o eq1 eq2. rewrite -> eq1. rewrite -> eq2.
  reflexivity.  Qed.

そして、trans_eqをさきほどの証明に使ってみます。しかし、実際にやってみるとapplyタクティックに多少細工が必要なことがわかります。

Example trans_eq_example' : forall (a b c d e f : nat),
     [a,b] = [c,d] ->
     [c,d] = [e,f] ->
     [a,b] = [e,f].
Proof.
  intros a b c d e f eq1 eq2.

  apply trans_eq with (m:=[c,d]). apply eq1. apply eq2.   Qed.

実際には、このように名前mをwithに与えるということはそれほど多くありません。Coqは多くの場合賢く振舞って、我々の要求を実現してくれます。ちなみにこの上のapplyはapply trans_eq withc,dと書くこともできます。

Example trans_eq_exercise : forall (n m o p : nat),
     m = (minustwo o) ->
     (n + p) = m ->
     (n + p) = (minustwo o).
Proof.
  (* FILL IN HERE *) Admitted.

Theorem beq_nat_trans : forall n m p,
  true = beq_nat n m ->
  true = beq_nat m p ->
  true = beq_nat n p.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem override_permute : forall {X:Type} x1 x2 k1 k2 k3 (f : nat->X),
  false = beq_nat k2 k1 ->
  (override (override f k2 x2) k1 x1) k3 = (override (override f k1 x1) k2 x2) k3.
Proof.
  (* FILL IN HERE *) Admitted.

☐

まとめ

ここまでに、たくさんの基本的なタクティックを見てきました。これだけあればしばらくの間は困らずに済むはずです。この先数回のレクチャーで2～3新しいものが出てきますが、その先ではさらに強力な「自動化されたタクティック」を紹介していきます。それを使うと、多くの低レベルな作業をCoqに処理してもらうことができます。しかし基本的に、皆さんはもう必要なことを知っていると考えていいでしょう。

ここまでに出てきたタクティックの一覧です

• intros: 仮定や変数をゴールからコンテキストに移す
• reflexivity: 証明を完了させる（ゴールがe = eという形になっている場合）
• apply: 仮定、補助定理、コンストラクタを使ってゴールを証明する
• apply... in H: 仮定、補助定理、コンストラクタを使ってゴールを証明する（前向きの証明）
• apply... with...: パターンマッチだけで決定できなかった変数を、特定の値に明示的に結びつける
• simpl: ゴールの式を簡約する
• simpl in H: ゴール、もしくは仮定Hの式を簡約する
• rewrite: 等式の形をした仮定（もしくは定理）を使い、ゴールを書き換える
• rewrite ... in H: 等式の形をした仮定（もしくは定理）を使い、ゴールや仮定を書き換える
• unfold: 定義された定数を、ゴールの右側の式で置き換える
• unfold... in H: 定義された定数を、ゴールや仮定の右側の式で置き換える
• destruct... as...: 帰納的に定義された型の値について、ケースごとに解析する
• induction... as...: 機能的に定義された型の値に帰納法を適用する
• inversion: コンストラクタの単射性と独立性を利用して証明を行う
• remember (e) as x: destructxとすることで式を失わないようにするため、式(e)に名前(x)を与える
• assert (e) as H: 定義した補助定理(e)をHという名前でコンテキストに導入する

さらなる練習問題

リストに関する多くの一般的な関数はfoldを使って書きなおすることができます。例えば、次に示すのはlengthの別な実装です。

Definition fold_length {X : Type} (l : list X) : nat :=
  fold (fun _ n => S n) l 0.

Example test_fold_length1 : fold_length [4,7,0] = 3.
Proof. reflexivity. Qed.

fold_lengthが正しいことを証明しなさい。

Theorem fold_length_correct : forall X (l : list X),
  fold_length l = length l.
(* FILL IN HERE *) Admitted.

☐

map関数もfoldを使って書くことができます。以下のfold_mapを完成させなさい。

Definition fold_map {X Y:Type} (f : X -> Y) (l : list X) : list Y :=
(* FILL IN HERE *) admit.

fold_mapの正しさを示す定理をCoqで書き、証明しなさい

(* FILL IN HERE *)

☐

Module MumbleBaz.

つぎの、機能的に定義された二つの型をよく観察してください。

Inductive mumble : Type :=
  | a : mumble
  | b : mumble -> nat -> mumble
  | c : mumble.
Inductive grumble (X:Type) : Type :=
  | d : mumble -> grumble X
  | e : X -> grumble X.

FILL IN HERE 次の式のうち、ある型Xについてgrumble Xの要素として正しく定義されているものはどれでしょうか。

• d (b a 5)
• d mumble (b a 5)
• d bool (b a 5)
• e bool true
• e mumble (b c 0)
• e bool (b c 0)
• c

(* FILL IN HERE *)☐

次の、機能的に定義された型をよく観察してください。

Inductive baz : Type :=
   | x : baz -> baz
   | y : baz -> bool -> baz.

FILL IN HERE 型bazはいくつの要素を持つことができるでしょうか？(* FILL IN HERE *)☐

End MumbleBaz.

チャレンジ問題: 二つの再帰関数forallb、existsbを定義しなさい。forallbは、リストの全ての要素が与えられた条件を満たしているかどうかを返します。

forallb oddb [1,3,5,7,9] = true

forallb negb [false,false] = true

forallb evenb [0,2,4,5] = false

forallb (beq_nat 5) [] = true

existsbは、リストの中に、与えられた条件を満たす要素が一つ以上あるかを返します。

existsb (beq_nat 5) [0,2,3,6] = false

existsb (andb true) [true,true,false] = true

existsb oddb [1,0,0,0,0,3] = true

existsb evenb [] = false

次にexistsb'を再帰関数としてではなく、forallbとnegbを使って定義しなさい。.

そして、existsb'とexistsbが同じ振る舞いをすることを証明しなさい。

(* FILL IN HERE *)

FILL IN HERE ☐

index関数の定義を思い出してください。

Fixpoint index {X : Type} (n : nat) (l : list X) : option X :=
  match l with
  | [] => None
  | a :: l' => if beq_nat n O then Some a else index (pred n) l'
  end.

次の定理の、非形式的な証明を書きなさい。

forall X n l, length l = n -> @index X (S n) l = None.

(* FILL IN HERE *)

☐