summaryrefslogtreecommitdiff
path: root/src/Soat/FirstOrder
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat/FirstOrder')
-rw-r--r--src/Soat/FirstOrder/Algebra.idr55
-rw-r--r--src/Soat/FirstOrder/Algebra/Coproduct.idr49
-rw-r--r--src/Soat/FirstOrder/Term.idr25
3 files changed, 52 insertions, 77 deletions
diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index b9c02c5..7bed448 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -53,52 +53,39 @@ public export
(.rawSetoid) a = MkRawSetoidAlgebra a.raw a.relation
public export
-record IsHomomorphism
- {0 sig : Signature} (a, b : Algebra sig)
- (f : (t : sig.T) -> a.raw.U t -> b.raw.U t)
- where
- constructor MkIsHomomorphism
- cong : (t : sig.T) -> {tm, tm' : a.raw.U t}
- -> a.relation t tm tm' -> b.relation t (f t tm) (f t tm')
- semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
- -> b.relation t (f t (a.raw.sem op tms)) (b.raw.sem op (map f tms))
-
-public export
record (~>) {0 sig : Signature} (a, b : Algebra sig)
where
constructor MkHomomorphism
- func : IFunc a.raw.U b.raw.U
- homo : IsHomomorphism a b func
+ func : (t : sig.T) -> a.raw.U t -> b.raw.U t
+ cong : (t : sig.T) -> {tm, tm' : a.raw.U t}
+ -> a.relation t tm tm' -> b.relation t (func t tm) (func t tm')
+ semHomo : {t : sig.T} -> (op : Op sig t) -> (tms : a.raw.U ^ op.arity)
+ -> b.relation t (func t (a.raw.sem op tms)) (b.raw.sem op (map func tms))
public export
-idIsHomo : {a : Algebra sig} -> IsHomomorphism a a (\_ => Basics.id)
-idIsHomo = MkIsHomomorphism
- (\_ => id)
- (\op, tms =>
+idHomo : {a : Algebra sig} -> a ~> a
+idHomo = MkHomomorphism
+ { func = \_ => id
+ , cong = \_ => id
+ , semHomo = \op, tms =>
(a.algebra.equivalence _).equalImpliesEq $
sym $
cong (a.raw.sem op) $
- mapId tms)
+ mapId tms
+ }
public export
-idHomo : {a : Algebra sig} -> a ~> a
-idHomo = MkHomomorphism _ idIsHomo
-
-public export
-compIsHomo : {a, b, c : Algebra sig} -> {f : IFunc b.raw.U c.raw.U} -> {g : IFunc a.raw.U b.raw.U}
- -> IsHomomorphism b c f -> IsHomomorphism a b g -> IsHomomorphism a c (\i => f i . g i)
-compIsHomo fHomo gHomo = MkIsHomomorphism
- (\t => fHomo.cong t . gHomo.cong t)
- (\op, tms =>
+compHomo : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
+compHomo f g = MkHomomorphism
+ { func = \t => f.func t . g.func t
+ , cong = \t => f.cong t . g.cong t
+ , semHomo = \op, tms =>
(c.algebra.equivalence _).transitive
- (fHomo.cong _ $ gHomo.semHomo op tms) $
+ (f.cong _ $ g.semHomo op tms) $
(c.algebra.equivalence _).transitive
- (fHomo.semHomo op (map g tms)) $
+ (f.semHomo op (map g.func tms)) $
(c.algebra.equivalence _).equalImpliesEq $
sym $
cong (c.raw.sem op) $
- mapComp tms)
-
-public export
-compHomo : {a, b, c : Algebra sig} -> b ~> c -> a ~> b -> a ~> c
-compHomo f g = MkHomomorphism _ $ compIsHomo f.homo g.homo
+ mapComp tms
+ }
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index 5e6d4ce..a98391b 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -96,28 +96,22 @@ CoproductAlgebra : (x, y : Algebra sig) -> Algebra sig
CoproductAlgebra x y = MkAlgebra (Coproduct x.raw y.raw) $ CoproductIsAlgebra x.algebra y.algebra
public export
-injectLIsHomo : IsHomomorphism x (CoproductAlgebra x y) (\_ => Done . Left)
-injectLIsHomo = MkIsHomomorphism
- { cong = \_ => DoneL
+injectLHomo : x ~> CoproductAlgebra x y
+injectLHomo = MkHomomorphism
+ { func = \_ => Done . Left
+ , cong = \_ => DoneL
, semHomo = InjectL
}
public export
-injectRIsHomo : IsHomomorphism y (CoproductAlgebra x y) (\_ => Done . Right)
-injectRIsHomo = MkIsHomomorphism
- { cong = \_ => DoneR
+injectRHomo : y ~> CoproductAlgebra x y
+injectRHomo = MkHomomorphism
+ { func = \_ => Done . Right
+ , cong = \_ => DoneR
, semHomo = InjectR
}
public export
-injectLHomo : x ~> CoproductAlgebra x y
-injectLHomo = MkHomomorphism _ $ injectLIsHomo
-
-public export
-injectRHomo : 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))
@@ -137,19 +131,19 @@ coproductsCong : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
-> Pointwise ((~=~) x.rawSetoid y.rawSetoid) 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 _ (DoneL eq) = f.cong _ eq
+coproductCong f g _ (DoneR eq) = g.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 f.func ts) ...(f.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 g.func ts) ...(g.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
@@ -162,10 +156,11 @@ coproductsCong f g _ (eq :: eqs) =
coproductCong f g _ eq :: coproductsCong f g _ eqs
public export
-coproductIsHomo : {x, y, z : Algebra sig} -> (f : x ~> z) -> (g : y ~> z)
- -> IsHomomorphism (CoproductAlgebra x y) z (coproduct {z = z.raw} f.func g.func)
-coproductIsHomo f g = MkIsHomomorphism
- { cong = coproductCong f g
+coproductHomo : {x, y, z : Algebra sig} -> x ~> z -> y ~> z
+ -> CoproductAlgebra x y ~> z
+coproductHomo f g = MkHomomorphism
+ { func = coproduct {z = z.raw} f.func g.func
+ , cong = coproductCong f g
, semHomo = \op, tms =>
(z.algebra.equivalence _).equalImpliesEq $
cong (z.raw.sem op) $
@@ -173,16 +168,12 @@ coproductIsHomo f g = MkIsHomomorphism
}
public export
-coproductHomo : {x, y, z : Algebra sig} -> x ~> z -> y ~> z
- -> CoproductAlgebra x y ~> z
-coproductHomo f g = MkHomomorphism _ $ coproductIsHomo f g
-
-public export
termToCoproduct : (x, y : Algebra sig)
-> FreeAlgebra (fromIndexed (\i => EitherSetoid (x.setoid.index i) (y.setoid.index i))) ~>
CoproductAlgebra x y
-termToCoproduct x y = MkHomomorphism (\_ => id) $ MkIsHomomorphism
- { cong = \t => tmRelImpliesCoprodRel
+termToCoproduct x y = MkHomomorphism
+ { func = \_ => id
+ , cong = \t => tmRelImpliesCoprodRel
, semHomo = \op, tms =>
Call op $
coprodsRelReflexive
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index bedfe3f..f9f0879 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -170,19 +170,16 @@ bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
bindTermsCong env = bindTermsCong' env.cong
public export
-bindIsHomo : (a : Algebra sig) -> (env : IFunction v a.setoid)
- -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.func)
-bindIsHomo a env = MkIsHomomorphism
- (\t, eq => bindTermCong env eq)
- (\op, tms =>
- a.algebra.semCong op $
- map (\t => (a.algebra.equivalence t).equalImpliesEq) $
- equalImpliesPwEq $
- bindTermsIsMap {a = a.raw} env.func tms)
-
-public export
bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> FreeAlgebra v ~> a
-bindHomo env = MkHomomorphism _ (bindIsHomo _ env)
+bindHomo env = MkHomomorphism
+ { func = \_ => bindTerm {a = a.raw} env.func
+ , cong = \_ => bindTermCong env
+ , semHomo = \op, tms =>
+ a.algebra.semCong op $
+ map (\t => (a.algebra.equivalence t).equalImpliesEq) $
+ equalImpliesPwEq $
+ bindTermsIsMap {a = a.raw} env.func tms
+ }
public export
bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
@@ -201,9 +198,9 @@ bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig}
bindUnique' f g cong (Done i) = cong i
bindUnique' f g cong (Call op ts) = CalcWith (a.setoid.index _) $
|~ f.func _ (Call op ts)
- ~~ a.raw.sem op (map f.func ts) ...( f.homo.semHomo op ts )
+ ~~ a.raw.sem op (map f.func ts) ...( f.semHomo op ts )
~~ a.raw.sem op (map g.func ts) ...( a.algebra.semCong op $ bindsUnique' f g cong ts )
- ~~ g.func _ (Call op ts) ..<( g.homo.semHomo op ts )
+ ~~ g.func _ (Call op ts) ..<( g.semHomo op ts )
bindsUnique' f g cong [] = []
bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g cong ts
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-29 21:34:14 +0000