自然数とリスト: exists (3.6)
ここまで forall, ->, and, or, not のCoqでの使い方を見ました。Wikipediaの一階述語論理のページなどを見てみると、もう一種類、この手の論理結合子があります。∃（存在する）。Coq では、exists と書きます。
Theorem even_or_odd: forall (n:nat), exists m, (n=2*m \/ n=2*m+1). Proof. induction n.
「どんな自然数 n に対しても、自然数 m が存在して、(n=2*m \/ n=2*m+1) を満たす」。こういう「これこれこういう値が存在します」という主張の定理を書くために使います。
証明してみましょう。帰納法でやります。induction n。
0の場合とそれ以外の場合にゴールが分かれますが、まずは0の方から。nを0に置き換えた
------------------------------- exists m:nat, 0=2*m \/ 0=2*m+1
これを証明しないといけません。どうしましょう。existの正体を見てみると Coq.Init.Logic.ex:
(* Remark: exists x, Q denotes ex (fun x => Q) ... *) Inductive ex (A:Type) (P:A -> Prop) : Prop := ex_intro : forall x:A, P x -> ex (A:=A) P.
これも Inductive な命題です。exists x, P を証明するための公理は「"具体的な値 x" と "P x の証明" があれば、ex P が証明できる」という ex_intro。要するに、「Pであるようなxが存在する」を証明するには、具体的にそのxの値を人間が思いついて、Coqさんに教えてあげないといけません。
今回の場合、0=2*m \/ 0=2*m+1 を満たすような m は… m=0 とすれば成り立ってますね。これを Coq に教える tactic は、命題の記述と同じなのでちょっとややこしいですが、exists です。
exists 0.
これで、ゴールが 0=2*0 \/ 0=2*0+1 に変わります。あとは簡単。
left. simpl. reflexivity.
exists 0. の代わりに、Inductiveなゴールの証明の仕方の基本通り、"apply コンストラクタ" で書くこともできます: apply (ex_intro _ 0). が、やや面倒なのでexists tacticを使うのがよいと思います。
帰納法のもう一つのケースはこちら。
n : nat IHn : exists m : nat, n = 2 * m \/ n = 2 * m + 1 -------------------------------------------------- exists m : nat, S n = 2 * m \/ S n = 2 * m + 1
今度は仮定の方にもexistsが出てきますが、Inductiveなものが仮定にでききたらdestruct IHn. こう変わります。
n : nat x : nat H : n = 2 * x \/ n = 2 * x + 1 -------------------------------------------------- exists m : nat, S n = 2 * m \/ S n = 2 * m + 1
「ほにゃららな自然数 m が存在する」という仮定を、「自然数 x がある」「x はほにゃららを満たす」と分解してくれます。
仮定 H がまだ \/ の形なのでさらに分解 destruct H. すると、ゴールが２つに分裂して、１つめはこう。
H : n = 2 * x -------------------------------------------------- exists m : nat, S n = 2 * m \/ S n = 2 * m + 1
さて、n=2*x という仮定の下で、m をどうすれば S n = 2 * m \/ S n = 2 * m + 1 が成り立つようにできるか。ここはうんうん唸って考えましょう。m=x とすれば、∨の右側が成り立ちます。
exists x. right. omega.
もう一つのゴールは
H : n = 2 * x + 1 -------------------------------------------------- exists m : nat, S n = 2 * m \/ S n = 2 * m + 1
こうですが、今度は、m=x+1 とすると、左が成り立ちます。
exists (x+1). left. omega. Qed.
まとめ。
- exists e.
- exists x, P という形のゴールを示すときに、x=e とすれば示せますよ！と具体的な値をCoqさんに教える方向で証明する。
たぶん、Coqを使った証明で一番直接的に難しいのは、exists の証明です。これを証明するには、具体的にどの値を当てはめれば成り立つのか、完全に人間が考えてあげないといけません。今回だと、こっちの場合はm=xで行ける、こっちだとm=x+1…と言った具合に。数学の教科書などでは「十分大きな x を取れば P x が成り立つから exists x, P x」のような言い方をしたりしますが、こういう時でも、十分大きい x とは具体的にいくつなのか、100なのか65536なのか無量大数なのか、中身が実際に証明できる大きさを明確に書く必要があります。
などは、直感的には対して難しくない定理なはずなんですが、この難しさのせいで結構な難問になってるように思います。
適度な練習問題としては、さきほども紹介しましたが、
などなど。
Setバージョン
前回、A∨B には、よく似た意味の {A}+{B} というものがある、という紹介をしました。違いは、前者が Prop で後者が Set なことですが、証明の仕方はだいたい同じです。exists x, P にも同じ関係の {x | P} という Set バージョンがあります（Coq.Init.Specif.sig）。
などに登場します。この問題の
Definition tails {A:Set} (ys: list A) : {xss | all_suffixes xss ys}.は、だいたい
Theorem tails: forall (A:Set) (ys: list A), exists xss, all_suffixes xss ys.
と同じ意味です。証明も全く同じく、exists と destruct でできます。違いは、{_}+{_} の場合と同じく、「ゴールがSetのときはPropをdestructできない」という制約のみ。この制約の意味するところについては、次回ご紹介したいと思います。
