自然数を扱う

4章では自然数を扱います。まず自然数とその加法、乗法を定義し、自然数に関する帰納法による証明を紹介します。その後は自然数の性質二つと、それらを使って鳩の巣原理と呼ばれる命題を証明します。

自然数の定義

Coq で自然数は Inductive を使って以下のように定義されます。

Inductive nat : Set := 
  | O : nat              (* 0(ゼロ) ではなく O(オー)です *)
  | S : nat -> nat.

Set はソートの一種で、プログラムに使う型を含んでいます。

O(オー) は 0(ゼロ) の意味で、S は自然数 a を受け取って a の次の自然数を返す関数、つまり S a は a + 1 の意味です。

これらを使って、1 は "S O"、2 は "S (S O)"、3 は "S (S (S O))" と表現されますが、いくつも S を書くのは面倒なので Coq では単に数字で "0"、"1"、"2"、…… と書けばそれぞれ O、S O、S (S O)、……と解釈されます。

また、自然数の加法と乗法は次のように定められます。

Fixpoint plus (n m : nat) : nat :=
  match n with
  | O => m
  | S p => S (plus p m)
  end.

Fixpoint mult (n m : nat) : nat :=
  match n with
  | O => O
  | S p => m + mult p m
  end.

n と m に具体的な値を代入してみれば確かに加法と乗法になっていることが分かります。plus n m、mult n m はそれぞれ "n + m"、"n * m" と書けます。

自然数に関する帰納法

自然数の加法や乗法には、たとえば n = n + 0 や (a * b) * c = a * (b * c) など沢山の性質がありますが、これらはリストのときと同じように帰納法を使って証明できます。

自然数に関する帰納法は

となります。3章 で出たリストに関する帰納法と似ていますね。

帰納法を使って n = n + 0 の証明をしてみます。

Goal forall (n : nat), n = n + 0.
intros.

1 subgoal
n : nat
______________________________________(1/1)
n = n + 0

となり、この後リストの証明のときのように n に対して induction タクティクを使ってみると

induction n.

2 subgoals
______________________________________(1/2)
0 = 0 + 0


______________________________________(2/2)
S n = S n + 0

と証明図が変わります。一つ目のサブゴールは (1)、二つ目のサブゴールは (2) に対応しています。

この後は難しくないので続けて書いてしまうと

reflexivity.
simpl.
f_equal.
apply IHn.
Qed.

です。自然数はリストと似た構造をしているので、自然数の加法や乗法に関する性質の証明はリストのときとよく似た手順で証明できることが多いです。また加法や乗法の基本的な定理の多くは標準ライブラリの Arith モジュールにあります。そのため 4 章では加法や乗法の基本的な定理は自分で証明せず、Arith モジュールをインポートし、そこにある定理を利用して別の自然数の性質を証明してみようと思います。

Arith モジュールをインポートするには、List と同じように

Require Import Arith.

とします。

自然数の性質

この節では「〜が存在する」という命題からなる自然数の性質を一つと、不等号が入った命題の証明をします。

存在証明

まず自然数のこんな性質を証明してみます。

「〜が存在する」という命題はこれまでに出て来ませんでした。「〜が存在する」という命題は exists を使って表します。上の命題は、

forall (n : nat), (exists m : nat, n = m * 4) -> exists k : nat, n = k * 2

と型で書けます。exists は forall に似た表記で使い、「P をみたす a : A が存在する」は "exists a : A, P" のように exists の後に存在する対象、カンマの後に存在する条件が続きます。ではこの命題を証明してみましょう。

Require Import Arith.

Goal forall (n : nat), (exists m : nat, n = m * 4) -> exists k : nat, n = k * 2.
intros.

1 subgoal
n : nat
H : exists m : nat, n = m * 4
______________________________________(1/1)
exists k : nat, n = k * 2

intros タクティクを使ってみると、証明図がこのようになりました。仮定の H の型は exists が使われています。仮定に "X : exists 〜" があるときも、 and や or と同様、 case や destruct タクティクが使えます。

destruct H.

1 subgoal
n : nat
x : nat
H : n = x * 4
______________________________________(1/1)
exists k : nat, n = k * 2

仮定に "x : nat" が増え、H の型が "n = x * 4" に変わりました。destruct は何をしたかというと、前の段階で「n = m * 4 をみたす m が存在する」と分かっていた(仮定にあった)ので「具体的にその m を x という変数で表す」というはたらきをしました。

