Coq
久々の記事もまたCoqでソフトウェアの基礎ネタです。 今回はList_Jにおける練習問題「rev_injective」について。 問題のTheorem Theorem rev_injective: forall l1 l2: natlist, rev l1 = rev l2 -> l1 = l2. ソフトウェアの基礎では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 (…