Define list-dependent product of indexed family.

1 files changed, 99 insertions, 0 deletions

diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
new file mode 100644
index 0000000..4f6ac34
--- /dev/null
+++ b/src/Soat/Data/Product.idr
@@ -0,0 +1,99 @@
+module Soat.Data.Product
+
+import Control.Relation
+
+%default total
+
+infix 10 ^
+
+-- Definitions
+
+public export
+data (^) : (0 _ : a -> Type) -> List a -> Type where
+  Nil  : x ^ []
+  (::) : {0 x : a -> Type} -> x i -> x ^ is -> x ^ (i :: is)
+
+public export
+ary : List Type -> Type -> Type
+ary []        y = y
+ary (x :: xs) y = x -> ary xs y
+
+-- Conversions
+
+public export
+uncurry : map x is `ary` a -> x ^ is -> a
+uncurry f []        = f
+uncurry f (x :: xs) = uncurry (f x) xs
+
+-- Operations
+
+public export
+map : (f : (i : a) -> x i -> y i) -> {is : List a} -> x ^ is -> y ^ is
+map f []        = []
+map f (x :: xs) = f _ x :: map f xs
+
+public export
+head : x ^ (i :: is) -> x i
+head (x :: xs) = x
+
+public export
+tail : x ^ (i :: is) -> x ^ is
+tail (x :: xs) = xs
+
+public export
+consHeadTail : (xs : x ^ (i :: is)) -> head xs :: tail xs = xs
+consHeadTail (x :: xs) = Refl
+
+-- Relations
+
+namespace Pointwise
+  public export
+  data Pointwise : (0 _ : (i : a) -> Rel (x i)) -> forall is . Rel (x ^ is) where
+    Nil  : Pointwise rel {is = Nil} xs xs
+    (::) : forall b . {0 xs, ys : b ^ (i :: is)} -> {0 rel : (i : a) -> Rel (b i)}
+      -> (r : rel i (head xs) (head ys)) -> (rs : Pointwise rel {is} (tail xs) (tail ys))
+      -> Pointwise rel xs ys
+
+  public export
+  map : forall b . {0 r, s : (i : a) -> Rel (b i)}
+    -> ((i : a) -> {x, y : b i} -> r i x y -> s i x y)
+    -> {is : List a} -> {xs, ys : b ^ is} -> Pointwise r {is} xs ys -> Pointwise s {is} xs ys
+  map f []        = []
+  map f (r :: rs) = f _ r :: map f rs
+
+  public export
+  pwEqImpliesEqual : Pointwise (\_ => Equal) xs ys -> xs = ys
+  pwEqImpliesEqual []        = Refl
+  pwEqImpliesEqual (r :: rs) = trans
+    (sym $ consHeadTail _)
+    (trans (cong2 (::) r (pwEqImpliesEqual rs)) (consHeadTail _))
+
+  public export
+  equalImpliesPwEq : {is : List a} -> {0 xs, ys : b ^ is}
+    -> xs = ys -> Pointwise (\_ => Equal) {is} xs ys
+  equalImpliesPwEq {is = []}        Refl = []
+  equalImpliesPwEq {is = (x :: xs)} eq   = cong head eq :: equalImpliesPwEq (cong tail eq)
+
+  -- FIXME: work out how to expose interfaces
+
+  public export
+  pwRefl : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
+    -> ((i : a) -> Reflexive (x i) (rel i))
+    -> {is : List a} -> {xs : x ^ is} -> Pointwise rel xs xs
+  pwRefl f {xs = []}        = []
+  pwRefl f {xs = (x :: xs)} = reflexive :: pwRefl f
+
+  public export
+  pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
+    -> ((i : a) -> Symmetric (x i) (rel i))
+    -> {is : List a} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel ys xs
+  pwSym f []        = []
+  pwSym f (r :: rs) = symmetric r :: pwSym f rs
+
+  public export
+  pwTrans : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
+    -> ((i : a) -> Transitive (x i) (rel i))
+    -> {is : List a} -> {xs, ys, zs : x ^ is}
+    -> Pointwise rel xs ys -> Pointwise rel ys zs -> Pointwise rel xs zs
+  pwTrans f []        []        = []
+  pwTrans f (r :: rs) (s :: ss) = transitive r s :: pwTrans f rs ss