[Coq] Specification of rev

そもそもの動機は（普通に再帰で書かれた） rev 関数の正しさを保証する最小の Unit Test ケースは何だろうみたいな話で、リストを逆転する rev 関数についての性質を話していて。

A:Type とし、f : list A -> list A な関数とするとき、

• f (x::nil) = x::nil
• f (xs ++ ys) = f ys ++ f xs

が成り立てば f = rev と言えるか？

については下記の様に肯定的に示せる。

Require Import FunctionalExtensionality.
Require Import List.
Require Import Omega.

Goal forall (A:Type)(f:list A->list A),
 (forall xs ys, f (xs++ys) = f ys ++ f xs) ->
 (forall x, f (x::nil) = x::nil) ->
 f = (@rev A).
Proof.
intros.
assert(f nil = nil).
 specialize(app_length (f nil) (f nil)). intro.
 rewrite <- (H nil nil) in H1. simpl in H1.
 assert(length (f nil) = 0).
  omega.
 induction (f nil).
  auto.
 simpl in H2. discriminate H2.
assert(forall x xs, f (x::xs) = f xs ++ (x::nil)).
 intros.
 replace (x::xs) with ((x::nil) ++ xs).
  rewrite H. rewrite H0. auto.
 simpl. auto.
extensionality l.
induction l.
 simpl. auto.
simpl. rewrite H2. rewrite IHl. auto.
Qed.