これで H の型が exists を使わずに表され、扱いやすい型になりました。ではサブゴールを見てみます。「n = k * 2 をみたす k が存在する」ことを示せばいいのですから、実際に n = k * 2 となる k を与えてやれば証明になります。たとえば「ネッシーが存在する」ことを示したいならば、この場にネッシーを一匹でも連れてくれば確かな証明になりますね。

それでは n = k * 2 をみたす k には何があるでしょう。仮定の H から n = x * 4 であることが分かっているので、k に x * 2 を代入すれば確かに n = k * 2 = (x * 2) * 2 = x * 4 となり、正しい式になります。

サブゴールが "exists x, P" のとき、P をみたす x を具体的に与えるには exists というタクティクを使います。型にある exists と同じ名前ですが、中身は別なので注意してださい。

exists (x * 2).

1 subgoal
n : nat
x : nat
H : n = x * 4
______________________________________(1/1)
n = x * 2 * 2

k に x * 2 が代入されました。H をそのまま適用するために n = x * 2 * 2 を簡約して n = x * 4 に変形したいところです。2 * 2 は simpl タクティクで 4 に簡約できますが、* は左結合なので、"x * 2 * 2" は "(x * 2) * 2" となってしまい、そのままでは簡約できません。そのためまず x * 2 * 2 を x * (2 * 2) に変形します。

Arith モジュールをインポートすると

mult_assoc_reverse : forall (n m p : nat), n * m * p = n * (m * p)

という定理が利用できます。

Coq の標準ライブラリはここで見れ、mult_assoc_reverse はArith.Multにあります。便利な定理が色々あるので、端から眺めていっても面白いと思います。

rewrite タクティクで mult_assoc_reverse を使って x * 2 * 2 を x * (2 * 2) に変形しましょう。

rewrite mult_assoc_reverse.

1 subgoal
n : nat
x : nat
H : n = x * 4
______________________________________(1/1)
n = x * (2 * 2)

これで simpl タクティクを使えば 2 * 2 を 4 に簡約できます。

simpl.

1 subgoal
n : nat
x : nat
H : n = x * 4
______________________________________(1/1)
n = x * 4

あとは H をそのまま apply すれば証明終了ですね。

apply H.
Qed.

Unnamed_thm0 is defined

これまでの証明をまとめて書きます。

Goal forall (n : nat), (exists m : nat, n = m * 4) -> exists k : nat, n = k * 2.
intros.
destruct H.                   (* 仮定の H : exists m : nat, n = m * 4 を H : n = x * 4 に *)
exists (x * 2).               (* サブゴールの exists に x * 2 を与える *)
rewrite mult_assoc_reverse.   (* x * 2 * 2 を x * (2 * 2) に *)
simpl.
apply H.
Qed.

不等号

今度は、不等号の入ったこんな命題を証明してみます。

lt_Snm_nm : forall (n m : nat), S n < m -> n < m

"a < b" は「b は a より大きい」という命題を表す型です。"=" と同じように、ブール値を返す関数ではありません。

この lt_Snm_nm を言葉で書くと、

となります。ここでは lt_Snm_nm を次のような Arith モジュールにある定理を使って証明しようと思います。

lt_trans : forall n m p, n < m -> m < p -> n < p

lt_n_Sn : forall n, n < S n

この二つの定理を使うと、lt_Snm_nm はとてもシンプルに証明できます。

Theorem lt_Snm_nm : forall (n m : nat), S n < m -> n < m.

1 subgoal
______________________________________(1/1)
forall n m : nat, S n < m -> n < m

intros.

1 subgoal
n : nat
m : nat
H : S n < m
______________________________________(1/1)
n < m

ここで、lt_trans の "forall n m p," の n、m、p それぞれに仮定の n、(S n)、m を代入してみると "n < S n -> S n < m -> n < m" となり、サブゴールに apply できます。

apply (lt_trans n (S n) m).

2 subgoals
n : nat
m : nat
H : S n < m
______________________________________(1/2)
n < S n


______________________________________(2/2)
S n < m

一つ目のサブゴールは lt_n_Sn、二つ目は仮定の H そのままなので、それらを apply すれば証明終了です。

apply lt_n_Sn.
apply H.
Qed.

証明のまとめを書きます。

