眠気と戦う日々

眠気と戦いながらいろいろと書くブログ

Coq

リスト反転関数が単射であることを証明する

coq

久々の記事もまたCoqでソフトウェアの基礎ネタです。 今回はList_Jにおける練習問題「rev_injective」について。 問題のTheorem Theorem rev_injective: forall l1 l2: natlist, rev l1 = rev l2 -> l1 = l2. ソフトウェアの基礎ではCoqコードではありません…

内部でFixpointの関数を呼ぶ関数を定義した時にsimplだと証明できない

Coq

はい、表題のとおりです。 Coqを勉強していたらよくわからない挙動にぶつかったのでメモ。 問題のコード Fixpoint evenb (n:nat) : bool := match n with | O => true | S O => false | S (S n') => evenb n' end. Definition oddb (n:nat) : bool := negb (…