2019年9月19日 | ブログ記事

定理証明で遊ぼう(しなさい)

stretchybox

こんにちは、stretchyboxです。
この記事はtraP夏のブログリレー 9月19日の記事です。

いよいよ夏休みも残り一週間ですね、皆さんは有意義で楽しい休みを送れましたか?
僕はずっと家で寝てました。

定理証明とは

定理証明(自動定理証明)とは、数学的な命題やプログラムの仕様を形式化してその証明を与え、そのコード(証明)が正しく書かれているかを定理証明器で確認することで正当性を検証する手法です。
具体的な用途としては四色問題Kepler予想といった複雑で誰も査読したがらないような数学の問題の証明であったり、高い安全性を求められるソフトウェアの検証に使われています。
今回はその中でも有名なCoqという定理証明器と、それを使って問題が解けるTopProverというサイトで遊んでみようと思います。

Coqの導入

Coq自体の導入は簡単でここのインストーラーを落としてポチポチしてればできます。デフォルトのCoqIDEが使いにくければProofGeneralやVScoqなどのエディタの拡張を使うこともできます。
CoqIDEを起動すると左側にコードを書く部分、右上に示すべき式右下にエラーなどを表示する部分が現れます。ツールバーの右から三番目にある緑色の下向き矢印を押すと、"."区切りの文が読み込まれて、正しければコードが緑色になり、誤りがあればエラーが表示されます。証明のすべてが正しく読み込まれれば証明がなされたことになります。

問題 plus_assoc

問題文
示すべき式は

n,m,oNn+m+o=n+(m+o)\forall n, m, o \in \mathbb{N} \quad n + m + o = n + (m + o)

です。加法は左結合なので自然数の加法における結合法則を表しています。
下の証明ではnに関する帰納法で示しています。

assoc.vDefinition plus_assoc := forall n m o : nat, n + m + o = n + (m + o).
Theorem plus_assoc_proof: plus_assoc.
Proof.
  unfold plus_assoc.
  intro.
  induction n.
  intros.
  simpl.
  reflexivity.
  intros.
  simpl.
  rewrite IHn.
  reflexivity.
Qed.

第一行で問題で与えられる示すべき命題の名前を定義していて、第二行でその命題の証明をこれからすることを示しています。ProofからQedまでの間にあるものは全てタクティックと呼ばれるもので仮定やいま示すべきもの(サブゴール)を変形したり、証明を終了させたりする命令です。

実際にこのコードをコピペして一行ずつ動かしてみると、これらのタクティックがどのように働いているのかがなんとなく見えると思います。
詳しい説明はここをみるとこれらのタクティックの使い方がわかりやすく載っています。また、TopProverでは参加者のコードが見ることができるので上級者のコードを参照することも勉強になると思います。

参考文献

萩原 学『Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化』
基本的なCoqとSSReflectなどのライブラリの使い方が載っていてよいです。
Amazonリンク

おわりに

私の時間と実力が足りずCoqのほんの一部しか紹介できませんでしたが、興味がある方は萩原先生の本や公式ドキュメントに詳しく載っているので調べてみてください。TopProverでは毎週コンテストを行っていてratingもつくようになっているらしいです。私はまだ参加できていないのでこれから参加して強くなっていきたいですね。
明日はRLookさんの記事です。楽しみですね

この記事を書いた人
stretchybox

ロジックが好き

この記事をシェア

このエントリーをはてなブックマークに追加

関連する記事

2019年9月24日
夏のブログリレーエンディング
HF
2019年9月23日
ヒダッカソンに参加しました
oribe
2019年9月22日
ベクターレイヤーを使おう
Sigma1023
2019年9月21日
5,000円の液タブ(笑)を買ってみた。
Hinaruhi
2019年9月20日
Kotlin + GradleでReactアプリを作る
RLook
2019年9月17日
コンピュータの旅をしよう
yasu

活動の紹介

カテゴリ

タグ