<論文・報告>証明支援系Coqの基礎を学ぶ

Abstract

専修コースにおいてPierce他著であるテキストSoftwareFoundationsを用いて，基礎的なCoqの使用方法を学んだ．証明支援システムとは，命題及び証明の記述，証明に欠陥がないかの確認が行えるソフトウェアのことである．利用者はタクティクスと呼ばれるコマンドを用いてソフトウェアと対話方式で証明の記述を進めていく．本論文では，3 つの証明例を用いてCoq の基礎的証明手法を説明する．命題は，(a+b+c+d)2 の展開，ド・モルガンの法則の一例，0 からn までの2 乗の総和に関する公式の3 つである．(a+b+c+d)2 の展開に関しては，タクティクスとしてintros，rewrite，reflexivity が用いられている．ド・モルガンの法則の一例は，bool に関する命題でdestruct という場合分けのためのタクティクスが3 回用いられている．そして0 からn までの2 乗の総和に関する公式は，数学的帰納法を用いるためのタクティクスinduction を使った後，rewrite とassertを用いて書き換えることで証明されている．確かにCoq は厳密性に富むが，証明を理解するのは非常に難しいため，コメントを入れるべきである. I learnt how to use the formal proof management system, Coq, by using the textbook entitled “Software Foundations” by Pierce et al. A proof management system is a piece of computer software that allows users to write down mathematical propositions and proofs, and is able to mechanically check if proofs are correct. Users develop a proof by using commands called “tactics.” In this report, I explain the basic use of Coq with three example proofs. The three statements include the development of (a+b+c+d)2, an instance of De Morgan’s laws, and the formula of the summation of squares of natural numbers from 0 to n. In the development of (a+b+c+d)2, tactics called “rewrite, ” “intros, ” and “reflexivity” are used. In the instance of De Morgan’s laws, which concern Boolean algebra, a tactic called “destruct, ” by which users perform case analysis in Coq, is used three times. The formula of the summation of squares is proven by making use of “rewrite” and “assert” after using the tactic of induction for mathematical induction. Although Coq is very rigorous, users should insert comments into their proofs because it is very difficult for other people to understand proofs written in Coq.