Vector_rev.v

Require Import Coq.Vectors.Vector.
Import VectorNotations.

Fixpoint vappend {T : Type} {n m} (v1 : t T n) (v2 : t T m)
  : t T (plus n m) :=
  match v1 in t _ n return t T (plus n m) with
  | [] => v2
  | x :: v1' => x :: vappend v1' v2
  end.

Fixpoint plus_n_S n m : n + S m = S (n + m) :=
  match n with
  | 0 => eq_refl
  | S n => f_equal S (plus_n_S n m)
  end.

Fixpoint plus_n_O n : n + 0 = n :=
  match n with
  | 0 => eq_refl
  | S n => f_equal S (plus_n_O n)
  end.

Fixpoint vreverse {T : Type} {n} (v : t T n) : t T n :=
  match v in t _ n return t T n with
  | [] => []
  | x :: v =>
    eq_rect _ (t T)
      (eq_rect _ (t T) (vappend (vreverse v) [x]) _ (plus_n_S _ 0))
              _ (f_equal S ( plus_n_O _))
  end.

Compute vreverse (1 :: 2 :: 3 :: []).