zakky_dev https://blog.hatena.ne.jp/zakky_dev/ 眠気と戦う日々 https://zakky-dev.hateblo.jp/ coq 久々の記事もまたCoqでソフトウェアの基礎ネタです。 今回はList_Jにおける練習問題「rev_injective」について。 問題のTheorem Theorem rev_injective: forall l1 l2: natlist, rev l1 = rev l2 -> l1 = l2. ソフトウェアの基礎ではCoqコードではありませんが、型Xの部分をnatとしてCoqコードにするとこんな感じになります。 これについて証明していきましょう。 定理の意味を確認 まずはとにかく定理を見てみましょう。 Theorem rev_injective: forall l1 l2: natlist… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fzakky-dev.hateblo.jp%2Fentry%2F2014%2F10%2F12%2F072518" title="リスト反転関数が単射であることを証明する - 眠気と戦う日々" 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 2014-10-12 07:25:18 rich https://zakky-dev.hateblo.jp/entry/2014/10/12/072518 1.0 100%