読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

さあ!証明しよう!

Coq入門 Proof

今日紹介するコマンドはProofコマンドだ。
このコマンドは何もしない。
Proofというからには、自動証明をやってくれるだろう、とか、何かすごいCoqの力で証明が変形するのかな、とか思う人がいるかもしれないが、このコマンドは何もしない。
このコマンドをいつでも、何回でも使うことができるが、使わなくても結果はかわらない。「これから証明するぞ!」という意気込みを表す勢いだけのコマンドである。
しかしあなどってはならない。このコマンドを証明の最初に入力することによって、どんな難問でも証明できてしまうような勇気がでてくるのだ。このことは紙での証明でも同じで、非常に重要であるように感じる。なぜなら証明するために必要な要素は勇気だからである。
Coqの取り扱い説明書にも、証明の最初にProofコマンドを使う奴は男前だと書いてある!
今日から証明するときにはプルーフ!と堂々と宣言しよう!