diff options
Diffstat (limited to 'src/Soat/Data/Product.idr')
| -rw-r--r-- | src/Soat/Data/Product.idr | 79 |
1 files changed, 35 insertions, 44 deletions
diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr index 0cb5dda..1532d4b 100644 --- a/src/Soat/Data/Product.idr +++ b/src/Soat/Data/Product.idr @@ -1,7 +1,6 @@ module Soat.Data.Product import Data.List.Elem -import Data.Morphism.Indexed import Data.Setoid.Indexed %default total @@ -68,7 +67,7 @@ map f [] = [] map f (x :: xs) = f _ x :: map f xs public export -indexMap : {0 f : IFunc x y} -> (xs : x ^ is) -> (elem : Elem i is) +indexMap : forall x, y . {0 f : (i : a) -> x i -> y i} -> (xs : x ^ is) -> (elem : Elem i is) -> index (map f xs) elem = f i (index xs elem) indexMap (x :: xs) Here = Refl indexMap (x :: xs) (There elem) = indexMap xs elem @@ -79,8 +78,8 @@ mapId [] = Refl mapId (x :: xs) = cong ((::) x) $ mapId xs public export -mapComp : {0 f : IFunc y z} -> {0 g : IFunc x y} -> (xs : x ^ is) - -> map (\i => f i . g i) xs = map f (map g xs) +mapComp : forall x, y, z . {0 f : (i : a) -> y i -> z i} -> {0 g : (i : a) -> x i -> y i} + -> (xs : x ^ is) -> map (\i => f i . g i) xs = map f (map g xs) mapComp [] = Refl mapComp (x :: xs) = cong ((::) (f _ (g _ x))) $ mapComp xs @@ -95,7 +94,7 @@ wrap f [] = [] wrap f (x :: xs) = x :: wrap f xs public export -mapWrap : {0 f : IFunc x y} -> (0 g : a -> b) -> (xs : (x . g) ^ is) +mapWrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b) -> (xs : (x . g) ^ is) -> map f (wrap g xs) = wrap g (map (\i => f (g i)) xs) mapWrap g [] = Refl mapWrap g (x :: xs) = cong ((::) (f (g _) x)) $ mapWrap g xs @@ -106,7 +105,8 @@ unwrap f {is = []} [] = [] unwrap f {is = (i :: is)} (x :: xs) = x :: unwrap f xs public export -mapUnwrap : {0 f : IFunc x y} -> (0 g : a -> b) -> {is : _} -> (xs : x ^ map g is) +mapUnwrap : forall x, y . {0 f : (i : b) -> x i -> y i} -> (0 g : a -> b) + -> {is : _} -> (xs : x ^ map g is) -> map (\i => f (g i)) {is} (unwrap g xs) = unwrap g {is} (map f xs) mapUnwrap g {is = []} [] = Refl mapUnwrap g {is = (i :: is)} (x :: xs) = cong (Product.(::) (f (g i) x)) $ mapUnwrap g xs @@ -148,89 +148,80 @@ namespace Pointwise -- Relational Properties - 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 : {xs, ys : b ^ is} -> xs = ys -> Pointwise (\_ => Equal) xs ys equalImpliesPwEq {xs = []} {ys = []} eq = [] equalImpliesPwEq {xs = (x :: xs)} {ys = (y :: ys)} 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 - + -> ((i : a) -> (u : x i) -> rel i u u) + -> {is : List a} -> (xs : x ^ is) -> Pointwise rel xs xs + pwRefl refl [] = [] + pwRefl refl (x :: xs) = refl _ x :: pwRefl refl xs - public export - pwReflexive : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)} - -> ((i : a) -> Reflexive (x i) (rel i)) - -> {is : List a} -> {xs, ys : x ^ is} -> xs = ys -> Pointwise rel xs ys - pwReflexive refl Refl = pwRefl refl - - public export pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)} - -> ((i : a) -> Symmetric (x i) (rel i)) + -> ((i : a) -> (u, v : x i) -> rel i u v -> rel i v u) -> {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 + pwSym sym [] = [] + pwSym sym (r :: rs) = sym _ _ _ r :: pwSym sym rs - public export pwTrans : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)} - -> ((i : a) -> Transitive (x i) (rel i)) + -> ((i : a) -> (u, v, w : x i) -> rel i u v -> rel i v w -> rel i u w) -> {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 + pwTrans trans [] [] = [] + pwTrans trans (r :: rs) (s :: ss) = trans _ _ _ _ r s :: pwTrans trans rs ss public export - pwEquivalence : IEquivalence x rel -> {is : _} -> Setoid.Equivalence (x ^ is) (Pointwise rel) - pwEquivalence eq = MkEquivalence - (MkReflexive $ pwRefl (\i => (eq i).refl)) - (MkSymmetric $ pwSym (\i => (eq i).sym)) - (MkTransitive $ pwTrans (\i => (eq i).trans)) + pwEquivalence : IndexedEquivalence a x -> IndexedEquivalence (List a) ((^) x) + pwEquivalence eq = MkIndexedEquivalence + { relation = \_ => Pointwise eq.relation + , reflexive = \_ => pwRefl eq.reflexive + , symmetric = \_, _, _ => pwSym eq.symmetric + , transitive = \_, _, _, _ => pwTrans eq.transitive + } public export - pwSetoid : ISetoid a -> List a -> Setoid - pwSetoid x is = MkSetoid (x.U ^ is) _ (pwEquivalence x.equivalence) + pwSetoid : IndexedSetoid a -> IndexedSetoid (List a) + pwSetoid x = MkIndexedSetoid ((^) x.U) (pwEquivalence x.equivalence) -- Introductors and Eliminators public export - mapIntro'' : forall x, y . {0 rel : IRel x} -> {0 rel' : IRel y} -> {0 f, g : IFunc x y} + mapIntro'' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)} + -> {0 f, g : (i : a) -> x i -> y i} -> (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} + mapIntro' : forall x, y . {0 rel : (i : a) -> Rel (x i)} -> {0 rel' : (i : a) -> Rel (y i)} + -> {0 f, g : (i : a) -> x i -> y i} -> (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 + mapIntro : (f : x ~> y) -> {is : _} -> {xs, ys : x.U ^ is} + -> Pointwise x.equivalence.relation xs ys + -> Pointwise y.equivalence.relation (map f.H xs) (map f.H ys) + mapIntro f = mapIntro' f.homomorphic public export - wrapIntro : forall f . {0 rel : IRel x} -> {0 xs, ys : (x . f) ^ is} + wrapIntro : forall f . {0 rel : (i : a) -> Rel (x i)} -> {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} + unwrapIntro : forall f . {0 rel : (i : b) -> Rel (x i)} -> {is : _} -> {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 |