Require Import List.
Require Import Arith.
 
Theorem lt_Snm_nm : forall (n m : nat), S n < m -> n < m.
intros.
apply (lt_trans n (S n) m).
apply lt_n_Sn.
apply H.
Qed.

リストと自然数

この節では、これまでの知識を使って以下の定理を証明します。 これまでは and や or など、最初から定義されていた型を使った命題を証明していましたが、この節では自分で型を定義してそれについての証明をしてみようと思います。

これは「鳩の巣原理」や「ディリクレの箱入れ原理」などと呼ばれます。

新しい型の定義

Coq で鳩の巣原理を表現するには少し工夫が要ります。Coq で表現するために、ここでは「m 個の箱の列」を「長さ m のリスト」、「i 番目の箱に n 個の物が入っている」ということを「リストの i 番目の要素は n である」と置き換えます。たとえば「箱の列 xs で、ある箱に 1 個の物が入っている」という命題をこの置き換えの下で表すと、「リスト xs の、ある要素は 1 である」となり、言い方を変えると「1 はリスト xs の要素である」となります。この「a はリスト xs の要素である」という命題を表すために、今回は新しく自分で型を定義します。

Coq でデータ型を定義するときは、そのデータ型が何からできているかを列挙して定義します。たとえばすでに登場した型 or は

Inductive or (A B : Prop) : Prop :=
  | or_introl : A -> or A B
  | or_intror : B -> or A B.

と定義されており、「A または B が成り立つ」は「A が成り立つ」と「B が成り立つ」のどちらかからできているので上のように定義されるのでした。

「a が xs の要素である」という命題が何からできているかを考えましょう。リストに a が属している場合、以下のどちらかが成り立ちます。

直感的には、リストの「先頭の要素が a である」と「残りに a が属している」のように解釈できます。これを Inductive を使って定義してみましょう。

Inductive InList (A : Type)(a : A) : list A -> Prop :=
  | headIL : forall xs, InList A a (a::xs)   (* 1 *)
  | consIL : forall x xs, InList A a xs -> InList A a (x::xs).   (* 2 *)

コメントで付けた (* 1 *)、(* 2 *) がそれぞれ 1、2 に対応していますね。それでは、InList を用いて鳩の巣原理を Coq で表現してみます。

pigeonhole : forall (xs : list nat),
  length xs < fold_right plus 0 xs -> exists x : nat, InList nat (S (S x)) xs

端から順番に定義を見てみます。まず、xs は箱の列に相当し、前述したとおり xs の i 番目の要素が n であることは i 番目の箱に n 個の物が入っていることを表します。"forall (xs : list nat), " は「任意のリスト xs に対して」という意味でしたが、リストを箱に置き換えて意味を考えると「任意の箱の列に対して、物がどのように入っていても」となります。

次に length という関数が見えます。length は文字通りリストを受け取ってその長さを返す関数で、型は "forall (A : Type), list A -> nat" です。これで length xs が箱の個数を表すと分かります。

fold_right は 3章 の練習問題で登場した関数で、以下のように定義されていました。

Fixpoint fold_right (A B : Type)(f : B -> A -> A)(a0 : A)(l : list B) : A :=
  match l with
  | nil => a0
  | b :: t => f b (fold_right A B f a0 t)
  end.
(ただし標準ライブラリにある fold_right を使う場合は A B は省略可)

fold_right plus 0 xs は xs の要素の総和を計算します。具体的に、たとえば xs を 3 :: (2 :: (1 :: nil)) として fold_right を定義通り展開すると 3 + (2 + (1 + 0)) となり、要素の総和になっていますね。

xs の i 番目の要素は i 番目の箱に入っている物の個数を表すので、要素の総和は「物が全部で何個あるか」を表します。これを踏まえて "length xs < fold_right plus 0 xs" がどういう意味かを考えると、「(箱の個数) < (物全部の個数)」となり、言葉で書いた鳩の巣原理の m と n はそれぞれ箱の個数と物全部の個数であったので、きちんと対応が取れていることが分かります。

最後に "exists x : nat, InList nat (S (S x)) xs" です。そのまま言葉にすると「x + 2 がリスト xs の要素になるような自然数 x が存在する」で、リストを箱に置き換えると「ある箱に x + 2 個の物が入るような x が存在する」となります。少し分かり辛いですが、Coq で自然数は 0 から始まることに注意するとこれは「ある箱に 2 個以上の物が入っている」と書き直せます。これで pigeonhole の型が言葉で書いた命題を表現していることが確認できました。

