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
  | cons : X → list → list.

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

{}を使ってデータ定義に暗黙のパラメータを与えることができる

listとはいったい何なのか、というと、「暗に型を引数にとり、帰納的な定義を返す関数である」あるいは「暗に型を引数にとり、型を返す関数」と考えてもいいかもしれません。


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 listnatex := [1, 2, 3].

Definition listboolex := [true, true, false].

natのlistでもboolのlistでも同様の書き方が可能

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

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

X:=X により、list定義中の暗黙のXに、ここでのXを明示的にあてはめている

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

nilやconsと同様に、lengthも暗黙の型を意識せずに使うことができます。

Example test_length1 :
    length [1,2] = 2.
Proof. reflexivity. Qed.

このlengthを別の型のリストに使うこともできます。

Example test_length2 :
    length [true] = 1.
Proof. reflexivity. Qed.

lengthがnatにもboolにも使える

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

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

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

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

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

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

暗黙のXが定まらないときは明示しないといけない

型推論


それでは、app関数の定義をもう一度書いてみましょう。ただし今回は、全ての暗黙の型を明示してみます。

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

（せっかく暗黙にしている意味が無い…）


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

consの後の X:=X だけでも定義可能

Coqは型推論という機構を持っていて、これを使い、l1やl2の型が何であるべきかを、その使われ方から導き出します。例えば、cons (X:=X) h とあることから h の型は X だと分かり、h は l1 が分解されたものであるので l1 の型は list (X:=X) であることが分かります。

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

型の記述を省略できる所もある

quiz07-a



引数の同化（Synthesis）


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

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

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

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

周りの記述から定まる型は省略してOK

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


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

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

Fixpoint repeat {X : Type} (n : X) (count : nat) : list (X:=X) :=
   admit.

Example test_repeat1:
  repeat true 2 = cons true (cons true nil).
Admitted.

Theorem nil_app : ∀ X:Type, ∀ l:list (X:=X),
  app [] l = l.
Proof.
Admitted.

Theorem rev_snoc : ∀ X : Type,
                     ∀ v : X,
                     ∀ s : list X,
  rev (snoc s v) = v :: (rev s).
Proof.
Admitted.
☐

多相的なペア


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

Inductive prod {X Y : Type} : Type :=
  pair : X → Y → prod.

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

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

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

Notation "X * Y" := (prod (X:=X) (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:=X)) (ly : list (X:=Y))
           : list (X*Y) :=
  match (lx,ly) with
  | ([],_) => []
  | (_,[]) => []
  | (x::tx, y::ty) => (x,y) :: (combine tx ty)
  end.

combine [1,2] [true,false] = [(1,true),(2,flase)]

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

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

練習問題: ★ (combine_checks)

