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

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

ハノイ

Coqでハノイの塔に関する証明

Coqが今流行っているらしい。twitter経由で偶然ハノイの塔をCoq形式化している記事を見つけた。 なんか巷でCoqがはやっているようなので - 菊やんの雑記帳なんかおもしろそうなので一つ簡単な命題を証明してみた。証明したこと Lemma answer_length : forall…