Initial version

2 files changed, 142 insertions, 0 deletions

diff --git a/src/Data/Setoid/Vect/Functional.idr b/src/Data/Setoid/Vect/Functional.idr
new file mode 100644
index 0000000..8fd6e3b
--- /dev/null
+++ b/src/Data/Setoid/Vect/Functional.idr
@@ -0,0 +1,64 @@
+||| The setoid of vectors over a given setoid, defined using a function
+module Data.Setoid.Vect.Functional
+
+import Data.Setoid.Definition
+
+import Data.Vect
+import Data.HVect
+import Data.Vect.Properties
+import Data.Setoid.Vect.Inductive
+import Control.Order
+import Syntax.PreorderReasoning.Setoid
+
+
+%default total
+
+public export
+0 (.VectEquality) : (a : Setoid) -> Rel (Vect n (U a))
+a.VectEquality xs ys = (i : Fin n) ->
+  a.equivalence.relation (index i xs) (index i ys)
+
+-- Not using the more sensible type definition
+-- Inductive.(.VectEquality) a xs ys -> Functional.(.VectEquality) a xs ys
+-- so that the arguments are in the order as Vect's index.
+export
+index : (i : Fin n) ->
+        Inductive.(.VectEquality) a xs ys ->
+        a.equivalence.relation (index i xs) (index i ys)
+index FZ     (hdEq :: _) = hdEq
+index (FS k) (_ :: tlEq) = index k tlEq
+
+%hide Inductive.(.VectEquality)
+%hide Inductive.VectSetoid
+
+public export
+VectSetoid : (n : Nat) -> (a : Setoid) -> Setoid
+VectSetoid n a = MkSetoid (Vect n (U a))
+  $ MkEquivalence
+  { relation   = (.VectEquality) a
+  , reflexive  = \xs                    , i =>
+      a.equivalence.reflexive  _
+  , symmetric  = \xs,ys, prf            , i =>
+      a.equivalence.symmetric  _ _   (prf  i)
+  , transitive = \xs, ys, zs, prf1, prf2, i =>
+      a.equivalence.transitive _ _ _ (prf1 i) (prf2 i)
+  }
+
+public export
+VectMap : {a, b : Setoid} -> (a ~~> b) ~>
+  (VectSetoid n a ~~> VectSetoid n b)
+VectMap = MkSetoidHomomorphism
+  (\f => MkSetoidHomomorphism
+    (\xs => map f.H xs)
+    $ \xs, ys, prf, i  => CalcWith b $
+    |~ index i (map f.H xs)
+    ~~ f.H (index i xs)
+                        .=.(indexNaturality _ _ _)
+    ~~ f.H (index i ys) ...(f.homomorphic _ _ $ prf i)
+    ~~ index i (map f.H ys)
+                          .=<(indexNaturality _ _ _))
+  $ \f,g,prf,xs,i => CalcWith b $
+  |~ index i (map f.H xs)
+  ~~ f.H (index i xs) .=.(indexNaturality _ _ _)
+  ~~ g.H (index i xs) ...(prf _)
+  ~~ index i (map g.H xs) .=<(indexNaturality _ _ _)
diff --git a/src/Data/Setoid/Vect/Inductive.idr b/src/Data/Setoid/Vect/Inductive.idr
new file mode 100644
index 0000000..28076c5
--- /dev/null
+++ b/src/Data/Setoid/Vect/Inductive.idr
@@ -0,0 +1,78 @@
+||| The setoid of vectors over a given setoid, defined inductively
+module Data.Setoid.Vect.Inductive
+
+import Data.Setoid.Definition
+
+import Data.Vect
+import Data.HVect
+import Data.Vect.Properties
+
+%default total
+
+public export
+data (.VectEquality) : (a : Setoid) -> Rel (Vect n (U a)) where
+  Nil : a.VectEquality [] []
+  (::) : (hdEq : a.equivalence.relation x y) ->
+         (tlEq : a.VectEquality xs ys) ->
+         a.VectEquality (x :: xs) (y :: ys)
+
+export
+(++) : a.VectEquality xs ys -> a.VectEquality as bs ->
+       a.VectEquality (xs ++ as) (ys ++ bs)
+[] ++ qs = qs
+(p :: ps) ++ qs = p :: (ps ++ qs)
+
+public export
+(.VectEqualityReflexive) : (a : Setoid) -> (xs : Vect n $ U a) -> a.VectEquality xs xs
+a.VectEqualityReflexive [] = []
+a.VectEqualityReflexive (x :: xs) = a.equivalence.reflexive x :: a.VectEqualityReflexive xs
+
+public export
+(.VectEqualitySymmetric) : (a : Setoid) -> (xs,ys : Vect n $ U a) -> (prf : a.VectEquality xs ys) ->
+  a.VectEquality ys xs
+a.VectEqualitySymmetric [] [] [] = []
+a.VectEqualitySymmetric (x :: xs) (y :: ys) (hdEq :: tlEq)
+  = a.equivalence.symmetric x y hdEq :: a.VectEqualitySymmetric xs ys tlEq
+
+public export
+(.VectEqualityTransitive) : (a : Setoid) -> (xs,ys,zs : Vect n $ U a) ->
+  (prf1 : a.VectEquality xs ys) -> (prf2 : a.VectEquality ys zs) ->
+  a.VectEquality xs zs
+a.VectEqualityTransitive [] [] [] [] [] = []
+a.VectEqualityTransitive (x :: xs) (y :: ys) (z :: zs) (hdEq1 :: tlEq1) (hdEq2 :: tlEq2)
+  = a.equivalence.transitive x  y  z  hdEq1 hdEq2 ::
+    a.VectEqualityTransitive xs ys zs tlEq1 tlEq2
+
+public export
+VectSetoid : (n : Nat) -> (a : Setoid) -> Setoid
+VectSetoid n a = MkSetoid (Vect n (U a))
+  $ MkEquivalence
+  { relation   = a.VectEquality
+  , reflexive  = a.VectEqualityReflexive
+  , symmetric  = a.VectEqualitySymmetric
+  , transitive = a.VectEqualityTransitive
+  }
+
+public export
+VectMapFunctionHomomorphism : (f : a ~> b) ->
+  SetoidHomomorphism (VectSetoid n a) (VectSetoid n b) (map f.H)
+VectMapFunctionHomomorphism f [] [] [] = []
+VectMapFunctionHomomorphism f (x :: xs) (y :: ys) (hdEq :: tlEq) =
+  f.homomorphic x y hdEq :: VectMapFunctionHomomorphism f xs ys tlEq
+
+public export
+VectMapHomomorphism : (f : a ~> b) -> (VectSetoid n a ~> VectSetoid n b)
+VectMapHomomorphism f = MkSetoidHomomorphism (map f.H) (VectMapFunctionHomomorphism f)
+
+public export
+VectMapIsHomomorphism : SetoidHomomorphism (a ~~> b) (VectSetoid n a ~~> VectSetoid n b)
+  VectMapHomomorphism
+VectMapIsHomomorphism f g f_eq_g [] = []
+VectMapIsHomomorphism f g f_eq_g (x :: xs) = f_eq_g x :: VectMapIsHomomorphism f g f_eq_g xs
+
+public export
+VectMap : {0 a, b : Setoid} -> (a ~~> b) ~> (VectSetoid n a ~~> VectSetoid n b)
+VectMap = MkSetoidHomomorphism
+  { H           = VectMapHomomorphism
+  , homomorphic = VectMapIsHomomorphism
+  }