[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.