今日の証明: 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 A) (ys : list A) := match xs with | nil => ys | x::xs => x :: (append xs ys) end. (* append を演算子に *) Infix "+++" := append (at level 50). Fixpoint reverse {A : Type} (xs : list A) := match xs with | nil => nil | x::xs => (reverse xs) +++ (x::nil) end. Lemma ReverseAppend {A : Type} (xs : list A) (x : A) : reverse (xs +++ (x::nil)) = x::(reverse xs). Proof. intros A xs. induction xs. reflexivity. intros. simpl in |- *. rewrite IHxs in |- *. reflexivity. Qed. Theorem RevReflect : forall {A : Type} {xs : list A}, reverse (reverse xs) = xs. Proof. intros. induction xs. reflexivity. simpl in |- *. rewrite ReverseAppend in |- *. rewrite IHxs in |- *. reflexivity. Qed.