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