鳩の巣原理の証明

それでは鳩の巣原理の証明をしてみましょう。

Require Import List.
Require Import Arith.

Theorem pigeonhole : forall (xs : list nat),
  length xs < fold_right plus 0 xs -> exists x : nat, InList nat (S (S x)) xs.

1 subgoal
______________________________________(1/1)
forall xs : list nat,
length xs < fold_right plus 0 xs -> exists x : nat, InList nat (S (S x)) xs

intros して、xs についての帰納法で証明します。

intros.
induction xs.

2 subgoals
H : length nil < fold_right plus 0 nil
______________________________________(1/2)
exists x : nat, InList nat (S (S x)) nil


______________________________________(2/2)
exists x : nat, InList nat (S (S x)) (a :: xs)

仮定の H を見てみましょう。定義から length nil と fold_right plus 0 nil は両方とも 0 に簡約できます。仮定 H の型を簡約するには、"simpl in H." と書きます。

simpl in H.

2 subgoals
H : 0 < 0
______________________________________(1/2)
exists x : nat, InList nat (S (S x)) nil

...

ここで、0 < 0 は明らかに間違った命題ですね。二階論理で、全ての P に対して "(矛盾) → P" は真とされています。

Coq では "False_ind : forall (P : Prop), False -> P" という定理を使います。

apply False_ind.

2 subgoals
H : 0 < 0
______________________________________(1/2)
False

...

一つ目のサブゴールが False に変わりました。これで H から矛盾が導かれることを示せれば一つ目のサブゴールの証明は完了です。Arith モジュールには

lt_n_O : forall (n : nat), ~ n < 0

という定理があります。~ P は P -> False の別の書き方だったことを思い出せば、lt_n_O はサブゴールに apply できることに気付きます。n に 0 を代入すると 0 < 0 -> False となるので、H を lt_n_O に渡せば False が証明されます。

apply (lt_n_O 0 H).

1 subgoal
a : nat
xs : list nat
H : length (a :: xs) < fold_right plus 0 (a :: xs)
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/1)
exists x : nat, InList nat (S (S x)) (a :: xs)

サブゴールが一つ消えました。H を見ると、length (a :: xs) は S (legnth xs) に、fold_right plus 0 (a :: xs) は a + fold_right plus 0 xs に簡約できるので simpl タクティクを使います。

simpl in H.

1 subgoal
a : nat
xs : list nat
H : S (length xs) < a + fold_right plus 0 xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/1)
exists x : nat, InList nat (S (S x)) (a :: xs)

この後どうすれば良いか考えてみます。まず InList nat (S (S x)) (a :: xs) が成り立つのは

(1) headIL : forall xs, InList A a (a::xs)
(2) consIL : forall y xs, InList A (S (S x))xs -> InList A (S (S x)) (a::xs)

のどちらかが成り立つときです。今のサブゴールに合てはめてみると、(1) が成り立つのは S (S x) = a のとき、(2) が成り立つのは InList nat (S (S x)) xs が成り立つときです。

まず (2) と仮定の IHxs に注目してみます。IHxs の型は

length xs < fold_right plus 0 xs -> exists x : nat, InList nat (S (S x)) xs

であり、(2) の consIL の型をサブゴールに合うように変数に値を代入すると

InList nat (S (S x)) xs -> InList nat (S (S x)) (a :: xs)

となります。この二つを合わせて考えると、もし length xs < fold_right plus 0 xs が成り立つならば IHxs により InList nat (S (S x)) xs なる x が存在します。そこから consIL によりその x について InList nat (S (S x)) (a :: xs) が成り立ち、めでたくサブゴールの形になりました。

これより length xs < fold_right plus 0 xs が成り立つときはこのサブゴールは証明できそうです。ではどんなときに length xs < fold_right plus 0 xs が成り立つのでしょうか。仮定を見ると "H : S (length xs) < a + fold_right plus 0 xs" とあり、これを上手く変形して length xs < fold_right plus 0 xs に持って行きましょう。ここでは a に関して場合分けをして考えてみます。

