summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Soat/FirstOrder/Algebra/Coproduct.idr224
1 files changed, 224 insertions, 0 deletions
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
new file mode 100644
index 0000000..d0b1b14
--- /dev/null
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -0,0 +1,224 @@
+module Soat.FirstOrder.Algebra.Coproduct
+
+import Data.Morphism.Indexed
+import Data.Setoid.Indexed
+import Data.Setoid.Either
+
+import Soat.FirstOrder.Algebra
+import Soat.FirstOrder.Signature
+import Soat.FirstOrder.Term
+
+import Syntax.PreorderReasoning.Setoid
+
+%default total
+
+public export
+CoproductSet : (0 sig : Signature) -> (0 x, y : sig.T -> Type) -> sig.T -> Type
+CoproductSet sig x y = Term sig (\i => Either (x i) (y i))
+
+public export
+data (~=~) : (0 x, y : RawAlgebraWithRelation sig) -> IRel (CoproductSet sig x.raw.U y.raw.U) where
+ DoneL : {0 x, y : RawAlgebraWithRelation sig}
+ -> {t : sig.T} -> {i, j : x.raw.U t} -> x.relation t i j
+ -> (~=~) x y t (Done $ Left i) (Done $ Left j)
+ DoneR : {0 x, y : RawAlgebraWithRelation sig}
+ -> {t : sig.T} -> {i, j : y.raw.U t} -> y.relation t i j
+ -> (~=~) x y t (Done $ Right i) (Done $ Right j)
+ Call : {t : sig.T} -> (op : Op sig t) -> {xs, ys : _} -> Pointwise ((~=~) x y) xs ys
+ -> (~=~) x y t (Call op xs) (Call op ys)
+ InjectL : {t : sig.T} -> (op : Op sig t) -> (xs : _)
+ -> (~=~) x y t (Done $ Left $ x.raw.sem op xs) (Call op (map (\_ => Done . Left) xs))
+ InjectR : {t : sig.T} -> (op : Op sig t) -> (xs : _)
+ -> (~=~) x y t (Done $ Right $ y.raw.sem op xs) (Call op (map (\_ => Done . Right) xs))
+ Sym : {0 x, y : RawAlgebraWithRelation sig} -> {t : sig.T} -> {tm, tm' : _}
+ -> (~=~) x y t tm tm' -> (~=~) x y t tm' tm
+ Trans : {0 x, y : RawAlgebraWithRelation sig} -> {t : sig.T} -> {tm, tm', tm'' : _}
+ -> (~=~) x y t tm tm' -> (~=~) x y t tm' tm'' -> (~=~) x y t tm tm''
+
+parameters {0 x, y : RawAlgebraWithRelation sig}
+ coprodRelRefl : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation
+ -> {t : _} -> (tm : _) -> (~=~) x y t tm tm
+ coprodsRelRefl : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation
+ -> {ts : _} -> (tms : _ ^ ts) -> Pointwise ((~=~) x y) tms tms
+
+ coprodRelRefl x y (Done (Left i)) = DoneL $ reflexive @{x _}
+ coprodRelRefl x y (Done (Right i)) = DoneR $ reflexive @{y _}
+ coprodRelRefl x y (Call op ts) = Call op $ coprodsRelRefl x y ts
+
+ coprodsRelRefl x y [] = []
+ coprodsRelRefl x y (t :: ts) = coprodRelRefl x y t :: coprodsRelRefl x y ts
+
+ coprodsRelReflexive : IReflexive x.raw.U x.relation -> IReflexive y.raw.U y.relation
+ -> {ts : _} -> {tms, tms' : _ ^ ts} -> tms = tms' -> Pointwise ((~=~) x y) tms tms'
+ coprodsRelReflexive x y Refl = coprodsRelRefl x y _
+
+ tmRelImpliesCoprodRel : Term.Rel.(~=~) (\i => Either (x.relation i) (y.relation i)) t tm tm'
+ -> (~=~) x y t tm tm'
+ tmRelsImpliesCoprodRels : {0 tms, tms' : _ ^ ts}
+ -> Pointwise (Term.Rel.(~=~) (\i => Either (x.relation i) (y.relation i))) tms tms'
+ -> Pointwise ((~=~) x y) tms tms'
+
+ tmRelImpliesCoprodRel (Done' (Left eq)) = DoneL eq
+ tmRelImpliesCoprodRel (Done' (Right eq)) = DoneR eq
+ tmRelImpliesCoprodRel (Call' op eqs) = Call op $ tmRelsImpliesCoprodRels eqs
+
+ tmRelsImpliesCoprodRels [] = []
+ tmRelsImpliesCoprodRels (eq :: eqs) = tmRelImpliesCoprodRel eq :: tmRelsImpliesCoprodRels eqs
+
+public export
+Coproduct : (x, y : RawAlgebra sig) -> RawAlgebra sig
+Coproduct x y = MakeRawAlgebra
+ { U = CoproductSet sig x.U y.U
+ , sem = Call
+ }
+
+public export
+CoproductIsAlgebra : IsAlgebra sig x rel -> IsAlgebra sig y rel'
+ -> IsAlgebra sig (Coproduct x y)
+ ((~=~) (MkRawAlgebraWithRelation x rel) (MkRawAlgebraWithRelation y rel'))
+CoproductIsAlgebra xIsAlgebra yIsAlgebra = MkIsAlgebra
+ { equivalence = \t => MkEquivalence
+ { refl = MkReflexive $ coprodRelRefl
+ (\t => (xIsAlgebra.equivalence t).refl)
+ (\t => (yIsAlgebra.equivalence t).refl)
+ _
+ , sym = MkSymmetric $ Sym
+ , trans = MkTransitive $ Trans
+ }
+ , semCong = Call
+ }
+
+public export
+CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
+CoproductAlgebra x y = MkAlgebra _ _ $ CoproductIsAlgebra x.algebra y.algebra
+
+public export
+injectLIsHomo : IsHomomorphism x (CoproductAlgebra x y) (\_ => Done . Left)
+injectLIsHomo = MkIsHomomorphism
+ { cong = \_ => DoneL
+ , semHomo = InjectL
+ }
+
+public export
+injectRIsHomo : IsHomomorphism y (CoproductAlgebra x y) (\_ => Done . Right)
+injectRIsHomo = MkIsHomomorphism
+ { cong = \_ => DoneR
+ , semHomo = InjectR
+ }
+
+public export
+injectLHomo : Homomorphism x (CoproductAlgebra x y)
+injectLHomo = MkHomomorphism _ $ injectLIsHomo
+
+public export
+injectRHomo : Homomorphism y (CoproductAlgebra x y)
+injectRHomo = MkHomomorphism _ $ injectRIsHomo
+
+public export
+coproduct : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> IFunc (CoproductSet sig x y) z.U
+coproduct f g _ = bindTerm (\i => either (f i) (g i))
+
+public export
+coproducts : {z : RawAlgebra sig} -> IFunc x z.U -> IFunc y z.U -> (ts : _)
+ -> CoproductSet sig x y ^ ts -> z.U ^ ts
+coproducts f g _ = bindTerms (\i => either (f i) (g i))
+
+public export
+coproductCong : {x, y, z : Algebra sig}
+ -> (f : Homomorphism x z) -> (g : Homomorphism y z)
+ -> (t : sig.T) -> {tm, tm' : _} -> (~=~) x.rawWithRelation y.rawWithRelation t tm tm'
+ -> (z.relation t `on` coproduct {z = z.raw} f.func g.func t) tm tm'
+
+public export
+coproductsCong : {x, y, z : Algebra sig}
+ -> (f : Homomorphism x z) -> (g : Homomorphism y z)
+ -> (ts : List sig.T) -> {tms, tms' : _ ^ ts}
+ -> Pointwise ((~=~) x.rawWithRelation y.rawWithRelation) tms tms'
+ -> (Pointwise z.relation `on` (coproducts {z = z.raw} f.func g.func ts)) tms tms'
+
+coproductCong f g _ (DoneL eq) = f.homo.cong _ eq
+coproductCong f g _ (DoneR eq) = g.homo.cong _ eq
+coproductCong f g _ (Call op eqs) =
+ z.algebra.semCong op $
+ coproductsCong f g _ eqs
+coproductCong f g _ (InjectL op ts) = CalcWith (z.setoid.index _) $
+ |~ f.func _ (x.raw.sem op ts)
+ ~~ z.raw.sem op (map f.func ts) ...(f.homo.semHomo op ts)
+ ~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Left) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
+ ~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Left) ts)) .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
+coproductCong f g _ (InjectR op ts) = CalcWith (z.setoid.index _) $
+ |~ g.func _ (y.raw.sem op ts)
+ ~~ z.raw.sem op (map g.func ts) ...(g.homo.semHomo op ts)
+ ~~ z.raw.sem op (map (coproduct f.func g.func) (map (\_ => Done . Right) ts)) .=.(cong (z.raw.sem op) $ mapComp ts)
+ ~~ z.raw.sem op (coproducts f.func g.func _ (map (\_ => Done . Right) ts)) .=<(cong (z.raw.sem op) $ bindTermsIsMap {a = z.raw} _ _)
+coproductCong f g _ (Sym eq) = (z.algebra.equivalence _).symmetric $ coproductCong f g _ eq
+coproductCong f g _ (Trans eq eq') = (z.algebra.equivalence _).transitive
+ (coproductCong f g _ eq)
+ (coproductCong f g _ eq')
+
+coproductsCong f g _ [] = []
+coproductsCong f g _ (eq :: eqs) =
+ coproductCong f g _ eq :: coproductsCong f g _ eqs
+
+public export
+coproductIsHomo : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z)
+ -> IsHomomorphism (CoproductAlgebra x y) z (coproduct {z = z.raw} f.func g.func)
+coproductIsHomo f g = MkIsHomomorphism
+ { cong = coproductCong f g
+ , semHomo = \op, tms =>
+ (z.algebra.equivalence _).equalImpliesEq $
+ cong (z.raw.sem op) $
+ bindTermsIsMap {a = z.raw} _ tms
+ }
+
+public export
+coproductHomo : {x, y, z : Algebra sig} -> Homomorphism x z -> Homomorphism y z
+ -> Homomorphism (CoproductAlgebra x y) z
+coproductHomo f g = MkHomomorphism _ $ coproductIsHomo f g
+
+public export
+termToCoproduct : (x, y : Algebra sig)
+ -> Homomorphism
+ (FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))))
+ (CoproductAlgebra x y)
+termToCoproduct x y = MkHomomorphism (\_ => id) $ MkIsHomomorphism
+ { cong = \t => tmRelImpliesCoprodRel
+ , semHomo = \op, tms =>
+ Call op $
+ coprodsRelReflexive
+ (\i => (x.algebra.equivalence i).refl)
+ (\i => (y.algebra.equivalence i).refl) $
+ sym $
+ mapId tms
+ }
+
+public export
+coproductUnique' : {x, y, z : Algebra sig}
+ -> (f : Homomorphism (CoproductAlgebra x y) z)
+ -> (g : Homomorphism (CoproductAlgebra x y) z)
+ -> (congL : {t : sig.T} -> (i : x.raw.U t)
+ -> z.relation t (f.func t (Done (Left i))) (g.func t (Done (Left i))))
+ -> (congR : {t : sig.T} -> (i : y.raw.U t)
+ -> z.relation t (f.func t (Done (Right i))) (g.func t (Done (Right i))))
+ -> {t : sig.T} -> (tm : _)
+ -> z.relation t (f.func t tm) (g.func t tm)
+coproductUnique' f g congL congR tm = bindUnique'
+ { v = fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))
+ , f = compHomo f $ termToCoproduct x y
+ , g = compHomo g $ termToCoproduct x y
+ , cong = \x => case x of
+ (Left x) => congL x
+ (Right x) => congR x
+ , tm = tm
+ }
+
+public export
+coproductUnique : {x, y, z : Algebra sig} -> (f : Homomorphism x z) -> (g : Homomorphism y z)
+ -> (h : Homomorphism (CoproductAlgebra x y) z)
+ -> (congL : {t : sig.T} -> (i : x.raw.U t)
+ -> z.relation t (h.func t (Done (Left i))) (f.func t i))
+ -> (congR : {t : sig.T} -> (i : y.raw.U t)
+ -> z.relation t (h.func t (Done (Right i))) (g.func t i))
+ -> {t : sig.T} -> (tm : _)
+ -> z.relation t (h.func t tm) (coproduct {z = z.raw} f.func g.func t tm)
+coproductUnique f g h = coproductUnique' h (coproductHomo f g)
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 16:26:22 +0000