自然数とリスト: Inductive (3.1)
前回、andやorなどの命題が"Inductive"で作られてることをご紹介しました。Coqでは、命題だけでなく、自然数やリストなどなど、普通のデータ型も、Inductiveで定義します。
例えば自然数は Coq.Init.Datatypes.nat
Inductive nat : Set := | O : nat | S : nat -> nat.
こう。O (大文字のオーです) は、0 (ゼロです) を表します。S n は「n の一つ後ろの数」を表します。S (S (S O))) は 3。（ただし、実際に大量に S を並べるのは大変なので、Coq のコードでは 100 や 200 と普通に書けば勝手に処理系がS S ... (S O)と解釈してくれます。実体は S S S ... なので、10000 とか大きい定数を書くと結構大変なことになりますが…）
リストは Coq.Lists.List.list:
Variable A : Type. Inductive list : Type := | nil : list | cons : A -> list -> list. Infix "::" := cons (at level 60, right associativity) : list_scope.
nil で空リストを作るか、cons で、リストに要素を一個足すか、どちらかの方法でリストは作れるし、その方法で作れるものだけがリストです。
さてさて、では早速、この辺りが登場する証明をやってみましょう。まずは簡単なものから。「x が 0 じゃない自然数なら、x+x は x より大きい」。
Require Import Arith Omega. Lemma double_is_big: forall (x:nat), x <> 0 -> x < x+x. Proof. intros.
1行目の Require Import ですが、Arith と Omega という二つの「ライブラリ」をこれから使います、とCoqさんに伝えています。どちらもCoqの標準ライブラリで、Arithには自然数に関する基本的な定理が大量に証明されて入っています。自然数の証明をする場合、とりあえずRequire Importしておくと良いと思います。Omegaについては後で。
さて、続きは…色々なやり方があります。ここで紹介するのはあくまで一例ですので、皆様もっと綺麗な証明を探してみて下さい。
仮定の所に x: nat とあります。仮定にInductiveなものがあわられたら、destructして分解してみる。これはandやorでなくても、命題じゃない、自然数のようなデータ型でも使えます。
destruct x.
natには二つコンストラクタがあったので、ゴールが2つに分かれます。Oで作ったnatの場合（つまりx=0の場合）と、Sで作ったnatの場合です、0の方は、こんな風になります。
H: 0 <> 0 -------------- 0 < 0 + 0
0 < 0+0 って成り立ってないので証明できなさそうな気がしますが、これは、仮定の方がおかしいのです。"H: 0<>0 ならば"…といわれても、そんなことはあり得ません！ということを証明したら、全体を証明したことになります。
そういえば説明し忘れましたが、x <> y は "~(x=y)" のシンタックスシュガーです。x=yではない。
unfold not in H.
すると "H: 0=0 -> False" に変わることで確認できます（注：確認だけなので、これはやってもやらなくても以下の証明には変化ありません）。unfold 〜 in で、ゴールの中だけではなく仮定の中もunfoldできます。
「仮定に成り立たない命題が入ってるぞ」ということをCoqに伝えるのは、contradictionというtacticです。
contradiction H.
- contradiction H.
- 仮定 H: A1->A2->...->An->False があったら、ゴールを、A1とA2と...とAnのn個のゴールに変える
今回の例は "0=0 -> False" なんて仮定は成り立ちませんよ！とcontradictionしたので、証明すべき命題は 0=0 です。
reflexivity.
そりゃ当たり前に = ですよね、とCoqさんに伝えます。イコールに関するtacticは以下の4種類です。