もし a = 0 ならば、a + fold_right plus 0 xs = fold_right plus 0 xs となり、H は S (length xs) < fold_right plus 0 xs となります。ここで前に証明した lt_Snm_nm : forall (n m : nat), S n < m -> n < m を使うと、length xs < fold_right plus 0 xs が導けます。

a = 1 のときは、a + fold_right plus 0 xs = 1 + fold_right plus 0 xs = S (fold_right plus 0 xs) となり、H は S (length xs) < S (fold_right plus 0 xs) となります。これは両辺の S を取れば length xs < fold_right plus 0 xs になりますね。

a ≧ 2、違う書き方をすると、何か自然数 a' が存在して a = 2 + a' と書けるときはどうでしょう。結論を言うと、a ≧ 2 のときは H から length xs < fold_right plus 0 xs が成り立つかどうかは他の条件がないと分かりません。このことは自分で不等式を変形してみれば確認できると思います。ではどうやってこのサブゴールを証明するかというと、証明の方向を変えます。a = 0, 1 のときは (2)、つまり consIL を使って証明を進めようとしましたが、a ≧ 2 のときは (1)、headIL を使って証明ができます。

headIL が成り立つのは S (S x) = a のときなので、そのような x が存在すればサブゴールは証明できます。しかしそれは場合分けの仮定、「何か自然数 a' が存在して a = 2 + a' と書ける」そのものなので、ただちにサブゴールが証明できます。

それではこの証明を Coq に書き下しましょう。

a = 0 の場合

a に関しての場合分けをするので、destruct を使います。

destruct a.

2 subgoals
xs : list nat
H : S (length xs) < 0 + fold_right plus 0 xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
exists x : nat, InList nat (S (S x)) (0 :: xs)

...

この後は lt_Snm_nm を使って H から "length xs < fold_right plus 0 xs" を導く予定でした。一般に定理 "T : A -> B" があり、仮定に "X : A" があるとき、T を使って X から B を導きたいときは

apply T in X.

と書きます。実際に使ってみましょう。

apply lt_Snm_nm in H.

2 subgoals
xs : list nat
H : length xs < 0 + fold_right plus 0 xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
exists x : nat, InList nat (S (S x)) (0 :: xs)

...

H の型が length xs < 0 + fold_right plus 0 xs に変わりました。今度は IHxs を使って H から "InList nat (S (S x)) xs" を導けます。

apply IHxs in H.

2 subgoals
xs : list nat
H : exists x : nat, InList nat (S (S x)) xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
exists x : nat, InList nat (S (S x)) (0 :: xs)

...

H の型がまた変わりました。次は、前節の存在証明を思い出しましょう。仮定に "exists x : nat, 〜" があるので、destruct が使えて具体的に x という変数を仮定に入れられます。

destruct H.

2 subgoals
xs : list nat
x : nat
H : InList nat (S (S x)) xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
exists x0 : nat, InList nat (S (S x0)) (0 :: xs)

...

サブゴールが "exists X, 〜" のときは exists タクティクを使いました。x が "InList nat (S (S x)) (0 :: xs)" をみたして存在することを exists タクティクを使って Coq に教えましょう。

exists x.

2 subgoals
xs : list nat
x : nat
H : InList nat (S (S x)) xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
InList nat (S (S x)) (0 :: xs)

...

x0 が x に置き換わり、先頭の exists が消えました。

consIL の型は forall x xs, InList A a xs -> InList A a (x::xs) なのでサブゴールに適用できます。"apply consIL." しても良いですし、InList は二つの型構成子から成っていて、consIL はそのうちの一つ目なので "right." でも同じ挙動をします。しかし今回は constructor という新しいタクティクを使ってみます。

constructor.

2 subgoals
xs : list nat
x : nat
H : InList nat (S (S x)) xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
InList nat (S (S x)) xs

...

サブゴールが、"apply consIL." するときと同じ形になりました。constructor タクティクは、現在のサブゴールを見てそれに apply できる型構成子を推論できる場合は自動でその型構成子を apply します。そのまま apply を使う場合は自分で型構成子を指定しなければいけませんが、constructor を使えばその必要はありません。また left や right は型構成子が二つのときに限定されて使えましたが、constructor は型構成子の数がいくつでも使えます。

このサブゴールは H をそのまま apply すれば証明できますね。

apply H.

1 subgoal
a : nat
xs : list nat
H : S (length xs) < S a + fold_right plus 0 xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/1)
exists x : nat, InList nat (S (S x)) (S a :: xs)

