26 April, 2010

[Coq] reverse (reverse xs) = xs

 先日のProofCafeでみんなで解いていた reverse (reverse xs) = xs の証明について、どんな風に解くかを解説というか自分の解答を晒すというか。

 教科書でこの問題を演習課題として解く場合は、予め必要な補題が順々に証明課題として与えられる事が多いが、現実の問題ではそういうことはまず無い。(このあたり、現実の問題と試験問題の違いにも通ずる話だ。)

 まず、ProofCafe01から必要な定義をコピーしよう。
Inductive list (A: Type) : Type :=
| nil : list A
| cons : A -> list A -> list A.

Implicit Arguments nil [A].
Implicit Arguments cons [A].

Fixpoint append {A : Type} (xs ys: list A) : list A :=
match xs with
| nil => ys
| cons x xs => cons x (append xs ys)
end.
Infix "++" := append (at level 60).

Theorem append_assoc : forall (A:Type) (xs ys zs:list A),
(xs ++ ys) ++ zs = xs ++ (ys ++ zs).
Proof.
(* あなたの証明を書いてね *)
Qed.

定理append_assocの証明は難しく無いと思うが、判らない人はProofCafeのページを参照して欲しい。

 次いで、関数reverseを定義しよう。
 関数型言語で関数を末尾再帰で書くのに慣れている人は、ついうっかり
Fixpoint rev' {A:Set} (xs ys:list A) :=
match xs with
| nil => ys
| cons x xs' => rev' xs' (cons x ys)
end.
Definition rev {A:Set} (xs:list A) := rev' xs nil.

と書いてしまうだろう。私も実は当日そう書いてしまい嵌った。

 ここは実行効率を考えず、ひとまず素直に、
Fixpoint reverse {A:Set} (xs:list A) :=
match xs with
| nil => nil
| cons x xs' => (reverse xs') ++ (cons x nil)
end.

と定義して証明する方が簡単だ。関数を実際に動かしてみる場合は、
Eval compute in reverse (cons 1 (cons 2 (cons 3 nil))).

とか入力してみれば良い。

 ここから、どうやって証明していったか、考えた過程を示そう。
 まずはいきなり、定理を証明しようとしてみた。
Theorem reverse_reverse : forall (A:Set) (xs:list A),
reverse (reverse xs) = xs.
Proof.
induction xs; simpl.
reflexivity.

最初にxsについての帰納法を試み、xs=nilのケースは簡単に証明出来た。次のゴールの
reverse (reverse xs ++ (cons a nil) = cons a xs
については、リストを ++ で繋いでreverseする、
Hypothesis reverse_append : forall (A:Set) (xs ys:list A),
reverse (xs ++ ys) = (reverse ys) ++ (reverse xs).

という定理があれば都合が良さそうだと何となく思いつく。(なんとなく美しげな定理だし。)

 そこで、とりあえず上記のHypothesisを先に定義して、改めてreverse_reverseを証明する。
Theorem reverse_reverse : forall (A:Set) (xs:list A),
reverse (reverse xs) = xs.
Proof.
induction xs; simpl.
reflexivity.
rewrite (reverse_append A (reverse xs) (cons a nil)).
rewrite IHxs.


 この時点でゴールが
reverse (cons a nil) ++ xs = cons a xs
となる。そこで再度
Hypothesis append_cons_nil : forall (A:Set) (a:A) (xs:list A),
(cons a nil) ++ xs = cons a xs.
Hypothesis reverse_cons : forall (A:Set) (a:A),
reverse (cons a nil) = cons a nil.

を追加してから、改めてreverse_reverseを証明する。
Theorem reverse_reverse : forall (A:Set) (xs:list A),
reverse (reverse xs) = xs.
Proof.
induction xs; simpl.
reflexivity.
rewrite (reverse_append A (reverse xs) (cons a nil)).
rewrite IHxs.
rewrite (reverse_cons A a).
rewrite (append_cons_nil A a xs).
reflexivity.
Qed.


 証明が出来たので、Hypothesisで誤摩化していた部分をLemma, Theoremに書き換えて証明する。
Lemma append_cons_nil : forall (A:Set) (a:A) (xs:list A),
(cons a nil) ++ xs = cons a xs.
Lemma reverse_cons : forall (A:Set) (a:A),
reverse (cons a nil) = cons a nil.

については難しく無いので証明してみると良いだろう。(intros, simpl, reflexivityで証明出来る。)

Theorem reverse_append : forall (A:Set) (xs ys:list A),
reverse (xs ++ ys) = (reverse ys) ++ (reverse xs).

については、解説しよう。

Proof.
intros A xs ys.
induction xs; simpl.
assert (append_nil: forall (zs:list A), zs = zs ++ nil).
induction zs; simpl.
reflexivity.
rewrite <- IHzs. reflexivity.
apply (append_nil (reverse ys)).
rewrite IHxs.
rewrite (append_assoc A (reverse ys) (reverse xs) (cons a nil)).
reflexivity.
Qed.

証明の途中でzs = zs ++ nilが使いたくなり、わざわざ補題にするまでもないと思って、途中でassertで証明している。
 この証明したreverse_appendを使って、reverse_reverseを証明すれば完成。

 全体を改めて示すとこのようになる。
Inductive list (A: Type) : Type :=
| nil : list A
| cons : A -> list A -> list A.

Implicit Arguments nil [A].
Implicit Arguments cons [A].

Fixpoint append {A : Type} (xs ys: list A) : list A :=
match xs with
| nil => ys
| cons x xs => cons x (append xs ys)
end.
Infix "++" := append (at level 60).

Theorem append_assoc : forall (A: Type) (xs ys zs : list A),
(xs ++ ys) ++ zs = xs ++ (ys ++ zs).
Proof.
intros.
induction xs; simpl.
reflexivity.
rewrite IHxs. reflexivity.
Qed.

Fixpoint reverse {A:Set} (xs:list A) :=
match xs with
| nil => nil
| cons x xs' => (reverse xs') ++ (cons x nil)
end.

Lemma append_cons_nil : forall (A:Set) (a:A) (xs:list A),
(cons a nil) ++ xs = cons a xs.
Proof.
intros. simpl. reflexivity.
Qed.
Lemma reverse_cons : forall (A:Set) (a:A),
reverse (cons a nil) = cons a nil.
Proof.
intros. simpl. reflexivity.
Qed.

Theorem reverse_append : forall (A:Set) (xs ys:list A),
reverse (xs ++ ys) = (reverse ys) ++ (reverse xs).
Proof.
intros A xs ys.
induction xs; simpl.
assert (append_nil: forall (zs:list A), zs = zs ++ nil).
induction zs; simpl.
reflexivity.
rewrite <- IHzs. reflexivity.
apply (append_nil (reverse ys)).
rewrite IHxs.
rewrite (append_assoc A (reverse ys) (reverse xs) (cons a nil)).
reflexivity.
Qed.

Theorem reverse_reverse : forall (A:Set) (xs:list A),
reverse (reverse xs) = xs.
Proof.
induction xs; simpl.
reflexivity.
rewrite (reverse_append A (reverse xs) (cons a nil)).
rewrite IHxs.
rewrite (reverse_cons A a).
rewrite (append_cons_nil A a xs).
reflexivity.
Qed.

No comments: