module Data.Vect.Properties.Insert

import Data.Vect

export
mapInsertAt :
  (0 f : a -> b) ->
  (i : Fin (S n)) ->
  (0 x : a) ->
  (xs : Vect n a) ->
  map f (insertAt i x xs) = insertAt i (f x) (map f xs)
mapInsertAt f FZ x xs = Refl
mapInsertAt f (FS i) x (y :: xs) = cong (f y ::) $ mapInsertAt f i x xs

export
indexInsertAt : (i : Fin (S n)) -> (0 x : a) -> (xs : Vect n a) -> index i (insertAt i x xs) = x
indexInsertAt FZ x xs = Refl
indexInsertAt (FS i) x (y :: xs) = indexInsertAt i x xs

export
insertAtIndex :
  (i : Fin (S n)) ->
  (xs : Vect (S n) a) ->
  insertAt i (index i xs) (deleteAt i xs) = xs
insertAtIndex FZ (x :: xs) = Refl
insertAtIndex (FS i) (x :: xs@(_ :: _)) = cong (x ::) $ insertAtIndex i xs