定理証明系、はじめました

とりあえずCoqをインストールしていくつか証明を書いたのでそのメモ。
分かりやすい参考文献集


まずはCoqのインストール。Winならhttp://coq.inria.fr/downloadからダウンロード、Debian系OSならaptでcoqideをインストールする。

CoqIdeを起動すると、左側にファイルの編集画面、右側に実行結果などが表示される。まずはファイルに何か関数定義でも打ち込む。

Definition plus m n := m + n.

view raw define_function.coq hosted with ❤ by GitHub

画面上のボタン類から下向きの矢印を押すと、一行ずつ実行される。ショートカットはCtrl+Alt+Down(のはずが何故か効かない)

カリー＝ハワード同型対応より、命題は型として、証明はプログラムとして扱えるらしいけれども詳しい事はよく分かってない。
ここで簡単な証明、任意の命題A, Bに対し、A -> (A -> B) ->B を証明してみる。つまりこれを満たす関数を書く。

	Definition prop1: forall A B : Prop, A -> (A -> B) -> B :=
	fun A B x f => f x.

view raw easy_proof.coq hosted with ❤ by GitHub

forall A B : Prop, A -> (A -> B) -> Bとなるような関数を書けば良い。PropはA, Bの型。今回は無名関数の定義である fun を使う。
forallのA, Bも引数として取らなければいけないので、最初の引数は A B 、次にA型の値x、A -> B型の関数fを取って、fにxを適用すればBが帰ってくる。
関数が正しく定義出来ると、prop1 is definedのように表示される。

次にド・モルガンの定理の証明をしてみる。
先ほどのように簡単な証明だと関数を書けば終わるけれども、複雑な定理とかになってくるとそうもいかない。まずは証明する命題を示し、次にその命題をCoqに用意された様々なタクティクを利用して証明していく。タクティクについてはよく分かってないので上の参考文献集とかを適当に読んで下さい。おすすめはCoqの入門記事を書く会の記事。
まずは定理を示す。LemmmaとかTheoremとかを適当に選んで名前を付けたり、あるいは名前を付けずにGoalと書いてから命題をいきなり書くことも出来る。
次にapplyとかexactとかconstructorとか色々タクティクを使い倒して、目的の証明まで持っていく。
intros.はA->Bがゴールである時に、Aを前提にしてBをサブゴールにするタクティク。
applyは使える前提にA -> Bがあって、証明すべきゴールがBの時に、ゴールをAに変えるタクティク。
ド・モルガンの定理、forall P Q: Prop, ~(P\/Q) -> (~P/\~Q)の証明は次の通り。

	Theorem De_Morgen: forall P Q: Prop, ~(P\/Q) -> (~P/\~Q).
	Proof.
	unfold not.
	intros.
	split.
	intros.
	apply H.
	left.
	exact H0.
	intros.
	apply H.
	right.
	exact H0.
	Qed.
	Axiom EM: forall P: Prop, P\/~P.
	Theorem De_Morgen2: forall P Q:Prop, ~(P /\ Q) -> (~P \/ ~Q).
	Proof.
	assert (forall P: Prop, ~~P -> P).
	intros.
	assert (P\/~P) by apply EM.
	destruct H0.
	exact H0.
	contradiction.
	intros.
	apply H.
	intro.
	apply H0.
	split.
	apply H.
	intro.
	apply H1.
	left.
	exact H2.
	apply H.
	intro.
	apply H1.
	right.
	exact H2.
	Qed.

view raw de_morgen.coq hosted with ❤ by GitHub

Coqの証明を見つけたら、とりあえずIDEで実行してみると、大体の流れがつかめると思う。
ここで、Coqは排中律を認めないので、forall P Q:Prop, ~(P /\ Q) -> (~P \/ ~Q)とかは排中律を公理として追加しないといけないことにも注意が必要。


他にもCoq-99 : Part 1の証明を書いたりした。

	Lemma Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C.
	Proof.
	intros.
	apply H.
	apply H1.
	apply H0.
	apply H1.
	Qed.
	Lemma Coq_02 : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C.
	Proof.
	intros.
	destruct H.
	destruct H0.
	split.
	split.
	auto.
	auto.
	auto.
	Qed.
	Lemma Coq_03 : forall A B C D:Prop, (A -> C) /\ (B -> D) /\ A /\ B -> C /\ D.
	Proof.
	intros.
	destruct H.
	destruct H0.
	destruct H1.
	split.
	auto.
	auto.
	Qed.
	Lemma Coq_04 : forall A : Prop, ~(A /\ ~A).
	Proof.
	unfold not.
	intros.
	destruct H.
	apply H0.
	apply H.
	Qed.
	Lemma Coq_05 : forall A B C:Prop, A \/ (B \/ C) -> (A \/ B) \/ C.
	Proof.
	intros.
	destruct H.
	left.
	left.
	exact H.
	destruct H.
	left.
	right.
	exact H.
	right.
	exact H.
	Qed.
	Lemma Coq_06 : forall A, ~~~A -> ~A.
	Proof.
	intros.
	unfold not.
	unfold not in H.
	intros.
	apply H.
	intros.
	apply H1.
	exact H0.
	Qed.
	Lemma Coq_07 : forall A B:Prop, (A->B)->~B->~A.
	Proof.
	unfold not.
	intros.
	apply H0.
	apply H.
	apply H1.
	Qed.
	Lemma Coq_08: forall A B:Prop, ((((A->B)->A)->A)->B)->B.
	Proof.
	intros.
	apply H.
	intros.
	apply H0.
	intros.
	apply H.
	intros.
	exact H1.
	Qed.
	Lemma Coq_09 : forall A:Prop, ~~(A\/~A).
	Proof.
	unfold not.
	intros.
	apply H.
	right.
	intros.
	apply H.
	left.
	exact H0.
	Qed.

view raw Coq_99_part_1.coq hosted with ❤ by GitHub