Prove curry and uncurry form an isomorphism.

1 files changed, 11 insertions, 0 deletions

diff --git a/src/Soat/Data/Sublist.idr b/src/Soat/Data/Sublist.idr
index 82637ee..98e3c14 100644
--- a/src/Soat/Data/Sublist.idr
+++ b/src/Soat/Data/Sublist.idr
@@ -24,6 +24,17 @@ uncurry {xs = []}        f = []
 uncurry {xs = (x :: xs)} f = f Here :: uncurry (f . There)
 
 public export
+uncurryCurry : (f : xs `Sublist` ys) -> uncurry (curry f) = f
+uncurryCurry []            = Refl
+uncurryCurry (mem :: mems) = cong ((::) mem) (uncurryCurry mems)
+
+public export
+curryUncurry : (0 f : forall x . Elem x xs -> Elem x ys) -> (i : Elem x xs)
+  -> curry (uncurry f) i = f i
+curryUncurry f Here         = Refl
+curryUncurry f (There elem) = curryUncurry (f . There) elem
+
+public export
 Reflexive (List a) Sublist where
   reflexive = uncurry id