summaryrefslogtreecommitdiff
path: root/src/Data/Product.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data/Product.idr')
-rw-r--r--src/Data/Product.idr227
1 files changed, 227 insertions, 0 deletions
diff --git a/src/Data/Product.idr b/src/Data/Product.idr
new file mode 100644
index 0000000..348fa44
--- /dev/null
+++ b/src/Data/Product.idr
@@ -0,0 +1,227 @@
+module Data.Product
+
+import Data.List.Elem
+import Data.Setoid.Indexed
+
+%default total
+
+infix 10 ^
+infix 5 ++
+
+-- 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
+
+-- Destructors
+
+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
+
+public export
+index : x ^ is -> Elem i is -> x i
+index xs Here = head xs
+index xs (There elem) = index (tail xs) elem
+
+-- Constructors
+
+public export
+tabulate : {is : List a} -> ({i : a} -> Elem i is -> x i) -> x ^ is
+tabulate {is = []} f = []
+tabulate {is = (i :: is)} f = f Here :: tabulate (f . There)
+
+public export
+indexTabulate : forall x . (0 f : {i : a} -> Elem i is -> x i) -> (elem : Elem i is)
+ -> index (tabulate f) elem = f elem
+indexTabulate f Here = Refl
+indexTabulate f (There elem) = indexTabulate (f . There) elem
+
+-- 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
+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
+
+public export
+mapId : (xs : x ^ is) -> map (\_ => Basics.id) xs = xs
+mapId [] = Refl
+mapId (x :: xs) = cong ((::) x) $ mapId xs
+
+public export
+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
+
+public export
+(++) : x ^ is -> x ^ js -> x ^ (is ++ js)
+(++) [] ys = ys
+(++) (x :: xs) ys = x :: (xs ++ ys)
+
+public export
+wrap : (0 f : a -> b) -> (x . f) ^ is -> x ^ map f is
+wrap f [] = []
+wrap f (x :: xs) = x :: wrap f xs
+
+public export
+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
+
+public export
+unwrap : (0 f : a -> b) -> {is : _} -> x ^ map f is -> (x . f) ^ is
+unwrap f {is = []} [] = []
+unwrap f {is = (i :: is)} (x :: xs) = x :: unwrap f xs
+
+public export
+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
+
+public export
+unwrapWrap : (0 x : a -> Type) -> (xs : (x . f) ^ is) -> unwrap f (wrap {x} f xs) = xs
+unwrapWrap u [] = Refl
+unwrapWrap u (x :: xs) = cong ((::) x) $ unwrapWrap u xs
+
+public export
+wrapUnwrap : {is : _} -> (xs : x ^ map f is) -> wrap f {is} (unwrap f xs) = xs
+wrapUnwrap {is = []} [] = Refl
+wrapUnwrap {is = (i :: is)} (x :: xs) = cong ((::) x) $ wrapUnwrap xs
+
+-- Relations
+
+namespace Pointwise
+ public export
+ data Pointwise : (0 _ : (i : a) -> Rel (x i)) -> forall is . Rel (x ^ is) where
+ Nil : Pointwise rel [] []
+ (::) : forall b, x, y . {0 xs, ys : b ^ is} -> {0 rel : (i : a) -> Rel (b i)}
+ -> (r : rel i x y) -> (rs : Pointwise rel xs ys) -> Pointwise rel (x :: xs) (y :: ys)
+
+ -- Destructors
+
+ public export
+ index : Pointwise rel xs ys -> (elem : Elem i is) -> rel i (index xs elem) (index ys elem)
+ index (r :: rs) Here = r
+ index (r :: rs) (There elem) = index rs elem
+
+ -- Operators
+
+ 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
+
+ -- Relational Properties
+
+ pwEqImpliesEqual : Pointwise (\_ => Equal) xs ys -> xs = ys
+ pwEqImpliesEqual [] = Refl
+ pwEqImpliesEqual (r :: rs) = trans
+ (sym $ consHeadTail _)
+ (trans (cong2 (::) r (pwEqImpliesEqual rs)) (consHeadTail _))
+
+ 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)
+
+ pwRefl : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x i)}
+ -> ((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
+
+ pwSym : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x 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 sym [] = []
+ pwSym sym (r :: rs) = sym _ _ _ r :: pwSym sym rs
+
+ pwTrans : {0 x : a -> Type} -> {0 rel : (i : a) -> Rel (x 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 trans [] [] = []
+ pwTrans trans (r :: rs) (s :: ss) = trans _ _ _ _ r s :: pwTrans trans rs ss
+
+ public export
+ 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 : IndexedSetoid a -> IndexedSetoid (List a)
+ pwSetoid x = MkIndexedSetoid ((^) x.U) (pwEquivalence x.equivalence)
+
+ -- Introductors and Eliminators
+
+ public export
+ 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 : (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 : 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 : (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 : 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
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 21:55:40 +0000