yoshihiro503 https://blog.hatena.ne.jp/yoshihiro503/ にわとり小屋でのプログラミング https://yosh.hateblo.jp/ この記事は「Theorem Prover Advent Calendar 2013」5日目の記事である。 最近、とある大手企業のシステムのバイナリデータを扱う処理の高速化のためにCoqを使ったのだが、ちょっとアレっと思ったことを体験したのでそれを共有したいと思う。 問題の概要は表題の通り。シンプルな問題なので、レガシーCoq (version 8.4pl2) で説明する。 簡単のため、やや人工的な例を紹介する。 まず、正の自然数を引数にとる関数fを仮定し、その関数は引数が偶数のときは、戻り値はその半分になるとする。深い意味は無いので考えてはいけない。 Variable f : forall n… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fyosh.hateblo.jp%2Fentry%2F2013%2F12%2F06%2F202827" title="依存関係のある値のうちの一部をrewriteしようとしたときの問題 - にわとり小屋でのプログラミング" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2013-12-06 20:28:27 rich https://yosh.hateblo.jp/entry/2013/12/06/202827 1.0 100%