次の質問の答えを紙に書いた後で、Coqの出した答えと同じかチェックしなさい。
  • 関数combineの型は何でしょう (Check @combineの出力結果は？
  • それでは
            Eval simpl in (combine [1,2] [false,false,true,true]).

    は何を出力する？ ☐

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

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

☐

多相的なオプション


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

Inductive option {X:Type} : Type :=
  | Some : X → option
  | None : option.

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

Fixpoint index {X : Type} (n : nat)
               (l : list (X:=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.

練習問題: ★, optional (hd_opt_poly)

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

Definition hd_opt {X : Type} (l : list (X:=X)) : option (X:=X) :=
   admit.


Example test_hd_opt1 : hd_opt [1,2] = Some 1.
Admitted.
Example test_hd_opt2 : hd_opt [[1],[2]] = Some [1].
Admitted.
☐

quiz07-b



Report6:Teamsの形式手法チームの課題タブを参照してください


07↑↓08

データとしての関数


高階関数


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

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

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

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


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に二つの引数を一緒に与えていましたが、もし望むなら最初の一つだけを与えることもできます。これを部分適用といいます。
plusは「引数を1つ与えた戻り値として関数を返している」という見方ができる


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.

余談： カリー化


advanced topic

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

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 :=
   admit.

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

Check @prod_curry.
Check @prod_uncurry.

Theorem uncurry_curry : ∀ (X Y Z : Type) (f : X → Y → Z) x y,
  prod_curry (prod_uncurry f) x y = f x y.
Proof.
Admitted.

Theorem curry_uncurry : ∀ (X Y Z : Type)
                               (f : (X * Y) → Z) (p : X * Y),
  prod_uncurry (prod_curry f) p = f p.
Proof.
Admitted.
☐

フィルター (Filter)関数


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

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

testしてtrueとなる要素のみにして返す

例えば、この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:=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 :=
  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.

(fun…)の部分は2乗する関数だが名前は無い

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

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.

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


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

Definition filter_even_gt7 (l : list (X:=nat)) : list (X:=nat) :=
   admit.

Example test_filter_even_gt7_1 :
  filter_even_gt7 [1,2,6,9,10,3,12,8] = [10,12,8].
Admitted.

Example test_filter_even_gt7_2 :
  filter_even_gt7 [5,2,6,19,129] = [].
Admitted.

☐

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

filter関数を使って、partition関数を書きなさい。:
  partition : ∀ X : Type,
              (X → bool) → list (X:=X) → list (X:=X) * list (X:=X)

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

Definition partition {X : Type} (test : X → bool) (l : list X)
                     : list X * list X :=
admit.

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

quiz08-a

マップ（Map）関数


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

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

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

Xの関数をXのリストに使える


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.

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

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

Theorem map_rev : ∀ (X Y : Type) (f : X → Y) (l : list),
  map f (rev l) = rev (map f l).
Proof.
Admitted.
☐

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

map関数は、list (X:=X)からlist (X:=Y)へのマップを、型X → Yの関数を使って実現しています。同じような関数flat_mapを定義しましょう。これはlist (X:=X)からlist (X:=Y)へのマップですが、X → list (X:=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 (X:=Y)) (l:list (X:=X))
                   : (list (X:=Y)) :=
   admit.

Example test_flat_map1:
  flat_map (fun n => [n,n,n]) [1,5,4]
  = [1, 1, 1, 5, 5, 5, 4, 4, 4].
Admitted.
☐

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

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

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

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

畳み込み（Fold）関数


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

Fixpoint fold {X Y:Type} (f: X→Y→Y) (l:list) (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))).

foldは二項演算子をリストに適用する

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

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.

練習問題: ★, optional (fold_types_different)

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.

練習問題: ★ (override_example)

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

Theorem override_example : ∀ (b:bool),
  (override (constfun b) 3 true) 2 = b.
Proof.
Admitted.
☐

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

quiz08-b



Report7：Teamsの形式手法チームの課題タブを参照してください


08↑↓09

さらにCoqについて




unfoldタクティック


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

Theorem unfold_example_bad : ∀ m n,
  3 + n = m →
  plus3 n + 1 = m + 1.
Proof.
  intros m n H.
  Admitted.

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

Theorem unfold_example : ∀ m n,
  3 + n = m →
  plus3 n + 1 = m + 1.
Proof.
  intros m n H.
  unfold plus3.
  rewrite → H.
  reflexivity. Qed.


unfold: 指定した関数を展開

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

Theorem override_eq : ∀ {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を必要としている点だけ注意してください。

練習問題: ★★ (override_neq)

Theorem override_neq : ∀ {X:Type} x1 x2 k1 k2 (f : nat→X),
  f k1 = x1 →
  beq_nat k2 k1 = false →
  (override f k2 x2) k1 = x1.
Proof.
Admitted.
☐

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

反転（Inversion）


自然数の定義を思い出してください。
     Inductive nat : Type :=
       | O : nat
       | S : nat → nat.

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

各コンストラクタは独立したものであるべき

同じ原理が、全ての帰納的に定義された型にあてはまります。全てのコンストラクタは単射で、コンストラクタが違えば同じ値は生まれません。リストについて言えば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とすることで、この等式を"反転"し、そこに含まれている情報を以下のようなやり方で引き出します。

完全に一致するか、矛盾が生じているのかのどちらか

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

Theorem eq_add_S : ∀ (n m : nat),
     S n = S m →
     n = m.
Proof.
  intros n m eq. inversion eq. reflexivity. Qed.

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


inversionでコンストラクタを消せる（1引数の場合、そう見える）

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

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

練習問題: ★ (sillyex1)

Example sillyex1 : ∀ (X : Type) (x y z : X) (l j : list X),
     x :: y :: l = z :: j →
     y :: l = x :: j →
     x = y.
Proof.
Admitted.
☐

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

矛盾が生じてる場合、何でも証明できてしまう

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

練習問題: ★ (sillyex2)

Example sillyex2 : ∀ (X : Type) (x y z : X) (l j : list X),
     x :: y :: l = [] →
     y :: l = z :: j →
     x = z.
Proof.
Admitted.
☐

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

Lemma eq_remove_S : ∀ n m,
  n = m → S n = S m.
Proof. intros n m eq. rewrite → eq. reflexivity. Qed.

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

Theorem beq_nat_eq : ∀ 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_informal)

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

☐

練習問題: ★★★ (beq_nat_eq')

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

Theorem beq_nat_eq' : ∀ m n,
  beq_nat n m = true → n = m.
Proof.
  intros m. induction m as [| m'].
Admitted.
☐

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

Theorem length_snoc' : ∀ (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 : ∀ n,
  true = beq_nat 0 n → 0 = n.
Proof.
Admitted.

Theorem beq_nat_0_r : ∀ n,
  true = beq_nat n 0 → 0 = n.
Proof.
Admitted.
☐

Theorem double_injective : ∀ 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.

quiz09-a



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


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

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

Theorem S_inj : ∀ (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.


コンテキストの中にsimplを使う

同様に、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' : ∀ (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.


コンテキストの中にsymmetryやapplyを使う

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

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

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

Theorem plus_n_n_injective : ∀ n m,
     n + n = m + m →
     n = m.
Proof.
  intros n. induction n as [| n'].
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 : ∀ (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)を使って二つのケースに分け、証明を行います。

destruct a だけでなく、destruct (f a) の形でも使える


練習問題: ★ (override_shadow)

Theorem override_shadow : ∀ {X:Type} x1 x2 k1 k2 (f : nat→X),
  (override (override f k1 x2) k1 x1) k2 = (override f k1 x1) k2.
Proof.
Admitted.
☐

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

☐

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

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

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

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

☐

rememberタクティック


advanced topic: destructするが、元の値も忘れたくないときに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 : ∀ (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 : ∀ (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.

練習問題: ★★ (override_same)

Theorem override_same : ∀ {X:Type} x1 k1 k2 (f : nat→X),
  f k1 = x1 →
  (override f k1 x1) k2 = f k2.
Proof.
Admitted.
☐

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

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

Theorem filter_exercise : ∀ (X : Type) (test : X → bool)
                             (x : X) (l lf : list X),
     filter test l = x :: lf →
     test x = true.
Proof.
Admitted.
☐

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


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

Example trans_eq_example : ∀ (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 : ∀ {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' : ∀ (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.

apply trans_eq だけでは変数の対応が定まらないので、それをwithで与える

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

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

Example trans_eq_exercise : ∀ (n m o p : nat),
     m = (minustwo o) →
     (n + p) = m →
     (n + p) = (minustwo o).
Proof.
Admitted.

Theorem beq_nat_trans : ∀ n m p,
  true = beq_nat n m →
  true = beq_nat m p →
  true = beq_nat n p.
Proof.
Admitted.

Theorem override_permute : ∀ {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.
Admitted.
☐

まとめ


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

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

quiz09-b



Report8：Teamsの形式手法チームの課題タブを参照してください


09↑

さらなる練習問題


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

リストに関する多くの一般的な関数は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 : ∀ X (l : list X),
  fold_length l = length l.
Admitted.
☐

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

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

Definition fold_map {X Y:Type} (f : X → Y) (l : list X) : list Y :=
admit.

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

☐

Module MumbleBaz.

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

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

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

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

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

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

Inductive baz : Type :=
   | x : baz → baz
   | y : baz → bool → baz.

型bazはいくつの要素を持つことができるでしょうか？ ☐

End MumbleBaz.

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

チャレンジ問題: 二つの再帰関数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が同じ振る舞いをすることを証明しなさい。

☐

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

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.

次の定理の、非形式的な証明を書きなさい。
   ∀ X n l, length l = n → @index X (S n) l = None.

☐