先日の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.
