はじめてのCoq

Coqは証明支援系というらしいですが、普通の意味でのプログラミングできないことにはあまり役にたたないと思います。証明にこだわらないで、せめてソート関数なり、、、いやもっと実用的なものをプログラミングしてみたら良いんじゃないかと思います。

ですが、プログラミングで証明するとはどういうことか知りたいので、ついつい証明してしまいました。まず命題論理で

 (AvB->C)->((A^B)->C)

はトートロジーになってます。このことを証明します。無名の定理はGoalから始めて、命題を書けば良いようです(不正確ですが、論理命題の証明支援ツールとして使うならば、その理解で良いと思っています)。

Goal forall (A B C : Prop), ((A\/B)->C)->((A/\B)->C).

forallはAの逆さになった奴で所謂「任意の」ってやつですね。それでPropはA,B,Cが命題ですよってことをCoqに教えています。さっそく証明をはじめます。Proof.と書き、証明をずらずらと書きます。

Proof.
intros.
apply H.
left.
apply H0.
Qed.

これで証明できてるのですが、自然演繹法(フィッチスタイル)と比較すると次のようになります。applyする毎に自然演繹法と逆行して行ってます。