サブゴールが一つに減りました。

a = 1 の場合

今回は a が 0、1、2 以上、の三つの場合分けで証明するので、もう一度 destruct を使います。

destruct a.

2 subgoals
xs : list nat
H : S (length xs) < 1 + fold_right plus 0 xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
exists x : nat, InList nat (S (S x)) (1 :: xs)


______________________________________(2/2)
exists x : nat, InList nat (S (S x)) (S (S a) :: xs)

またサブゴールが二つになりましたが、一つ目のサブゴールは先程の要領ですぐに示せます。まず、"1 + fold_right plus 0 xs" を "S (fold_right plus 0 xs)" に簡約しましょう。

simpl in H.

2 subgoals
xs : list nat
H : S (length xs) < S (fold_right plus 0 xs)
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
exists x : nat, InList nat (S (S x)) (1 :: xs)

...

ここで、Arith モジュールにある

lt_S_n : forall (n m : nat), S n < S m -> n < m

という定理を使います。これは H に apply できますね。

apply lt_S_n in H.

2 subgoals
xs : list nat
H : length xs < fold_right plus 0 xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
exists x : nat, InList nat (S (S x)) (1 :: xs)

...

これで IHxs が H に apply できます。

apply IHxs in H.

2 subgoals
xs : list nat
H : exists x : nat, InList nat (S (S x)) xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
exists x : nat, InList nat (S (S x)) (1 :: xs)

...

ここからは先程のサブゴールのときの証明と同じです。H を destruct して x を取り出し、サブゴールに exists タクティクを使って与えましょう。

destruct H.

2 subgoals
xs : list nat
x : nat
H : InList nat (S (S x)) xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
exists x0 : nat, InList nat (S (S x0)) (1 :: xs)

...

exists x.

2 subgoals
xs : list nat
x : nat
H : InList nat (S (S x)) xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
InList nat (S (S x)) (1 :: xs)

...

また constructor タクティクが使えますね。

constructor.

2 subgoals
xs : list nat
x : nat
H : InList nat (S (S x)) xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/2)
InList nat (S (S x)) xs

...

apply H.

1 subgoal
a : nat
xs : list nat
H : S (length xs) < S (S a) + fold_right plus 0 xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/1)
exists x : nat, InList nat (S (S x)) (S (S a) :: xs)

a = 1 のときも証明できました。

a ≧ 2 の場合

今度は headIL を使って証明を進めるんでしたね。S (S x) = S (S a) になるように、"exists x : nat," の x を a として exists タクティクを使って与えます。

exists a.

1 subgoal
a : nat
xs : list nat
H : S (length xs) < S (S a) + fold_right plus 0 xs
IHxs : length xs < fold_right plus 0 xs ->
       exists x : nat, InList nat (S (S x)) xs
______________________________________(1/1)
InList nat (S (S a)) (S (S a) :: xs)

これは headIL の型に合うようにサブゴールが変わりました。"apply headIL." か "constructor." を使いましょう。

constructor.

Proof completed.

これで証明終了です!

今回はいつもより複雑でしたね。この章では Arith モジュールにある定理を使って、発展した命題を証明することを目標にしたので、証明中に使った lt_n_O や lt_S_n などの証明はしません。気になったら自分で証明してみても良いでしょう。

最後に証明のまとめを書きます。

Theorem pigeonhole : forall (xs : list nat),
  length xs < fold_right plus 0 xs -> exists x : nat, InList nat (S (S x)) xs.
intros.
induction xs.
 simpl in H.
 apply False_ind.
 apply (lt_n_O 0 H).

 simpl in H.
 destruct a.
  apply ltS in H.      (* a = 0 の場合 *)
  apply IHxs in H.
  destruct H.
  exists x.
  constructor.
  apply H.

  destruct a.          (* a = 1 の場合 *)
   simpl in H.
   apply lt_S_n in H.
   apply IHxs in H.
   destruct H.
   exists x.
   constructor.
   apply H.

   exists a.            (* a ≧ 2 の場合 *)
   constructor.
Qed.

イコールや自然数に関する命題についての自動証明タクティク

1章で auto や tauto といった自動証明タクティクを紹介しましたが、これらの他にイコールや自然数の証明をするときに特化した自動証明タクティクがいくつかあります。

