1 files changed, 84 insertions, 0 deletions
diff --git a/src/Data/Setoid/List.idr b/src/Data/Setoid/List.idr
new file mode 100644
index 0000000..76a79cd
--- /dev/null
+++ b/src/Data/Setoid/List.idr
@@ -0,0 +1,84 @@
+||| Setoid of lists over a setoid and associated definitions
+module Data.Setoid.List
+
+import Data.List
+import Data.Setoid.Definition
+
+%default total
+
+namespace Relation
+  public export
+  data (.ListEquality) : (a : Setoid) -> Rel (List $ U a) where
+    Nil : a.ListEquality [] []
+    (::) : (hdEq : a.equivalence.relation x y) -> (tlEq : a.ListEquality xs ys) ->
+          a.ListEquality (x :: xs) (y :: ys)
+
+public export
+(.ListEqualityReflexive) : (a : Setoid) -> (xs : List $ U a) -> a.ListEquality xs xs
+a.ListEqualityReflexive [] = []
+a.ListEqualityReflexive (x :: xs) = a.equivalence.reflexive x :: a.ListEqualityReflexive xs
+
+public export
+(.ListEqualitySymmetric) : (a : Setoid) -> (xs,ys : List $ U a) -> (prf : a.ListEquality xs ys) ->
+  a.ListEquality ys xs
+a.ListEqualitySymmetric [] [] [] = []
+a.ListEqualitySymmetric (x :: xs) (y :: ys) (hdEq :: tlEq)
+  = a.equivalence.symmetric x y hdEq :: a.ListEqualitySymmetric xs ys tlEq
+
+public export
+(.ListEqualityTransitive) : (a : Setoid) -> (xs,ys,zs : List $ U a) ->
+  (prf1 : a.ListEquality xs ys) -> (prf2 : a.ListEquality ys zs) ->
+  a.ListEquality xs zs
+a.ListEqualityTransitive [] [] [] [] [] = []
+a.ListEqualityTransitive (x :: xs) (y :: ys) (z :: zs) (hdEq1 :: tlEq1) (hdEq2 :: tlEq2)
+  = a.equivalence.transitive x  y  z  hdEq1 hdEq2 ::
+    a.ListEqualityTransitive xs ys zs tlEq1 tlEq2
+
+public export
+ListSetoid : (a : Setoid) -> Setoid
+ListSetoid a = MkSetoid (List $ U a)
+  $ MkEquivalence
+  { relation   = a.ListEquality
+  , reflexive  = a.ListEqualityReflexive
+  , symmetric  = a.ListEqualitySymmetric
+  , transitive = a.ListEqualityTransitive
+  }
+
+public export
+ListMapFunctionHomomorphism : (f : a ~> b) ->
+  SetoidHomomorphism (ListSetoid a) (ListSetoid b) (map f.H)
+ListMapFunctionHomomorphism f [] [] [] = []
+ListMapFunctionHomomorphism f (x :: xs) (y :: ys) (hdEq :: tlEq) =
+  f.homomorphic x y hdEq :: ListMapFunctionHomomorphism f xs ys tlEq
+
+public export
+ListMapHomomorphism : (f : a ~> b) -> (ListSetoid a ~> ListSetoid b)
+ListMapHomomorphism f = MkSetoidHomomorphism (map f.H) (ListMapFunctionHomomorphism f)
+
+public export
+ListMapIsHomomorphism : SetoidHomomorphism (a ~~> b) (ListSetoid a ~~> ListSetoid b)
+  ListMapHomomorphism
+ListMapIsHomomorphism f g f_eq_g [] = []
+ListMapIsHomomorphism f g f_eq_g (x :: xs) = f_eq_g x :: ListMapIsHomomorphism f g f_eq_g xs
+
+public export
+ListMap : {0 a, b : Setoid} -> (a ~~> b) ~> (ListSetoid a ~~> ListSetoid b)
+ListMap = MkSetoidHomomorphism
+  { H           = ListMapHomomorphism
+  , homomorphic = ListMapIsHomomorphism
+  }
+
+public export
+reverseHomomorphic : {a : Setoid} -> (x, y : List (U a)) ->
+  (a.ListEquality x y) -> a.ListEquality (reverse x) (reverse y)
+reverseHomomorphic x y prf = roh [] [] x y (a.ListEqualityReflexive _) prf
+  where roh  : (ws, xs, ys, zs : List (U a)) -> a.ListEquality ws xs -> a.ListEquality ys zs ->
+               a.ListEquality (reverseOnto ws ys) (reverseOnto xs zs)
+        roh ws xs   []      []    wx     []       = wx
+        roh ws xs (y::ys) (z::zs) wx (yzh :: yzt) = roh (y::ws) (z::xs) ys zs (yzh :: wx) yzt
+
+public export
+appendCongruence : {a : Setoid} -> (x1, x2, y1, y2 : List (U a)) ->
+  a.ListEquality x1 y1 -> a.ListEquality x2 y2 -> a.ListEquality (x1 ++ x2) (y1 ++ y2)
+appendCongruence   []    x2   []    y2    []    p = p
+appendCongruence (x::xs) x2 (y::ys) y2 (ph::pt) p = ph :: appendCongruence _ _ _ _ pt p