突然ですが、皆さんは定理証明支援器ってご存知ですか。
定理証明支援器というのは、命題論理の定理を半自動で証明することを可能にしてくれるツールです。
去年の末、「テスト？ちがうちがう。これからの時代は証明だよ！」という話になったので、どうせOCamlやってるんだしCoqをしっかり学んでみることにしました。
私が大学院で専攻している物理学（とくに理論物理学）は証明と密接な関係があります。（というより証明のない物理は物理じゃないです）
というわけで十八番だし、その辺の定理なんてサクっと証明してやんよ！と意気込んでやってみると、まあ物理の理論の証明と命題論理の定理の証明がそもそも違う訳でうまくいかず四苦八苦してます。
今回は練習がてら簡単な証明をやってるのでそれを今度からブログでのせていくことにしました。
今回は勉強の際に参考にさせてもらっているプログラミングCoqの練習問題の問8. forall (n : nat), (exists m, n = 2 * m) \/ (exists m, n = 2 * m + 1) をやってみました。プログラミングCoqのページにある回答の方がすっきりしてます。証明もリファクタリングが必要ですね！
Goal forall (n : nat), (exists m, n = 2 * m) \/ (exists m, n = 2 * m + 1). intros. (* 帰納法を使う *) induction n. (* まずはn=0のときから *) left. exists 0. reflexivity. (* 次にnが成り立つとして、n+1が成り立つか *) destruct IHn. right. destruct H. rewrite H. exists x. Require Import Arith. rewrite plus_comm. reflexivity. left. destruct H. rewrite H. exists (x + 1). rewrite mult_plus_distr_l. rewrite mult_1_r. rewrite <-H. Require Import ZArith. rewrite ZL0. rewrite plus_permute. rewrite <- ZL0. rewrite <- H. reflexivity. Qed.
まだまだStandard Libraryのモジュールを使いこなせていないので、そちらも使いこなせるようにもなりたいですね。あとは実際に関数を作って証明した上でExtractionしてプログラミングが今の目標ですね。シミュレーションとかできればいいなー。
