Define introductors for Pointwise.

1 files changed, 32 insertions, 0 deletions

diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index b20523a..1582d02 100644
--- a/src/Soat/Data/Product.idr
+++ b/src/Soat/Data/Product.idr
@@ -191,3 +191,35 @@ namespace Pointwise
     -> 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
+
+  -- Introductors and Eliminators
+
+  public export
+  mapIntro'' : forall x, y . {0 rel : IRel x} -> {0 rel' : IRel y} -> {0 f, g : IFunc x y}
+    -> (cong : (i : a) -> (u, v : x i) -> rel i u v -> rel' i (f i u) (g i v))
+    -> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys)
+  mapIntro'' cong []        = []
+  mapIntro'' cong (r :: rs) = cong _ _ _ r :: mapIntro'' cong rs
+
+  public export
+  mapIntro' : forall x, y . {0 rel : IRel x} -> {0 rel' : IRel y} -> {0 f, g : IFunc x y}
+    -> (cong : (i : a) -> {u, v : x i} -> rel i u v -> rel' i (f i u) (g i v))
+    -> {is : _} -> {xs, ys : x ^ is} -> Pointwise rel xs ys -> Pointwise rel' (map f xs) (map g ys)
+  mapIntro' cong = mapIntro'' (\t, _, _ => cong t)
+
+  public export
+  mapIntro : (f : IFunction x y) -> {is : _} -> {xs, ys : x.U ^ is}
+    -> Pointwise x.relation xs ys -> Pointwise y.relation (map f.func xs) (map f.func ys)
+  mapIntro f = mapIntro' f.cong
+
+  public export
+  wrapIntro : forall f . {0 rel : IRel x} -> {0 xs, ys : (x . f) ^ is}
+    -> Pointwise (\i => rel (f i)) xs ys -> Pointwise rel (wrap f xs) (wrap f ys)
+  wrapIntro []        = []
+  wrapIntro (r :: rs) = r :: wrapIntro rs
+
+  public export
+  unwrapIntro : {0 f : a -> b} -> {0 rel : IRel x} -> {is : List a} -> {0 xs, ys : x ^ map f is}
+    -> Pointwise rel xs ys -> Pointwise (\i => rel (f i)) {is = is} (unwrap f xs) (unwrap f ys)
+  unwrapIntro {is = []}        []        = []
+  unwrapIntro {is = (i :: is)} (r :: rs) = r :: unwrapIntro rs