Avoiding to rewrite by plus_n_Sm

ConcatVec.agda

module ConcatVec where

open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Vec
open import Function
open import Relation.Binary.PropositionalEquality

data Plus (m : ℕ) : (n p : ℕ) → Set where
  base : Plus m 0 m
  step : {n p : ℕ} (pr : Plus m n p) → Plus m (suc n) (suc p)

eqToPlus : (m n p : ℕ) (eq : n + m ≡ p) → Plus m n p
eqToPlus m zero    .m             refl = base
eqToPlus m (suc n) .(suc (n + m)) refl = step $ eqToPlus m n (n + m) refl

plusToEq : {m n p : ℕ} (pr : Plus m n p) → n + m ≡ p
plusToEq base      = refl
plusToEq (step pr) = cong suc $ plusToEq pr

reverseRec : {m n p : ℕ} {A : Set} (pr : Plus m n p)
             (xs : Vec A n) (ys : Vec A m) → Vec A p
reverseRec base      []       ys = ys
reverseRec (step pr) (x ∷ xs) ys = x ∷ reverseRec pr xs ys

reverse′ : {m n : ℕ} {A : Set} (xs : Vec A n) (ys : Vec A m) → Vec A (m + n)
reverse′ {m} {n} = reverseRec (eqToPlus _ _ _ (+-comm n m))

length : {A : Set} {n : ℕ} (xs : Vec A n) → ℕ
length []       = zero
length (x ∷ xs) = suc $ length xs

reverseRecLength : {m n p : ℕ} {A : Set} (pr : Plus m n p)
                   (xs : Vec A n) (ys : Vec A m) →
                   length (reverseRec pr xs ys) ≡ length xs + length ys
reverseRecLength base      []       ys = refl
reverseRecLength (step pr) (x ∷ xs) ys = cong suc $ reverseRecLength pr xs ys

reverse′Length : {m n : ℕ} {A : Set} (xs : Vec A n) (ys : Vec A m) →
                 length (reverse′ xs ys) ≡ length xs + length ys
reverse′Length {m} {n} = reverseRecLength (eqToPlus _ _ _ (+-comm n m))