diff options
| -rw-r--r-- | soat.ipkg | 1 | ||||
| -rw-r--r-- | src/Soat/SecondOrder/Algebra/Lift.idr | 361 |
2 files changed, 362 insertions, 0 deletions
@@ -9,5 +9,6 @@ modules = Soat.Data.Product , Soat.FirstOrder.Term , Soat.Relation , Soat.SecondOrder.Algebra + , Soat.SecondOrder.Algebra.Lift , Soat.SecondOrder.Signature , Soat.SecondOrder.Signature.Lift diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr new file mode 100644 index 0000000..00d453a --- /dev/null +++ b/src/Soat/SecondOrder/Algebra/Lift.idr @@ -0,0 +1,361 @@ +module Soat.SecondOrder.Algebra.Lift + +import Data.List.Elem + +import Soat.Data.Product +import Soat.Data.Sublist +import Soat.FirstOrder.Algebra +import Soat.FirstOrder.Term +import Soat.Relation +import Soat.SecondOrder.Algebra +import Soat.SecondOrder.Signature.Lift + +%default total + +public export +project : SecondOrder.Algebra.RawAlgebra (lift sig) -> (ctx : List sig.T) + -> FirstOrder.Algebra.RawAlgebra sig +project a ctx = MakeRawAlgebra + (flip a.U ctx) + (\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair [])) + +public export +projectIsAlgebra : {a : _} -> forall rel . SecondOrder.Algebra.IsAlgebra (lift sig) a rel + -> (ctx : List sig.T) + -> FirstOrder.Algebra.IsAlgebra sig (project a ctx) (\t => rel (t, ctx)) +projectIsAlgebra a ctx = MkIsAlgebra + (\t => a.equivalence (t, ctx)) + (\op => a.semCong ctx _ . wrapIntro) + +public export +projectAlgebra : SecondOrder.Algebra.Algebra (lift sig) -> (ctx : List sig.T) + -> FirstOrder.Algebra.Algebra sig +projectAlgebra a ctx = MkAlgebra _ _ (projectIsAlgebra a.algebra ctx) + +public export +projectIsHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> {f : _} -> IsHomomorphism a b f + -> (ctx : _) + -> IsHomomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx) (\t => f t ctx) +projectIsHomo {b = b} f ctx = MkIsHomomorphism + (\t => f.cong t ctx) + (\op, tms => + (b.algebra.equivalence _).transitive + (f.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms)) $ + b.algebra.semCong ctx (MkOp (Op op.op)) $ + map (\(_,_) => (b.algebra.equivalence _).equalImpliesEq) $ + equalImpliesPwEq $ + mapWrap (MkPair []) tms) + +public export +projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> Homomorphism a b + -> (ctx : _) -> Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra b ctx) +projectHomo f ctx = MkHomomorphism (\t => f.func t ctx) (projectIsHomo f.homo ctx) + +public export +(.renameHomo) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> {ctx, ctx' : _} + -> (f : ctx `Sublist` ctx') + -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx) (projectAlgebra a ctx') +(.renameHomo) a f = MkHomomorphism + (\t => a.raw.rename t f) + (MkIsHomomorphism + (\t => a.algebra.renameCong t f) + (\op, tms => (a.algebra.equivalence _).transitive + (a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms)) + (a.algebra.semCong _ (MkOp (Op op.op)) $ + map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $ + pwSym (\_ => MkSymmetric symmetric) $ + pwTrans (\_ => MkTransitive transitive) + (wrapIntro $ + mapIntro'' (\t, tm, _, Refl => + cong (\f => a.raw.rename t f tm) $ + sym $ + uncurryCurry f) $ + equalImpliesPwEq Refl) $ + equalImpliesPwEq $ + sym $ + mapWrap (MkPair []) tms))) + +public export +(.substHomo1) : (a : SecondOrder.Algebra.Algebra (lift sig)) -> (ctx : List sig.T) + -> {ctx' : List sig.T} -> (tms : (\t => a.raw.U t ctx) ^ ctx') + -> FirstOrder.Algebra.Homomorphism {sig = sig} (projectAlgebra a ctx') (projectAlgebra a ctx) +(.substHomo1) a ctx tms = MkHomomorphism + (\t, tm => a.raw.subst t ctx tm tms) + (MkIsHomomorphism + (\t, eq => a.algebra.substCong t ctx eq $ pwRefl (\_ => (a.algebra.equivalence _).refl)) + (\op, tms' => (a.algebra.equivalence _).transitive + (a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms) + (a.algebra.semCong ctx (MkOp (Op op.op)) $ + pwSym (\(_,_) => (a.algebra.equivalence _).sym) $ + pwTrans (\(_,_) => (a.algebra.equivalence _).trans) + (pwSym (\(_,_) => (a.algebra.equivalence _).sym) $ + wrapIntro $ + mapIntro'' (\t, tm, _, Refl => + a.algebra.substCong t ctx (a.algebra.equivalence _).reflexive $ + pwTrans (\_ => (a.algebra.equivalence _).trans) + (mapIntro'' (\t, tm, _, Refl => (a.algebra.equivalence _).transitive + ((a.algebra.equivalence _).equalImpliesEq $ + cong (\f => a.raw.rename t f tm) $ + uncurryCurry reflexive) + (a.algebra.renameId _ _ tm)) $ + equalImpliesPwEq Refl) $ + map (\_ => (a.algebra.equivalence _).equalImpliesEq) $ + equalImpliesPwEq $ + mapId tms) $ + equalImpliesPwEq Refl) $ + map (\(_,_) => (a.algebra.equivalence _).equalImpliesEq) $ + equalImpliesPwEq $ + sym $ + mapWrap (MkPair []) tms'))) + +renameBodyFunc : (f : ctx `Sublist` ctx') + -> IFunction + (isetoid (flip Elem ctx)) + (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx'))).setoid +renameBodyFunc f = MkIFunction (\_ => Done . curry f) (\_ => Done' . cong (curry f)) + +indexFunc : {ctx : List sig.T} -> (tms : Term sig (flip Elem ctx) ^ ts) + -> IFunction + (isetoid (flip Elem ts)) + (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx))).setoid +indexFunc tms = MkIFunction + (\_ => index tms) + (\_ => ((FreeIsAlgebra (isetoid (flip Elem _))).equivalence _).equalImpliesEq . cong (index tms)) + +-- renameFunc : (f : ctx `Sublist` ctx') +-- -> IFunction +-- (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx))).setoid +-- (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx'))).setoid +-- renameFunc f = MkIFunction +-- (\_ => bindTerm {a = Free _} (renameBodyFunc f).func) +-- (\t => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f)) + +public export +Initial : (0 sig : _) -> SecondOrder.Algebra.RawAlgebra (lift sig) +Initial sig = MakeRawAlgebra + (\t, ctx => Term sig (flip Elem ctx) t) + (\t, f => bindTerm {a = Free _} (renameBodyFunc f).func) + (\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair [])) + Done + (\_, _, t, ts => bindTerm {a = Free _} (\_ => index ts) t) + +public export +InitialIsAlgebra : (0 sig : _) + -> SecondOrder.Algebra.IsAlgebra + (lift sig) + (Initial sig) + (\(t, ctx) => (~=~) {sig = sig} {v = flip Elem ctx} (\_ => Equal) t) +InitialIsAlgebra sig = MkIsAlgebra + (\(t, ctx) => tmRelEq (\_ => equiv) t) + (\t, f => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f)) + (\_ , (MkOp (Op op)) => Call' (MkOp op) . unwrapIntro) + (\_, _, eq, eqs => bindTermCong' + {a = FreeAlgebra (isetoid (flip Elem _))} + (\t, Refl => index eqs _) + eq) + (\t, ctx, tm => + tmRelSym (\_ => MkSymmetric symmetric) $ + bindUnique (renameBodyFunc reflexive) idHomo (\i => Done' $ sym $ curryUncurry id i) $ + tm) + (\t, f, g, tm => + tmRelSym (\_ => MkSymmetric symmetric) $ + bindUnique + {a = FreeAlgebra (isetoid (flip Elem _))} + (renameBodyFunc (transitive g f)) + (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (renameBodyFunc g))) + (\i => Done' $ sym $ curryUncurry (curry f . curry g) i) $ + tm) + (\f, (MkOp (Op op)), tms => + Call' (MkOp op) $ + Pointwise.map (\_ => tmRelReflexive (\_ => MkReflexive reflexive)) $ + pwTrans (\_ => MkTransitive transitive) (equalImpliesPwEq $ bindTermsIsMap {a = Free _} _ _) $ + pwTrans (\_ => MkTransitive transitive) + (mapIntro' (\t, eq => + tmRelEqualIsEqual $ + bindTermCong' + {rel = \_ => Equal} + {a = FreeAlgebra (isetoid (flip Elem _))} + (\_, Refl => Done' $ sym $ curryUncurry (curry f) _) $ + tmRelReflexive (\_ => MkReflexive reflexive) $ + eq) $ + equalImpliesPwEq Refl) $ + equalImpliesPwEq $ + mapUnwrap _ _) + -- Pointwise.map (\_ => tmRelReflexive (\_ => MkReflexive reflexive)) $ + -- transitive (equalImpliesPwEq $ bindTermsIsMap {a = Free _} _ (unwrap (MkPair []) tms)) $ + -- transitive + -- (mapIntro + -- (\t, eq => + -- bindTermCong' + -- {v = isetoid (flip Elem _)} + -- {a = FreeAlgebra (isetoid (flip Elem _))} + -- (\_, Refl => Done' $ sym $ curryUncurry (curry f) _) $ + -- tmRelReflexive (\_ => MkReflexive reflexive) $ + -- eq) $ + -- equalImpliesPwEq Refl) $ + -- equalImpliesPwEq $ + -- mapUnwrap + -- (MkPair []) + -- (\ty => (renameFunc (reflexive ++ f)).func (snd ty)) + -- tms) + (\_, _ => Done' Refl) + (\t, f, tm, tms => + bindUnique + {a = FreeAlgebra (isetoid (flip Elem _))} + (indexFunc _) + (compHomo (bindHomo (renameBodyFunc f)) (bindHomo (indexFunc tms))) + (\i => + tmRelReflexive (\_ => MkReflexive reflexive) $ + sym $ + indexMap tms i) + tm) + (\t, ctx, f, tm, tms => + bindUnique + {a = FreeAlgebra (isetoid (flip Elem _))} + (indexFunc _) + (compHomo (bindHomo (indexFunc tms)) (bindHomo (renameBodyFunc f))) + (\i => + tmRelReflexive (\_ => MkReflexive reflexive) $ + sym $ + indexShuffle f i) + tm) + (\t, ctx, tm, tms, tms' => + bindUnique + {a = FreeAlgebra (isetoid (flip Elem _))} + (indexFunc _) + (compHomo (bindHomo (indexFunc tms')) (bindHomo (indexFunc tms))) + (\i => + tmRelReflexive (\_ => MkReflexive reflexive) $ + sym $ + indexMap tms i) + tm) + (\_, _, _ => tmRelRefl (\_ => MkReflexive reflexive) _) + (\t, ctx, tm => + tmRelSym (\_ => MkSymmetric symmetric) $ + bindUnique + {a = FreeAlgebra (isetoid (flip Elem _))} + (indexFunc _) + idHomo + (\i => + tmRelReflexive (\_ => MkReflexive reflexive) $ + sym $ + indexTabulate Done i) + tm) + (\ctx, (MkOp (Op op)), tms, tms' => + Call' (MkOp op) $ + tmsRelTrans (\_ => MkTransitive transitive) + (tmsRelSym (\_ => MkSymmetric symmetric) $ + bindsUnique + {a = FreeAlgebra (isetoid (flip Elem _))} + (indexFunc tms') + (bindHomo (indexFunc _)) + (\i => + (tmRelTrans (\_ => MkTransitive transitive) + (tmRelReflexive (\_ => MkReflexive reflexive) $ + indexMap + {f = (\_ => bindTerm {a = Free _} (\_ => Done . curry (uncurry (curry reflexive))))} + tms' + i) $ + tmRelSym (\_ => MkSymmetric symmetric) $ + (bindUnique + {a = FreeAlgebra (isetoid (flip Elem _))} + (renameBodyFunc _) + idHomo + (\i => + Done' $ + sym $ + transitive (curryUncurry (curry reflexive) i) (curryUncurry id i)) + (index tms' i)))) + (unwrap (MkPair []) tms)) $ + tmsRelReflexive (\_ => MkReflexive reflexive) $ + mapUnwrap _ _) + +public export +InitialAlgebra : (0 sig : _) -> SecondOrder.Algebra.Algebra (lift sig) +InitialAlgebra sig = MkAlgebra (Initial sig) _ (InitialIsAlgebra sig) + +public export +freeToInitialIsHomo : (0 sig : _) -> (ctx : List sig.T) + -> IsHomomorphism {sig = sig} + (FreeAlgebra (isetoid (flip Elem ctx))) + (projectAlgebra (InitialAlgebra sig) ctx) + (\_ => Basics.id) +freeToInitialIsHomo sig ctx = MkIsHomomorphism + (\_ => id) + (\(MkOp op), tms => + Call' (MkOp op) $ + tmsRelSym (\_ => MkSymmetric symmetric) $ + tmsRelReflexive (\_ => MkReflexive reflexive) $ + transitive (unwrapWrap _ _) (mapId tms)) + +public export +freeToInitialHomo : (0 sig : _) -> (ctx : List sig.T) + -> Homomorphism {sig = sig} + (FreeAlgebra (isetoid (flip Elem ctx))) + (projectAlgebra (InitialAlgebra sig) ctx) +freeToInitialHomo sig ctx = MkHomomorphism (\_ => id) (freeToInitialIsHomo sig ctx) + +public export +fromInitial : (a : SecondOrder.Algebra.RawAlgebra (lift sig)) -> (t : sig.T) -> (ctx : List sig.T) + -> (Initial sig).U t ctx -> a.U t ctx +fromInitial a t ctx = bindTerm {a = project a ctx} (\_ => a.var) + +public export +fromInitialIsHomo : (a : SecondOrder.Algebra.Algebra (lift sig)) + -> IsHomomorphism (InitialAlgebra sig) a (fromInitial a.raw) +fromInitialIsHomo a = MkIsHomomorphism + (\t , ctx => bindTermCong {a = projectAlgebra a ctx} (a.varFunc ctx)) + (\t, f => bindUnique' + {v = isetoid (flip Elem _)} + {a = projectAlgebra a _} + (compHomo (bindHomo (a.varFunc _)) (bindHomo (renameBodyFunc f))) + (compHomo (a.renameHomo f) (bindHomo (a.varFunc _))) + (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i)) + (\ctx, (MkOp (Op op)), tms => + a.algebra.semCong ctx (MkOp (Op op)) $ + map (\_ => (a.algebra.equivalence _).equalImpliesEq) $ + equalImpliesPwEq $ + transitive + (cong (wrap _) $ bindTermsIsMap {a = project a.raw _} (\_ => a.raw.var) $ unwrap _ tms) $ + transitive + (sym $ mapWrap (MkPair []) {f = \_ => fromInitial a.raw _ _} $ unwrap _ tms) $ + cong (map _) $ + wrapUnwrap tms) + (\_ => (a.algebra.equivalence _).reflexive) + (\t, ctx, tm, tms => bindUnique' + {v = isetoid (flip Elem _)} + {a = projectAlgebra a _} + (compHomo (bindHomo (a.varFunc _)) (bindHomo (indexFunc tms))) + (compHomo (a.substHomo1 ctx _) (bindHomo (a.varFunc _))) + (\i => + (a.algebra.equivalence _).transitive + (bindUnique + {v = isetoid (flip Elem _)} + {a = projectAlgebra a _} + (a.varFunc _) + (bindHomo (a.varFunc _)) + (\i => (a.algebra.equivalence _).reflexive) + (index tms i)) $ + (a.algebra.equivalence _).symmetric $ + (a.algebra.equivalence _).transitive + (a.algebra.substVarL ctx i _) $ + (a.algebra.equivalence _).equalImpliesEq $ + indexMap {f = \t => bindTerm {a = project a.raw ctx} (\_ => a.raw.var)} tms i) + tm) + +public export +fromInitialHomo : (a : SecondOrder.Algebra.Algebra (lift sig)) + -> Homomorphism (InitialAlgebra sig) a +fromInitialHomo a = MkHomomorphism (fromInitial a.raw) (fromInitialIsHomo a) + +public export +fromInitialUnique : {a : SecondOrder.Algebra.Algebra (lift sig)} + -> (f : Homomorphism (InitialAlgebra sig) a) + -> (t : sig.T) -> (ctx : List sig.T) -> (tm : Term sig (flip Elem ctx) t) + -> a.relation (t, ctx) (f.func t ctx tm) (fromInitial a.raw t ctx tm) +fromInitialUnique {sig = sig} {a = a} f t ctx = bindUnique + {v = isetoid (flip Elem _)} + {a = projectAlgebra a ctx} + (a.varFunc ctx) + (compHomo (projectHomo f ctx) (freeToInitialHomo sig ctx)) + f.homo.varHomo |