Idris proof that vector concatenation preserves length

ConcatVec.idr

||| Demonstration of length preservation during vector concatenation.
||| Derived from Guillaume Allais's Agda original.
|||
||| Ignore the fact that functions here are named "reverse" -- they are really
||| concatenation.
module ConcatVec

import Data.Vect

%default total

-- A proposition that `m + n = p`.
data Plus : (m, n, p : Nat) -> Type where
  -- `m + m = m`. 
  base : Plus m 0 m
  -- If `m + n = p`, `(suc m) + n = (suc p)`. 
  step : {n, p : Nat} -> (pr : Plus m n p) -> Plus m (S n) (S p)

-- Converts an equality proposition to a `Plus`.
eqToPlus : (m, n, p : Nat) -> (eq : n + m = p) -> Plus m n p
eqToPlus Z Z Z Refl = ?rhs 
eqToPlus (S m) Z (S p) prf with (decEq m p)
  eqToPlus (S m) Z (S m) prf | Yes Refl = base 
  eqToPlus (S m) Z (S p) prf | No neq = absurd (neq (succInjective _ _ prf))
 eqToPlus m (S n) (S p) prf = step $ eqToPlus m n p (succInjective _ _ prf)

-- Converts a `Plus` to the corresponding equality proposition.
plusToEq : {m, n, p : Nat} -> (pr : Plus m n p) -> n + m = p
plusToEq base      = Refl 
plusToEq (step pr) = cong $ plusToEq pr

-- Concatenates the elements of `xs` before `ys`, maintaining proof of the
-- length of the final product. 
reverseRec : {m, n, p : Nat} -> {A : Type} -> (pr : Plus m n p) ->
             (xs : Vect n A) -> (ys : Vect m A) -> Vect p A
reverseRec base      []       ys = ys 
reverseRec (step pr) (x :: xs) ys = x :: reverseRec pr xs ys

-- Concatenates two vectors.
reverse' : {m, n : Nat} -> {A : Type} -> (xs : Vect n A) -> (ys : Vect m A) ->
                                           Vect (m + n) A
reverse' {m} {n} = reverseRec (eqToPlus _ _ _ (plusCommutative n m))

-- Finds the length of a vector.
length' : {A : Type} -> {n : Nat} -> (xs : Vect n A) -> Nat
length' []       = Z
length' (x :: xs) = S $ length' xs

-- Proof that concatenation preserves length.
reverseRecLength : {m, n, p : Nat} -> {A : Type} -> (pr : Plus m n p) ->
                   (xs : Vect n A) -> (ys : Vect m A) ->
                   length' (reverseRec pr xs ys) = length' xs + length' ys
reverseRecLength base      []       ys = Refl
reverseRecLength (step pr) (x :: xs) ys = cong $ reverseRecLength pr xs ys

-- Proof that concatenation preserves length.
reverseLength : {m, n : Nat} -> {A : Type} -> (xs : Vect n A) ->
                                              (ys : Vect m A) -> 
                 length' (reverse' xs ys) = length' xs + length' ys
reverseLength {m} {n} = reverseRecLength (eqToPlus _ _ _ (plusCommutative n m))