x = y の形のサブゴールを証明するときに便利なのが、trivial というタクティクです。たとえば全ての自然数 n に対して 0 = n * 0 であることを示したいとすると、

Goal forall (n : nat), 0 = n * 0.
trivial.
Qed.

だけで自動的に証明が終了します。他にも auto の後に with arith を加えることによって自然数の証明に特化した自動証明ができます。具体的にこのように使います。

Goal forall (n m : nat), n * m = m * n.
auto with arith.
Qed.

他にも自然数の証明に役立つ自動証明タクティクとして omega があります。omega タクティクを使うには Omega モジュールをインポートする必要があります。

Require Import Omega.

Goal forall n m, 1 + 2 * n = 2 * m -> False.
intros.
omega.
Qed.

4章では紹介しなかった整数についても omega は作用します。

証明に慣れてきて自明なことを示すのが億劫になってきたらこれらのタクティクを使うと良いでしょう。

タクティクのまとめ

4章でもいくつか新しいタクティクが登場したので、まとめて表にします。

exists x	サブゴールが "exists a, 〜" のとき a として x を与える
constructor	現在のサブゴールに適用できる型構成子を apply する
trivial	イコールの証明に特化した自動証明タクティク
auto with arith, omega	自然数の証明に特化した自動証明タクティク

既存の定理の探し方

前述したThe Coq Standard Libraryで標準ライブラリにある定理を見れますが、「こういう定理がほしい」というときに端から探していくのは面倒です。Coq には定理を探すために便利なコマンドがいくつかあります。

たとえば自然数 n m p に関して、"n * (m + p) = n * m + n * p" という定理を探したいとします。そのときは Arith モジュールを読み込ませた状態で、Command Pane で

SearchPattern (左のテキストボックス)   (_ * (_ + _) = _ * _ + _ * _) (右のテキストボックス)

と打ってみてください。Ok を選択すると結果に

Result for command SearchPattern (_ * (_ + _) = _ * _ + _ * _) . :
mult_plus_distr_l: forall n m p : nat, n * (m + p) = n * m + n * p

と表示されます。これで n * (m + p) = n * m + n * p という定理は mult_plus_distr_l という名前で利用できると分かりました。

このように SearchPattern は、探したい定理の変数の部分を "_" で置き変えた式を渡せばそれに合う定理を探してくれます。

他にも、ある関数を使った定理を探したいときに便利な SearchAbout というコマンドがあります。たとえば関数 seq を使った定理を探したいときは、List モジュールを読み込ませた状態で Command Pane に

SearchAbout (左のテキストボックス)   seq (右のテキストボックス)

と打てば、結果に

Result for command SearchAbout seq . :
seq_length: forall len start : nat, length (seq start len) = len
seq_nth:
  forall len start n d : nat, n < len -> nth n (seq start len) d = start + n
seq_shift: forall len start : nat, map S (seq start len) = seq (S start) len

と出ます。seq に関する定理として seq_length、seq_nth、seq_shift という定理があることが分かりました。

標準ライブラリにある定理をどんどん使って証明していきたいときは、これらのコマンドを使ってみると良いでしょう。

前回の答え

問題はこうでした。

問6. rev_involutive : forall (A : Type)(l : list A), rev (rev l) = l

問7. fold_right_app : forall (A B : Type)(f : A -> B -> B)(l l' : list A)(i : B),
      fold_right f i (l ++ l') = fold_right f (fold_right f i l') l

下に答えの一例を書きます。

Theorem rev_involute : forall (A : Type)(l : list A), rev (rev l) = l.
intros.
induction l.
 reflexivity.

 simpl.
 rewrite rev_app_distr.
 simpl.
 f_equal.
 apply IHl.
Qed.

Theorem fold_right_app : forall (A B : Type)(f : B -> A -> A)(l l' : list B)(i : A),
      fold_right f i (l ++ l') = fold_right f (fold_right f i l') l.
intros.
induction l.
 reflexivity.

 simpl.
 f_equal.
 apply IHl.
Qed.

練習問題

次の章を書くのは夏休みで、練習問題を出しても答えが出るまでの期間が長くなってしまうので今回は練習問題は出しません。

それでも何か証明しておきたいという方は、Arith モジュールにある定理、特に今回証明せずに使った定理（lt_trans、lt_n_Sn、lt_n_O、lt_S_n)を自分で証明してみると良いでしょう。