この記事は「Theorem Prover Advent Calendar 2013」5日目の記事である。 最近、とある大手企業のシステムのバイナリデータを扱う処理の高速化のためにCoqを使ったのだが、ちょっとアレっと思ったことを体験したのでそれを共有したいと思う。 問題の概要は表…