diff options
Diffstat (limited to 'src/Data/Product.idr')
| -rw-r--r-- | src/Data/Product.idr | 106 |
1 files changed, 0 insertions, 106 deletions
diff --git a/src/Data/Product.idr b/src/Data/Product.idr index 348fa44..f1b5cc2 100644 --- a/src/Data/Product.idr +++ b/src/Data/Product.idr @@ -1,7 +1,6 @@ module Data.Product import Data.List.Elem -import Data.Setoid.Indexed %default total @@ -120,108 +119,3 @@ 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 |