From df7df335a91878448a9f231c0af36f57874ccd4e Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 6 Dec 2022 13:41:09 +0000 Subject: refactor: split product setoid into a new module. --- soat.ipkg | 1 + src/Data/Product.idr | 106 ----------------------------- src/Data/Setoid/Product.idr | 107 ++++++++++++++++++++++++++++++ src/Soat/FirstOrder/Algebra.idr | 3 +- src/Soat/FirstOrder/Algebra/Coproduct.idr | 1 + src/Soat/FirstOrder/Term.idr | 1 + src/Soat/SecondOrder/Algebra.idr | 1 + src/Soat/SecondOrder/Algebra/Lift.idr | 1 + 8 files changed, 114 insertions(+), 107 deletions(-) create mode 100644 src/Data/Setoid/Product.idr diff --git a/soat.ipkg b/soat.ipkg index ed3a86d..8e66ad3 100644 --- a/soat.ipkg +++ b/soat.ipkg @@ -6,6 +6,7 @@ depends = setoid modules = Data.List.Sublist , Data.Product + , Data.Setoid.Product , Soat.FirstOrder.Algebra , Soat.FirstOrder.Algebra.Coproduct , Soat.FirstOrder.Signature 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 diff --git a/src/Data/Setoid/Product.idr b/src/Data/Setoid/Product.idr new file mode 100644 index 0000000..90510e5 --- /dev/null +++ b/src/Data/Setoid/Product.idr @@ -0,0 +1,107 @@ +module Data.Setoid.Product + +import Data.List.Elem +import public Data.Product +import Data.Setoid.Indexed + +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 diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr index 876958f..97b6adc 100644 --- a/src/Soat/FirstOrder/Algebra.idr +++ b/src/Soat/FirstOrder/Algebra.idr @@ -1,7 +1,8 @@ module Soat.FirstOrder.Algebra -import public Data.Product +import Data.Product import Data.Setoid.Indexed +import Data.Setoid.Product import Soat.FirstOrder.Signature diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr index a8e4c0e..88db184 100644 --- a/src/Soat/FirstOrder/Algebra/Coproduct.idr +++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr @@ -2,6 +2,7 @@ module Soat.FirstOrder.Algebra.Coproduct import Data.Setoid.Indexed import Data.Setoid.Either +import Data.Setoid.Product import Soat.FirstOrder.Algebra import Soat.FirstOrder.Signature diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 00f7686..ee17093 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -2,6 +2,7 @@ module Soat.FirstOrder.Term import Data.Product import Data.Setoid.Indexed +import Data.Setoid.Product import Soat.FirstOrder.Algebra import Soat.FirstOrder.Signature diff --git a/src/Soat/SecondOrder/Algebra.idr b/src/Soat/SecondOrder/Algebra.idr index 95e5868..e7927ae 100644 --- a/src/Soat/SecondOrder/Algebra.idr +++ b/src/Soat/SecondOrder/Algebra.idr @@ -4,6 +4,7 @@ import Data.List.Elem import Data.List.Sublist import Data.Product import Data.Setoid.Indexed +import Data.Setoid.Product import Soat.SecondOrder.Signature diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr index 93043c4..116b5e4 100644 --- a/src/Soat/SecondOrder/Algebra/Lift.idr +++ b/src/Soat/SecondOrder/Algebra/Lift.idr @@ -4,6 +4,7 @@ import Data.List.Elem import Data.List.Sublist import Data.Product import Data.Setoid.Indexed +import Data.Setoid.Product import Soat.FirstOrder.Algebra import Soat.FirstOrder.Term -- cgit v1.2.3