reverse_spec_2.v

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Definition rev_spec (X: Type) (rev: list X -> list X) :=
  (forall x, rev [x] = [x]) /\ (forall xs ys, rev (xs ++ ys) = rev ys ++ rev xs).

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

Lemma rev_spec_nil:
  forall (X: Type) (rev: list X -> list X),
    rev_spec rev -> rev [] = [].
Proof.
  intros X rev [_ A].
  apply app_eq_nil with (xs := rev []).
  symmetry.
  change (rev ([] ++ []) = rev [] ++ rev []).
  apply A.
Qed.

Lemma rev_spec_cons:
  forall (X: Type) (rev: list X -> list X),
    rev_spec rev -> forall x xs, rev (x :: xs) = rev xs ++ [x].
Proof.
  intros X rev [S A] x xs.
  replace (x :: xs) with ([x] ++ xs) by reflexivity.
  rewrite A.
  rewrite S.
  reflexivity.
Qed.

Lemma rev_spec_unique:
  forall X (f g: list X -> list X),
    rev_spec f -> rev_spec g -> forall xs, f xs = g xs.
Proof.
  intros X f g F G.
  induction xs as [|x xs]; simpl.
  repeat rewrite rev_spec_nil; trivial.
  repeat match goal with
           | [ |- context [ ?f (x::xs) ] ] => rewrite rev_spec_cons with (rev := f)
         end; try (rewrite IHxs); trivial.
Qed.