Hatena::Groupcoq

mzpの日記

2009-11-23

今日の証明: 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.