[Coq] Tail-recursive reverse

　先のreverse (reverse xs) = xsで示した 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.
Eval compute in rev (cons 1 (cons 2 (cons 3 nil))).

について

Theorem reverse_rev : forall (A:Set) (xs:list A),
 reverse xs = rev xs.

が成り立つ事を示そう。まず補題

Lemma rev'_reverse : forall (A:Set) (xs ys:list A),
 rev' xs ys = reverse xs ++ ys.
Proof.
 intros A xs.
 induction xs; simpl.
   intro. reflexivity.
 intro ys'.
 rewrite (IHxs (cons a ys')).
 (* reverse xs ++ cons a ys' =
    (reverse xs ++ cons a nil) ++ ys' *)
 assert (H: cons a ys' = (cons a nil) ++ ys').
 induction ys'; simpl.
   reflexivity.
 reflexivity.
 rewrite H.
 rewrite (append_assoc A (reverse xs) (cons a nil) ys').
 reflexivity.
Qed.

である。証明の冒頭で intros A xs だけを行い、ysについては intro していないが、ys を残したまま xs の帰納法を行わないと、IHxs を apply するときにうまくいかない。「無闇に intro しない方が良い」という良い例なので、ys を一緒に intros してしまうなど自分で試行錯誤してみて欲しい。

　この補題を使えば、

Theorem reverse_rev : forall (A:Set) (xs:list A),
 reverse xs = rev xs.
Proof.
 intros.
 unfold rev.
 induction xs; simpl.
   reflexivity.
 (* reverse xs ++ cons a nil = rev' xs (cons a nil) *)
 rewrite IHxs.
 (* rev' xs nil ++ cons a nil = rev' xs (cons a nil) *)
 rewrite (rev'_reverse A xs nil).
 rewrite (rev'_reverse A xs (cons a nil)).
 assert (H: forall l:list A, l ++ nil = l).
   induction l; simpl.
     reflexivity.
   rewrite IHl.  reflexivity.
 rewrite (H (reverse xs)).
 reflexivity.
Qed.

と証明出来る。