Define zippers and prove no cycles exist.

1 files changed, 26 insertions, 0 deletions

diff --git a/src/Data/Vect/Properties/Insert.idr b/src/Data/Vect/Properties/Insert.idr
new file mode 100644
index 0000000..28393b1
--- /dev/null
+++ b/src/Data/Vect/Properties/Insert.idr
@@ -0,0 +1,26 @@
+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