ひとり勉強会 RSSフィード

2010-09-19

Coqの入門記事を書く会 (3)

| Coqの入門記事を書く会 (3)を含むブックマーク

このペースだと、なかなかCoqの一番面白いところ(とわたしが思うところ)に行き着かないので、今回は全力ですっ飛ばして、必要な細かい話を全部片付けちゃおうと思います。次回が面白くなるはずです。今回は、主に、自然数やリストにまつわる証明の巻。

自然数とリスト: Inductive (3.1)

| 自然数とリスト: 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については後で。

f:id:hzkr:20100917144845p:image

さて、続きは…色々なやり方があります。ここで紹介するのはあくまで一例ですので、皆様もっと綺麗な証明を探してみて下さい。

仮定の所に 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個のゴールに変える

仮定などに "H: False" があったらいきなりこれでゴールが0個になるので証明完了します。(練習問題: False @ AnarchyProof

今回の例は "0=0 -> False" なんて仮定は成り立ちませんよ!とcontradictionしたので、証明すべき命題は 0=0 です。

 reflexivity.

そりゃ当たり前に = ですよね、とCoqさんに伝えます。イコールに関するtacticは以下の4種類です。

reflexivity.
e = e の形のゴールを証明
symmetry.
e1 = e2 というゴールを e2 = e1 に変える
symmetry in H.
e1 = e2 という仮定Hを e2 = e1 に変える
transitivity e3.
e1 = e2 というゴールを e1 = e3 と e3 = e2 の2つに変える
discriminate H
S x = O や、nil = cons x y のような、「違うコンストラクタで作ったデータが等しいと主張するありえない仮定」H があったら、それは無理ですよ、とCoqさんに伝えて証明完了

自然数とリスト: rewriteなど (3.2)

| 自然数とリスト: rewriteなど (3.2)を含むブックマーク

x=0の場合は終わったので、残ったゴールはこれです。

-------------------------
S x < S x + S x

これを証明するには…なにか、このくらいはさっきImportしたArith標準ライブラリで証明されていないでしょうか。CoqIDEでは

SearchAbout (_ < _ + _).

と打ち込むか、F2キーを押して (_ < _ + _) を検索すると…

f:id:hzkr:20100917153953p:image

「(_ < _ + _) という形のゴールに apply できそうなライブラリ定理の一覧」が表示できます。便利です。

表示された一覧の中に、わたしが見た限りでは直接使えそうなものはなかったのですが、近い物がありました。

plus_lt_compat_l : forall n m p: nat, n<m -> p+n < p+m

これ。p+n < p+m というのは S x < S x + S x の形にはなっていませんが、これを使えば "S x + 0 < S x + S x" なら証明できそう。"S x" と "S x + 0" は等しいので、これが示せれば十分ですよね。

十分ではありません。まず「"S x" と "S x + 0" は等しい」から証明してあげないとCoqさんは納得してくれません。納得させます。

 assert (S x = S x + 0).

初回にやった assert (X:=t) というtacticは、tという証明を書いて、その型の命題を仮定に追加するものでした。今回の assert (命題) は、「(命題)が成り立つので仮定に足してくれ!証明は今からやる!」とCoqさんに伝えるものです。

assertすると、メインの証明はいったん脇に置いておいて、assertされた命題の証明モードに入ります。ゼロを足しても値は等しい、というのは流石に標準の定理にあって、SearchAbout (_ = _ + 0). するとすぐ見つかりますので、それをapplyすれば証明完了。

 apply plus_n_O.

証明が1行で書ける場合は

 assert (S x = S x + 0) by apply plus_n_O.

と assert 〜 by でまとめて書いちゃうこともできます。

assert P.
メインの証明のことは一端忘れて、P を証明するモードに入る。終わったら、メインの証明のなかで P を仮定として使えるようになる
assert P by tac.
Pの証明が1行で書ける場合。Pを仮定に追加。
cut P.
assertと順番が逆になったもの。ゴールが "P->今のゴール" に変わる。ただし、それが終わった後にPの証明をしないといけない。

assertで脇道にそれましたが、無事に仮定が増えて、こうなっているはずです。

H0: S x = S x + 0
-------------------------
S x < S x + S x

ここで、「"S x" は "S x + 0" に等しいとわかっているんだから、ゴールにある "S x" は "S x + 0" に書き換えてよ!」とCoqさんに伝えるtacticが、rewrite。

 rewrite H0 at 1.

"at 1" は"1個目の" S xを書き換えてね、の意味です。これを指定しないとゴールが(S x + 0) < (S x + 0) + (S x + 0) に全部変わってしまって困ります。"at 1" なら

-------------------------
S x + 0 < S x + S x

狙い通りにこの形になってくれるので、使いたかったライブラリ定理 plus_lt_compat_l : forall n m p: nat, n<m -> p+n < p+m が使えます。

 apply plus_lt_compat_l.

ゴールが 0 < S x に変わりますが、SearchAbout (0 < S _). で、ピッタリの定理が見つかります。

 apply lt_O_Sn.
Qed.

まとめ。

rewrite H (at p1 p2 ....)
e1 = e2 の形の仮定 H があるときに、ゴールの中のe1をe2に書き換え。at ... があるときは、指定した番号のe1のみを書き換え。
rewrite <-H.
e1 = e2 の仮定 H を使って、逆向きに、e2をe1に書き換え
rewrite (<-)H in H1.
ゴールじゃなくて別の仮定H1の中を書き換え

今回は使いませんでしたが、assert + rewrite は非常によく使うので、replace、という複合tacticも用意されています。

replace e1 with e2.
まず、e1=e2を証明するモードに入る。証明できたらゴールの中のe1をe2に書き換え。
replace e1 with e2 by tac.
tac 1行でe1=e2を証明。さらに、ゴールの中のe1をe2に書き換え。

残念ながら replace には "at" 指定がないので、今回は使いませんでした。atが要らないときはreplaceがおすすめです。

自然数とリスト: 自動証明 (3.3)

| 自然数とリスト: 自動証明 (3.3)を含むブックマーク

Coqさんは非常に賢いので、実は、今回くらいの証明は自動でやってくれます。

f:id:hzkr:20100917153954p:image

Proof.
 intros.
 omega.
Qed.

omega はプレスバーガー算術という美味しそうな名前の理論の簡易全自動ソルバーで、整数に関する等式や不等式のかなりの部分を自動的に証明してくれます。

omega
整数/自然数の、足し算引き算や定数倍に関する、等式や不等式を自動証明。変数と変数の掛け算があると使えない。
ring
足し算引き算掛け算に関する等式を、単に式を整理することで自動証明。不等式は使えない。
field
足し算引き算掛け算割り算に関する等式を、単に式を整理することで自動証明。不等式は使えない。
fourier
実数に関する線形不等式の自動証明

これらがないと、数式の証明はひたすらSearchAboutとrewriteを繰り返す退屈な作業になってしまうことが多いので、覚えておかないと大変です。数式の証明で困ったらomega! この入門記事シリーズでも、今後はomega/ring/fieldで証明できるところは使っていきます。

自然数とリスト: 帰納法 (3.4)

| 自然数とリスト: 帰納法 (3.4)を含むブックマーク

別の問題を証明してみましょう。Anarchy Proof から Sum of natural numbers をお借りします。ring を使わないでやってみよう、という問題ですが、気にせずringを使って解いちゃいますので、ネタバレにはなっていないはず…。

Require Import Arith Omega.

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

Theorem Sum_of_nat:
 forall (n: nat),  2 * sum n = n * (n + 1).
Proof.
 intros.
 destruct n.

まずは、ここまでで解説したtacticを使って挑戦してみます。実はそれではうまくいかないのですが、しばらくおつきあい下さい。

1つめのゴール、n=0の場合の 2*sum 0=0*(0+1)は簡単です。

 simpl.
 reflexivity.

両辺計算すると 0 になるので、0=0 は reflexivity で。simpl は計算できるところは計算して下さい、というtacticです。計算させるtacticはsimplの他にhnf、compute、cbv、lazy、vm_computeなどがありますが詳細はリファレンスなどをご覧下さい。そこそこ適当に計算するのがsimpl、本気でできる限り計算するのがcbv、くらいの感覚で。ringとfieldの性質を使って式を整理する、ring_simplify、field_simplify というのもあります。

もう一つのゴールが問題です。simpl すると…まだごちゃごちゃしているので、さらに ring_simplify すると

 simpl.
 ring_simplify.

n:nat
-----------------------------------
2*n + 2*sum n + 2  = n*n + 3*n + 2

こうなります。これは、もし 2*sum n = n*n + n が成り立てば、ゴールの中の 2*sum n を rewrite すれば左辺と右辺が同じになるのですが、それって、今証明しようとしている式ほとんどそのまんまです。堂々巡り。

こういう時に使うのが、数学的帰納法です。Coqでは、Inductiveな物をdestructする代わりに、inductionというtacticで分解します。

Theorem Sum_of_nat:
 forall (n: nat),  2 * sum n = n * (n + 1).
Proof.
 intros.
 induction n. (* destruct n の代わりに! *)

 simpl.
 reflexivity.

 simpl.
 ring_simplify.

さっきと同じ証明をすると、今度は…

f:id:hzkr:20100917231117p:image

仮定に IHn : 2 * sum n = n * (n+1) という便利な等式が入っています!

 rewrite IHn.
 ring.
Qed.

証明完了。

数学的帰納法についておさらいしておくと、自然数の場合、

  • n=0 で命題(たとえば 2 * sum 0 = 0 * (0 + 1))が成り立つ
  • nで成り立つなら、S n でも(2 * sum (S n) = S n * (S n + 1))成り立つ

この二つが証明できたなら、その命題はすべての自然数 n で成り立つ!という証明方法です。一方で destruct での証明は

  • n=0 で命題(たとえば 0<>0 -> 0<0+0)が成り立つ
  • S n でも(0<>S n -> S n < S n + S n)成り立つ

の二つが証明できたら、すべての自然数 n で成り立つ、という証明です。帰納法の方が、"nで成り立つなら" という仮定を使える分、強力なわけですね。

帰納法の考え方は、自然数だけではなく、再帰的に定義された(つまり、S : nat -> nat のようにコンストラクタが作りたいものと同じ型を引数にとる)Inductive すべてに一般化できます。リストの場合

  • xs=nil で成り立つ
  • xs で成り立つなら、cons x xs でも成り立つ

が言えれば、その命題は全てのリストで成り立つことが証明できます。

ここまでの総まとめの練習問題としては

などいかかでしょうか…と思ったら、まだ exists の説明してないですね。これはあとで。(3.6)でやります。

自然数とリスト: 帰納法の色々 (3.5)

| 自然数とリスト: 帰納法の色々 (3.5)を含むブックマーク

Coqでの帰納法の仕組みについて、ちょっとだけ。CoqIDE に

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

と打ち込んで nat を再定義してみてください。

nat is defined
nat_rect is defined
nat_ind is defined
nat_rec is defined

こう右下に表示されると思います。実は、nat を定義すると同時に、裏でひっそりと3つの公理がCoqによって自動で定義されているのです。これが帰納法の正体です。

Print nat_ind.

こんな命題です。

nat_ind =
fun P : nat -> Prop => nat_rect P
     : forall P : nat -> Prop,
       P O -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
  • 自然数に関するどんな命題 P : nat -> Prop も、
    • 0 で成り立つ P O 証明
    • n で成り立 P n てば、S n でも成り立つ P (S n) という証明
    • の二つがあるなら forall n : nat, P n すべての n で成り立つ

と書いてあります。まさに帰納法です。induction n. という tactic は、基本的には、実は apply nat_ind. しているだけだったりします(実際はゴールに n が複数あるときの扱いなど、induction n の方が便利になるように工夫が入っていますけど)。

Require Import List.
Print list_ind.

すると list の帰納法も見られます。


False_ind

and や or など再帰的じゃないInductiveにも、一応機械的に帰納法の公理が定義されているのですが、あんまり使い道はありません。唯一使えるのが False のために自動定義される False_ind で

Print False_ind.

False_ind = 略 : forall P : Prop, False -> P

どんな命題 P も、「False が成り立っているなどというあり得ない事態であれば、成り立つ」。これを使うと apply False_ind. で、どんなゴールも False に変えられます。仮定がそもそもおかしいときに「仮定がそもそもおかしいぞ」とCoqさんに伝えるのに使います。apply False_ind してから普通にFalseを証明してしまえばよし。さきほど紹介した condtraction H. があれば普通は用が足りますが、仮定にそのまま1個でバシッと矛盾しているものを作るのが難しいときには、「Falseを証明する」方が楽だったりします。


カリーハワード

さて、カリーハワード対応の時間です。「帰納法」とは、プログラミングで言うと、何にあたるのでしょうか。

list_ind =
fun (A : Type) (P : list A -> Prop) => list_rect P
     : forall (A : Type) (P : list A -> Prop),
       P nil ->
       (forall (a : A) (l : list A), P l -> P (a :: l)) ->
       forall l : list A, P l

答えは、foldr です。Haskell には"依存型"がないので、"P nil" や "P l" の部分が全部同じ型 b になって簡単化してますが、やっていることは同じで

  • nil の場合の結果
  • cons x xs の場合、x と "xs を foldr して結果" から計算結果を求めて返す関数

の二つから、任意のリストを受け取ってリスト全体を計算して返す関数を作るのがfoldrであります。


整礎帰納法

数学的帰納法」って、こうじゃなかったけ?と記憶されている方もいらっしゃるかもしれません。

  • nより小さい全ての数で成り立つなら、nでも成り立つ

が言えれば、「全てのnで成り立つ」と言える。

これは 整礎帰納法 と呼ばれる証明方法で、普通の帰納法よりさらに強力なテクニックです。Sqrt 2 @ Anarchy Proof などではたぶんこれが使いたくなると思います。

Coqでは自然数に関する整礎帰納法はCoq.Arith.Wf_natというモジュールで定義されていて、

Requirt Import Wf_nat.
Print lt_wf_ind.

lt_wf_ind =
 中略
     : forall (n : nat) (P : nat -> Prop),
       (forall n0 : nat,
        (forall m : nat, m < n0 -> P m) -> P n0) ->
       P n

こうです。読んで字のごとしです。使うには直接

 apply lt_wf_ind.

するか、induction 〜 using という tactic を使います。帰納法っぽいtacticを使いやすくapplyしてくれるものです。

 induction n using lt_wf_ind.

ある条件を満たす順序関係があれば、自然数以外でも整礎帰納法は使えます。詳しくは Coq.Init.Wf

introしすぎにご用心

さっきの例題を、ちょっとだけ形をいじって

Require Import Arith Omega.

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

Theorem Sum_of_nat:
 forall (n m: nat),
   m = 2 * sum n -> m = n*(n+1).
Proof.

こうしたものを考えます。

 intros.
 induction n.

こうすると、n=0 の場合まではなんとかなる(rewrite H. simpl. reflexivity.)のですが、S n の場合が

H : m = 2 * sum (S n)
IHn : m = 2 * sum n -> m = n * (n + 1)
---------------------------------------
m = S n * (S n + 1)

帰納法の仮定 IHn が、何かちょっと困った形になってしまいます。これは、全部 intros してから induction すると、「intros で仮定に押し上げて m を固定してしまった状態で帰納法を回す」ことになってしまうせい。正しくは

 forall (m:nat), m=2*sum n -> m = n*(n+1)

というように、m がforallされた命題が、全てのnで成り立つことを証明しないとうまくいきません。

ということで、intros ではなく、intro で n だけ剥がしてから induction しましょう。(実は induction tactic は便利に作られていて、なにもintroせずにinduction nと書いたら自動で n まででintroを止めてinducitonを始めてくれるので、それでも可です。)

Proof.
 intro n.
 induction n.

 (以下は練習問題)

「forall や -> を見たらとりあえず intros 」という方針をこれまで推奨してきましたが、induction を使う前に限っては、必要最小限の intro で 止めておく方がうまくいくことが多いようです。

実は、もっといじわるなバージョンも考えられます。

Theorem Sum_of_nat:
 forall (m n: nat),
   m = 2 * sum n -> m = n*(n+1).
Proof.

今度は、m の方が n より先にあるため、n だけを intro しようとしても無理で、intros m n. のように、必ず m も仮定に引っ張り上げてしまいます。こういう時には、仕方なく intros してから、"generalize" という tactic で、仮定を forall に戻します。

 intros m n.
 generalize m.
 induction n.

あとはさっきと同様。

自然数とリスト: exists (3.6)

| 自然数とリスト: 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。

f:id:hzkr:20100919001520p:image

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. すると、ゴールが2つに分裂して、1つめはこう。

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さんに教える方向で証明する。

仮定にexistsが出てきた場合は、destructが使えます。


たぶん、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できない」という制約のみ。この制約の意味するところについては、次回ご紹介したいと思います。

自然数とリスト: まとめ (3.7)

| 自然数とリスト: まとめ (3.7)を含むブックマーク

駆け足でいろいろ紹介しました。

  • SearchAbout でライブラリを検索
  • 自然数やリストはInductiveなデータ
  • = に関する証明 reflexivity, symmetry, transitivity, discriminate
  • = を使った書き換え rewrite, replace
  • 計算をすすめる simpl, cbv, ...
  • 自動証明 omega, ring, field, ring_simplify, field_simplify
  • 帰納法 induction
    • intro しすぎにご用心。generalize
    • 整礎帰納法
  • exists

当初の予定では3回くらいにわけるつもりだったんですが、めんどくさくなったので一気に書いてしまうことにしました。駆け足すぎてよくわからなくなってしまってると思いますが、他の入門記事やチュートリアルなどと併用してください(いい加減になってきた…)。ではでは。

追伸

そういえば、このシリーズでは intros や destruct では自分で仮定に名前をつけることはせずに、Coqの自動生成にまかせちゃっているんですが、これって、コーディングスタイルとしては良くないのかもしれません。ということにさっき気づきました。H0 やら H1 やらではよく分からないですよね。本当は、ちゃんと名前をつけて intros 等した方がいいと思います!

2010-09-14

Coqの入門記事を書く会 (2)

|  Coqの入門記事を書く会 (2)を含むブックマーク

第2回です。前回は「forall」と「->」の扱い方でした。今回は、「ならば (->)」以外の定番の論理演算、「and」「or」「not」のお話です。

実は、Coq の本当に言語組み込みの命題構成子は forall と -> だけで、「and」「or」「not」は、Coq使いなら自分で同じ機能のものを簡単に作れてしまう「ユーザー定義命題」です(もちろん、共通のものがないと不便なので標準ライブラリで真っ先に定義されてますけど)。逆に言うと、もっと本格的なCoqコードで出てくる複雑そうな命題も、全部、「and」「or」「not」と同じユーザー定義型の仕組みで定義されてますので、「and」「or」「not」の扱いさえマスターすれば、他のどんなユーザー定義の命題の証明も同じ道具で書けちゃいますよ。

andとorとnot: ド・モルガン (2.1)

|  andとorとnot: ド・モルガン (2.1)を含むブックマーク

andとorとnotを分けて説明するのが面倒くさいので、いきなり全部入りの定理を例にしましょう。今回のお題はド・モルガンの法則です。

Lemma De_Morgan:
  forall A B: Prop, ~(A \/ B) -> (~A /\ ~B).
Proof.

「(AまたはB)ではない、ならば、(Aではない、かつ、Bではない)」です。∨ が「または」で、∧ が「かつ」で、「~」が否定の「ではない」です。∨と∧はバックスラッシュを使って書くので、フォント環境によっては円記号に見えてしまっているかも。その場合はすみません、心眼で¥を\と読んで下さい。

そういえば前回は Theorem Modus_ponens と "Theorem" (定理) で書き始めましたが、今回は "Lemma" (補題) です。Coq 的には違いは何もありません。趣味の問題です。"Proposition" (命題) や "Corollary" (系)、"Fact"、"Remark" など色々ありますが趣味で使い分けて下さい。


notの扱い

さて、まず、否定の ~A は、「A -> False」の省略形です。リファレンスから引用します。Coq.Init.Logic.not:

Definition not (A:Prop) := A -> False.
Notation "~ x" := (not x) : type_scope.

「Aではない」とはすなわち、「Aならば偽」「Aだと仮定すると矛盾が生じる」である。これがCoqでの、そしてCoqがベースにしている論理体系での「~」の定義であります。False の定義はあとで解説しますが、とりあえず単にそういう名前の命題と思っておいて下さい。

「ならば」の扱いなら前回やって慣れてますので、安心ですね。「"not" なんて見慣れない単語を使わないで、全部 "->" の言葉でしゃべってください」と Coq さんに伝えましょう。

  unfold not.

"unfold" tactic を使います。単に、Definition ... := で定義された定義をインライン展開するだけのtacticです。

f:id:hzkr:20100914112259p:image

ついでに intros. しておきました。

andの扱い

示さないといけないゴールの形が、(A→False)∧(B→False) になりました。この ∧ とは何者かというと… Coq.Init.Logic.and:

Inductive and (A B:Prop) : Prop :=
  conj : A -> B -> A /\ B

where "A /\ B" := (and A B) : type_scope.

こんな物体です。なにやら複雑ですが、とりあえず最後の1行は「"A∧B" という中置演算みたいな記法は、(and A B) の略記です」と言ってるだけです。本体は上2行。"Inductive" 宣言を使って、二つのことを宣言しています。

  • "A∧B" という新種の命題をこれから使います!
  • この "A∧B" の「公理」は A -> B -> A∧B です!

"A∧B"が成り立つのは、Aが成り立って、しかもBが成り立っているとき、その時に限ります。つまり "Aならば(Bならば(A∧B))" が無条件で成立する…そういう∧という命題を使って色々書いたり証明したりするんでよろしくお願いします、とCoqさんに伝えるのがInductive宣言です。

さてさて、定義の話はいいから、証明のやり方はどうするのでしょうか。

実は、もう我々は証明のしかたを知っています。

  • ゴールは hoge ∧ fuga という形です
  • conj : hoge -> fuga -> hoge ∧ fuga という公理があります

公理はいつでも無条件に使えるので、仮定と同じように、apply することができて…

 apply conj.

"(A->False) ∧ (B->False)" を示すためには、A->False を示して、B->False を示せば、後は conj を使えば証明できます。そういう感じで証明しますんでよろしく、とCoqさんに伝えると

f:id:hzkr:20100914112300p:image

二つのゴールができました。

orの扱い

続いて、一つ目のゴールは "A->False" です。ゴールが "->" の形なので、何も考えず

  intros.

するとゴールが "False" になりますが、仮定を眺めると False を作れるのは "H: A∨B->False" しかないので、これをapplyしておきます。

 apply H.

f:id:hzkr:20100914112301p:image

ゴールは "A∨B" になりました。さてどうしましょう。定義を見ると Coq.Init.Logic.or:

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

where "A \/ B" := (or A B) : type_scope.

今度は、公理が2つあります。

  • or_introl: "A"が成り立つなら、"AまたはB"が成り立つ
  • or_intror: "B"が成り立つなら、"AまたはB"が成り立つ

まあor(または)の意味として納得の行く定義です。

というわけで、ゴールを証明するには "apply or_introl." か "apply or_intror." を使えばよいのですが…どっちが正解でしょうか?

  • ゴール A∨B に、or_introl: A->(A∨B) を apply すると、新ゴールは A になります
  • ゴール A∨B に、or_intror: B->(A∨B) を apply すると、新ゴールは B になります

どっちなら続きを証明できるかというと、今回は仮定に "H0: A" があるので、新ゴール A なら"exact H0."で証明完了です。というわけで、or_introl の方を使います。

  apply or_introl.
  exact H0.

こういう風に、or のような分岐があると「どっちに行ったら証明できるか」をよく考えて選んでやる必要があります。証明の完全な機械化は難しくて、Coqのように人間が考えて証明記述してやるシステムが必要な理由の一端は、ここにあります。頑張って人類の発想力を発揮しましょう。

apply conj でできたもう一つのゴール "B->False" も、同じように証明できます。こっちは or_intror の方を使います。

  intros.
  apply H.
  apply or_intror.
  exact H0.
Qed.

証明完了!

andとorとnot: カリーハワード (2.2)

|  andとorとnot: カリーハワード (2.2)を含むブックマーク

プログラミング言語としてみると」さっきの証明は何をやっていたことになるんでしょう。

"Inductive"は、ユーザー定義の新しい命題を定義するのでした。そして、命題=型です。つまり、ユーザー定義の新しい型を作る機能が対応します。Haskell だと "data" ですね。

data And a b = 
 Conj a b

data Or a b =
   OrIntroL a
 | OrIntroR b

Inductiveによるandとorの定義をHaskellで書き直すと、↑こうなります。公理とは、要するにコンストラクタです。はい。

class And<A,B> {
  public And(A a, B b) { ... }
}
class Or<A,B> {
  public Or(A a) { ... }
  public Or(B b) { ... }
}

Javaで書くとこんな感じです。Andは、2引数のコンストラクタを1つ持つ型です。Orは、1引数のコンストラクタが2つ。どっちを使っても作れますが、どっちかを使わないと作れません。

ちなみに False は、Coq.init.Logic.False:

Inductive False : Prop :=.

公理が一つもない…つまり証明する手段が1つも用意されていない命題、それがFalse、という定義です。Haskellでも

{-# OPTIONS_GHC -XEmptyDataDecls #-}
data False

こう、こういう変な型を定義するには追加オプションが要りますけど、作れます。

さて、あらためて、ド・モルガンの証明とはなんだったかというと…

de_morgan :: (Or a b -> False) -> And (a -> False) (b -> False)

Haskellで「この型を持つ値を作ってね!なんでもいいから!」と言われたら、どうしますか?

de_morgan f =
 Conj (\x -> f (OrIntroL x)) (\y -> f (OrIntroR y))

たとえば、こんな風に書けますね。これが、さっきCoqで作った証明です。

andとorとnot: コンストラクタ (2.3)

|  andとorとnot: コンストラクタ (2.3)を含むブックマーク

ここまでの内容をまとめると、

  • ゴールが A∧B の形なら ∧の公理(コンストラクタ)を使う
    • つまり apply conj.
  • ゴールが A∨B の形なら ∨の公理(コンストラクタ)を使う
    • つまり apply or_introl.
    • または apply or_intror.
    • どっちがいいかは人間が頑張って考える。

です。

これはこれでいいんですけど、「∧のコンストラクタの名前ってなんだったけ…」「∨のコンストラクタって…」って毎回思い出したり、リファレンス引いたりするのは面倒ですよね。

この辺は、自動化してくれる tactic があります。

Lemma De_Morgan:
  forall A B: Prop, ~(A \/ B) -> (~A /\ ~B).
Proof.
  unfold not.
  intros.
  constructor.  (* apply conj. の代わり *)

constructor. と打つと、名前忘れたけどコンストラクタ使うぜ!という意味になって、Coqさんが上手いことやってくれます。

orの場合はコンストラクタが2つあるので…

  intros.
  apply H.
  constructor 1. (* apply or_introl. の代わり *)
  exact H0.

  intros.
  apply H.
  constructor 2. (* apply or_intror. の代わり *)
  exact H0.
Qed.

どっちのコンストラクタなのか、「1番目のやつ!」「2番目のやつ!」と指定してあげましょう。番号指定しないと、コンストラクタを先頭から順にapplyしてみて成功した最初の結果を返すみたいです。

実は、さらにさらに、短く書く略記tacticも用意されています。

f:id:hzkr:20100914112302p:image

constructor.
ゴール命題の、コンストラクタをapply。(複数ある場合は最初にマッチした物)
constructor n.
ゴール命題の、n番目のコンストラクタをapply
split.
1つしかコンストラクタがないゴールに。そのコンストラクタをapply
left.
丁度2つコンストラクタがあるゴールに。constructor 1 と同じ
right.
丁度2つコンストラクタがあるゴールに。constructor 2 と同じ

splitは「"A∧B"を証明」というゴールを「Aを証明」と「Bを証明」に分ける(split)感覚で、leftは「"A∨B"を証明」というゴールを「Aを証明」に左(left)だけ残して変える感覚ですかね。rightは右。constructorのただの別名なので、splitもleftもrightも、andやor以外にも使えます(かえって意味がわかりにくくなったりするかもしれませんが…)。

andとorとnot: デストラクト (2.4)

|  andとorとnot: デストラクト (2.4)を含むブックマーク

コンストラクタがあるならデストラクタはないんですか」

あるのです。これを語らなくては話が終わりません。コンストラクタの逆の話なので、例題も逆にしましょう。ド・モルガンの法則は逆向きにも成り立ちます。

Lemma De_Morgan2:
 forall A B: Prop, (~A /\ ~B) -> ~(A \/ B).
Proof.
 unfold not.
 intros.

とりあえず unfold と intros してみるのは良いとして…

f:id:hzkr:20100914112303p:image

次、どうしましょう。仮定にあるのは

  • H: (A->False)∧(B->False)
  • H0: A∨B

だけで、-> がないので、もう apply もできません。困った。

逆に考えるんだ。

  • 「∧を証明できるのは公理 conj: hoge→fuga→hoge∧fuga しか存在しない」
  • 既に仮定 H に「(A->False)∧(B->False)」がある
  • これは conj に「A->False」と「B->False」を渡して作ったとしか考えられない

なので、「(A->False)∧(B->False)」を仮定しても良いなら、同時に、「A->False」と「B->False」も既に成り立っていると仮定して良いでしょう!

Coq さんに伝えるのが、destruct という tactic です。

 destruct H.

仮定から∧が消えて

  • H: A->False
  • H1: B->False
  • H0: A∨B

こう分解されます。「A∧Bを仮定してCが証明できる」ことを示すには、「AとBを仮定してCが証明できる」ことを示せば十分、と仮定を分解するのがdestructです。

もう一個、仮定に、分解できそうな子がいますね。

  • 「∨を証明できるのはor_introlかor_introrのどちらかしかない」
  • 既に仮定に H0: A∨B がある。これは
    • 「or_introl に A を渡して作った」か
    • 「or_intror に B を渡して作った」のどっちかしかあり得ない。

どっちかわからないけど、両方の場合を考えてどっちもゴールが証明できたらOKじゃない?とCoqさんにお願い。

 destruct H0.

f:id:hzkr:20100914112304p:image

「A∨Bを仮定してCが証明できる」ことを示すには、「Aを仮定してCが証明できる」と「Bを仮定してCが証明できる」の二つのゴールを証明すればよいのです。というわけでゴールが2つにわかれます。

ここまで来れば簡単ですね。

 exact (H H0).
 exact (H1 H0).
Qed.

まとめると…

Inductiveでユーザー定義した命題の公理(conj や or_introl や or_intror)は、「それを使うとユーザー定義命題を証明できる」という意味と、「それ以外の方法では決して証明できない」という、2つの意味があります。前者の性質を使うのがコンストラクタによる証明で、後者を使うのがdestruct tacticによる証明です。

destruct H.
仮定Hの型TがInductiveで、そのコンストラクタが A->B->T、C->D->T、E->F->T、… だったら、「Hを仮定してゴールを示す」という状態を「AとBを仮定してゴールを示す」「CとDを仮定してゴールを示す」「EとFを仮定してゴールを示す」…に分解する
destruct H as [HA HB].
destruct H as [HA|HB].
destruct H as [HA [HB HC] ].
説明してませんでしたが、destructした時に新しく増える命題にはasで名前をつけることができます。andのようにゴールが分岐せず仮定が増える部分には[HA HB]と並べ、orのようにゴールが増える部分には[HA|HB]と並べます。ネストさせるとA∧B∧Cみたいなのを一気にdestructしたりできます。詳しくはリファレンスをどうぞ。
decompose [and or] H.
実はわたしは使ったこともちゃんと調べたこともないのですけど、賢く全部destructしつくしてくれる感じのtactic?
elim H
case H
destruct よりももっとプリミティブな操作です。destructすると「元々あった仮定を消して新しく分解後の仮定を追加」しますが、elim を使うと「元々の仮定は消さない。分解後の結果は過程に追加するのではなく、ゴールに->で追加」します。さらに、「分解した仮定Hが他の仮定の中に使われていた場合にそのHも書き換える」がdestructで書き換えないのがelim。まあなんだかややこしいのですが、要は、「destructはちょっとやり過ぎで困る」と思ったらelimに変えて試してみるといいかも…。

まあ、ややこしいことは気にせず仮定にInductiveなものがあったらとりあえずdestructしてみるという証明戦略は結構うまくいく気がします。

ややこしいことは気にせずといえば、カリーハワード対応脳の人には、destructのもっとずっとわかりやすい説明があります。要するにこれは、

Print De_Morgan2.

De_Morgan2 =
fun (A B : Prop) (H : (A -> False) /\ (B -> False)) (H0 : A \/ B) =>
match H with
| conj H1 H2 =>
    match H0 with
    | or_introl H3 => H1 H3
    | or_intror H3 => H2 H3
    end
end

パターンマッチなのです。

andとorとnot以外のInductive (2.5)

|  andとorとnot以外のInductive (2.5)を含むブックマーク

何度か繰り返しているように、andやorやFalseは、Coqに組み込みの摩訶不思議な何かではなく、ユーザー定義できる命題です。andやorに使える証明方法は、他のInductive命題にもそのまま使えます。試しに他に何か自作してみましょう。

こんなの考えてみました。

Inductive major (A B C:Prop) : Prop :=
| ab : A->B->major A B C
| bc : B->C->major A B C
| ca : C->A->major A B C.

AとBとCのうち、2個以上が成り立つなら成り立つ、多数決命題 major A B C を定義しました。例えば、こんな定理が成り立ちます。

Theorem majmaj:
 forall A B C: Prop,
   major A B C -> ~major (~A) (~B) (~C).
Proof.

とりあえず unfold not. して、intros. して…あとは仮定に major ばっかりになるので、Inductive な命題が仮定にあるときは…? 練習問題です(^^)。


他に重要な例としては、Anarchy Proof の問題でも時々でてきます(Prime is decidable など)が、{A}+{B} というのがあります。これの定義はCoq.Init.Specif.sumbool:

Inductive sumbool (A B:Prop) : Set :=
  | left : A -> {A} + {B}
  | right : B -> {A} + {B} 
 where "{ A } + { B }" := (sumbool A B) : type_scope.

コンストラクタの名前が違うだけで、ほとんど A∨B と同じです。実際、∨を{}+{}に変えた

Lemma De_Morgan3:
 forall A B: Prop,
  ({A}+{B}->False) -> ((A->False) /\ (B->False)).

でも

Lemma De_Morgan4:
 forall A B: Prop,
  ((A->False) /\ (B->False)) -> ({A}+{B}->False).

でも、全く同じに、"constructor" と "destruct" を使って証明できます。試してみて下さい。練習問題です(^^)。こんな風に、見たことのない新しい命題が現れても、どれもandやorと同じく、constructorとdestructで証明にとりかかれます。簡単ですね。


※ {A}+{B} に関しては、A∨B と唯一違うところは、∨の方は:Propと宣言されてましたが、{}+}{}の方は:Setと宣言されているところです。PropとSetの違いはそのうち多分説明するような気がしますが、とりあえず証明を考える際に問題となる違いは1点だけ。

  • ゴールが Set のときは、Prop の destruct はできない

この制約のせいで、"forall A B:Prop, {A}+{B} -> A\/ B" は証明できますが、"forall A B:Prop, A\/ B -> {A}+{B}" はできません。この形になってしまったときは、destructを使わずになんとか迂回して証明することになります。

andとorとnot: 次回予告 (2.6)

|  andとorとnot: 次回予告 (2.6)を含むブックマーク

もう今回の内容でInductiveの扱いは完璧…!

といいたいところなんですが、「再帰的なInductive」の証明テクニックの解説が実はまだ残っています。次は多分それについて書きたいなあと思っています。それかFalse周りの証明をさらにいろいろ。

CC0
To the extent possible under law, the person who associated CC0 with this work has waived all copyright and related or neighboring rights to this work.