Coq を使って「どう書く」の問題を解いてみた 〜五角形の世界であなたは過去の自分に出会う〜 - Qiita

これは Theorem Prover Advent Calendar 2016 の5日目の記事です。 はじめに オフラインリアルタイムどう書くというプログラマ向けイベントがあります。オフラインで集まって、主催者が出したプログラミング課題を参加者が制限時間内に解いて、回答を発表しあうというものです。そこで過去に出題された課題に対してCoq/SSReflectを使った回答を試みた、というのがこの記事の趣旨です。さすがにイベントで回答するには時間が足りなさすぎるので、自宅で解きました。この記事で扱う問題はこれです。 五角形の世界であなたは過去の自分に出会う 五角形で敷き詰められた升目を移動するためのコマンド列が与えられるので、閉路を見つけなさいという問題です。詳細はリンク先をご覧ください。回答を試みたところ、結果的にこうなりました。 自分なりに回答した。問題を自分なりに定式化して、その仕様を満た