From 1e64c562ad58d0fb264a11f11bc32b9311e728c4 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 6 Dec 2022 13:33:06 +0000 Subject: refactor: rename Soat.Data -> Data. --- src/Soat/Data/Product.idr | 227 ---------------------------------------------- 1 file changed, 227 deletions(-) delete mode 100644 src/Soat/Data/Product.idr (limited to 'src/Soat/Data/Product.idr') diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr deleted file mode 100644 index 1532d4b..0000000 --- a/src/Soat/Data/Product.idr +++ /dev/null @@ -1,227 +0,0 @@ -module Soat.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 -- cgit v1.2.3