rev.v

Notation "`Begin p" := p (at level 20, right associativity).
Notation "a =] p ] pr" := (@eq_trans _ a _ _ p pr) (at level 30, right associativity).
Notation "a =[ p [ pr" := (@eq_trans _ a _ _ (eq_sym p) pr) (at level 30, right associativity).
Notation "a `End" := (@eq_refl _ a) (at level 10).

Proposition congr {A B : Type} {a b : A} (P : A -> B) (p : a = b) : P a = P b.
  rewrite p. reflexivity.
Qed.

Inductive list (T: Type) : Type :=
| nil : list T
| cons : T -> list T -> list T.

Arguments nil {_}.
Arguments cons {_}.

Variable (T : Type).

Fixpoint append (xs : list T) (ys : list T) : list T :=
  match xs with
    | nil => ys
    | cons z zs => cons z (append zs ys)
  end.

Notation "l1 ++ l2" := (append l1 l2).

Fixpoint append_nil_right (xs : list T) : xs ++ nil = xs :=
  match xs with
    | nil => eq_refl
    | cons z zs => congr (cons z) (append_nil_right zs)
  end.

Fixpoint append_assoc (xs ys zs : list T) : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
  match xs with
    | nil => eq_refl
    | cons x xss => congr (cons x) (append_assoc xss ys zs)
  end.

Fixpoint reverse (xs : list T) : list T :=
  match xs with
    | nil => nil
    | cons x xs => reverse xs ++ cons x nil
  end.

Fixpoint rev_append (xs ys : list T) : reverse (xs ++ ys) = reverse ys ++ reverse xs :=
  match xs with
    | nil =>
      `Begin
       reverse (nil ++ ys) =] eq_sym (append_nil_right (reverse ys)) ]
       (reverse ys ++ reverse nil)
      `End
    | cons x xs =>
      match ys with
        | nil =>
          `Begin
           reverse (cons x xs ++ nil) =] congr reverse (append_nil_right (cons x xs)) ]
           reverse (cons x xs) =] eq_refl ]
           (reverse nil ++ reverse (cons x xs))
          `End
        | ys =>
          `Begin
           reverse (cons x xs ++ ys) =] eq_refl ]
           (reverse (xs ++ ys) ++ cons x nil) =] congr (fun t => t ++ _) (rev_append _ _) ]
           ((reverse ys ++ reverse xs) ++ cons x nil) =] eq_sym (append_assoc _ _ _) ]
           (reverse ys ++ (reverse xs ++ cons x nil)) =] eq_refl ]
           (reverse ys ++ reverse (cons x xs))
          `End
      end
  end.

Fixpoint rev_rev_id (xs : list T) : reverse (reverse xs) = xs :=
  match xs with
    | nil => eq_refl
    | cons x xs =>
      `Begin
       reverse (reverse (cons x xs)) =] eq_refl ]
       reverse (reverse xs ++ cons x nil) =] rev_append _ _ ]
       (reverse (cons x nil) ++ reverse (reverse xs)) =] congr _ (rev_rev_id xs) ]
       (reverse (cons x nil) ++ xs) =] eq_refl ]
       (cons x xs)
      `End
  end.