From 8c529393421843a7ccad041d2f29fa90b46bf6b6 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 30 Jun 2023 20:45:33 +0100
Subject: Define zippers and prove no cycles exist.

---
 src/Data/Vect/Properties/Insert.idr | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 src/Data/Vect/Properties/Insert.idr

(limited to 'src/Data/Vect/Properties')

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
-- 
cgit v1.2.3