今日の証明: reverse (reverse xs) = xs - みずぴー日記最近Coqが流行してるので、ボクも流れに乗ってみました。 今回、ボクが証明したかったのは、2回reverseすると元に戻るという性質です。 Theorem RevReflect : forall {A : Type} {xs : list A}, reverse (reverse xs) = xs. そののために、appendを定義したり、Lemmaを証明したりしてます。 状況に応じて、TheoremやLemma、Fact、Remark、Corollary、Propositionを使い分けるのがクールらしいですよ。参考 あとReverseAppendを証明するときは、全部introsしちゃうのじゃなくて、xを残しとくという覚えたてのテクニックを使ってます。引数の順番大事! Require Import List. Fixpoint append {A : Type} (xs : list
