reverse_spec.v

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Fixpoint reverse (X: Type) (xs: list X): list X :=
  match xs with
    | [] => []
    | x :: xs' => reverse xs' ++ [x]
  end.

Lemma app_eq_nil: forall (X: Type) (xs ys: list X), xs ++ ys = xs -> ys = [].
  induction xs; simpl; inversion 1; auto.
Qed.

Theorem rev_spec_complete:
  forall (X: Type) (rev: list X -> list X),
    (forall x, rev [x] = [x]) ->
    (forall xs ys, rev (xs ++ ys) = rev ys ++ rev xs) ->
    (forall xs, rev xs = reverse xs).
Proof.
  intros X rev S A; induction xs as [|x' xs']; simpl.
  assert (rev ([] ++ []) = rev [] ++ rev []) as H; auto.
  apply (@app_eq_nil X (rev [])); symmetry; apply H.
  assert (x' :: xs' = [x'] ++ xs') as H; auto.
  rewrite H; rewrite <- IHxs'; rewrite A; rewrite S; reflexivity.
Qed.