diff options
| -rw-r--r-- | src/Soat/SecondOrder/Algebra/Lift.idr | 206 |
1 files changed, 98 insertions, 108 deletions
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr index 463fa84..30bcd91 100644 --- a/src/Soat/SecondOrder/Algebra/Lift.idr +++ b/src/Soat/SecondOrder/Algebra/Lift.idr @@ -11,6 +11,8 @@ import Soat.FirstOrder.Term import Soat.SecondOrder.Algebra import Soat.SecondOrder.Signature.Lift +import Syntax.PreorderReasoning.Setoid + %default total public export @@ -37,13 +39,12 @@ projectHomo : {a, b : SecondOrder.Algebra.Algebra (lift sig)} -> a ~> b projectHomo f ctx = MkHomomorphism { func = \t => f.func t ctx , cong = \t => f.cong t ctx - , semHomo = \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 + , semHomo = \op, tms => CalcWith (b.setoid.index _) $ + |~ f.func _ ctx (a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) tms)) + ~~ b.raw.sem ctx (MkOp (Op op.op)) (map (extendFunc f.func ctx) (wrap (MkPair []) tms)) + ...(f.semHomo ctx (MkOp (Op op.op)) (wrap (MkPair []) tms)) + ~~ b.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => f.func t ctx) tms)) + .=.(cong (b.raw.sem ctx (MkOp (Op op.op))) $ mapWrap (MkPair []) {f = extendFunc f.func ctx} tms) } public export @@ -53,21 +54,21 @@ public export (.renameHomo) a f = MkHomomorphism { func = \t => a.raw.rename t f , cong = \t => a.algebra.renameCong t f - , semHomo = \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) + , semHomo = \op, tms => CalcWith (a.setoid.index _) $ + |~ a.raw.rename _ f (a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) tms)) + ~~ a.raw.sem _ (MkOp (Op op.op)) (map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms)) + ...(a.algebra.semNat f (MkOp (Op op.op)) (wrap (MkPair []) tms)) + ~~ a.raw.sem _ (MkOp (Op op.op)) (wrap (MkPair []) (map (\t => a.raw.rename t f) tms)) + ...(a.algebra.semCong _ (MkOp (Op op.op)) $ + CalcWith (pwSetoid (reindex (\ty => (snd ty, fst ty ++ _)) a.setoid) _) $ + |~ map (\ty => a.raw.rename (snd ty) (reflexive {x = fst ty} ++ f)) (wrap (MkPair []) tms) + ~~ wrap (MkPair []) (map (\t => a.raw.rename t (reflexive {x = []} ++ f)) tms) + .=.(mapWrap (MkPair []) tms) + ~~ wrap (MkPair []) (map (\t => a.raw.rename t f) tms) + .=.(cong (wrap (MkPair [])) $ + pwEqImpliesEqual $ + mapIntro'' (\t, tm, _, Refl => cong (\f => a.raw.rename t f tm) $ uncurryCurry f) $ + equalImpliesPwEq Refl)) } public export @@ -79,30 +80,32 @@ public export , cong = \t, eq => a.algebra.substCong t ctx eq $ pwRefl (\_ => (a.algebra.equivalence _).refl) - , semHomo = \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') + , semHomo = \op, tms' => CalcWith (a.setoid.index _) $ + |~ a.raw.subst _ ctx (a.raw.sem ctx' (MkOp (Op op.op)) (wrap (MkPair []) tms')) tms + ~~ a.raw.sem ctx (MkOp (Op op.op)) (map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms')) + ...(a.algebra.substCompat ctx (MkOp (Op op.op)) (wrap (MkPair []) tms') tms) + ~~ a.raw.sem ctx (MkOp (Op op.op)) (wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms')) + ...(a.algebra.semCong ctx (MkOp (Op op.op)) $ + CalcWith (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) _) $ + |~ map (a.raw.extendSubst ctx tms) (wrap (MkPair []) tms') + ~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm (map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms)) tms') + .=.(mapWrap (MkPair []) tms') + ~~ wrap (MkPair []) (map (\t, tm => a.raw.subst t ctx tm tms) tms') + ...(wrapIntro $ + mapIntro' (\t, eq => + a.algebra.substCong t ctx eq $ + CalcWith (pwSetoid (a.setoidAt _) _) $ + |~ map (\t => a.raw.rename t ([] {ys = []} ++ reflexive)) tms + ~~ map (\t => a.raw.rename t reflexive) tms + .=.(pwEqImpliesEqual $ + mapIntro' (\t => cong2 (a.raw.rename t) $ uncurryCurry reflexive) $ + equalImpliesPwEq Refl) + ~~ map (\t => id) tms + ...(mapIntro' (\t, Refl => a.algebra.renameId t ctx _) $ + equalImpliesPwEq Refl) + ~~ tms + .=.(mapId tms)) $ + pwRefl (\t => (a.algebra.equivalence _).refl))) } renameBodyFunc : (f : ctx `Sublist` ctx') @@ -153,20 +156,19 @@ InitialIsAlgebra sig = MkIsAlgebra tm , semNat = \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 _ _ + CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $ + |~ bindTerms {a = Free _} (\_ => Done . curry f) (unwrap (MkPair []) tms) + ~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry f)) (unwrap (MkPair []) tms) + .=.(bindTermsIsMap {a = Free _} _ _) + ~~ map (\_ => bindTerm {a = Free _} (\_ => Done . curry (reflexive {x = []} ++ f))) (unwrap (MkPair []) tms) + ..<(mapIntro' (\t => + bindTermCong' + {rel = \_ => Equal} + {a = FreeAlgebra (isetoid (flip Elem _))} + (\_, Refl => Done' $ curryUncurry (curry f) _)) $ + tmsRelRefl (\_ => MkReflexive reflexive) (unwrap (MkPair []) tms)) + ~~ unwrap (MkPair []) (map (\ty => bindTerm {a = Free _} (\_ => Done . curry (reflexive {x = fst ty} ++ f))) tms) + .=.(mapUnwrap (MkPair []) tms) , varNat = \_, _ => Done' Refl , substNat = \t, f, tm, tms => bindUnique @@ -212,32 +214,28 @@ InitialIsAlgebra sig = MkIsAlgebra tm , substCompat = \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 _) - id - (\i => - Done' $ - sym $ - transitive (curryUncurry (curry reflexive) i) (curryUncurry id i)) - (index tms' i)))) - (unwrap (MkPair []) tms)) $ - tmsRelReflexive (\_ => MkReflexive reflexive) $ - mapUnwrap _ _ + CalcWith (pwSetoid (FreeAlgebra (isetoid (flip Elem _))).setoid _) $ + |~ bindTerms {a = Free _} (\_ => index tms') (unwrap (MkPair []) tms) + ~~ map (\_ => bindTerm {a = Free _} (\_ => index tms')) (unwrap (MkPair []) tms) + .=.(bindTermsIsMap {a = Free _} _ _) + ~~ map (\t => (Initial sig).extendSubst ctx tms' ([], t)) (unwrap (MkPair []) tms) + ..<(mapIntro' (\t => bindTermCong' + {rel = \_ => Equal} + {a = FreeAlgebra (isetoid (flip Elem _))} + (\t, Refl => CalcWith ((FreeAlgebra (isetoid (flip Elem _))).setoid.index _) $ + |~ index (map (\_ => bindTerm {a = Free _} (\_ => Done . curry ([] {ys = []} ++ reflexive))) tms') _ + ~~ bindTerm {a = Free _} (\_ => Done . curry ([] {ys = []} ++ reflexive)) (index tms' _) + .=.(indexMap tms' _) + ~~ index tms' _ + ..<(bindUnique + (renameBodyFunc ([] {ys = []} ++ reflexive)) + id + (\i => Done' $ sym $ trans (curryUncurry _ i) (curryUncurry id i)) + (index tms' _)))) $ + tmsRelRefl (\_ => MkReflexive reflexive) $ + unwrap (MkPair []) tms) + ~~ unwrap (MkPair []) (map ((Initial sig).extendSubst ctx tms') tms) + .=.(mapUnwrap (MkPair []) tms) } public export @@ -275,34 +273,26 @@ fromInitialHomo a = MkHomomorphism (\i => (a.algebra.equivalence _).symmetric $ a.algebra.varNat f i) , semHomo = \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 + CalcWith (pwSetoid (reindex (\ty => (snd ty, fst ty ++ ctx)) a.setoid) _) $ + |~ wrap (MkPair []) (bindTerms {a = project a.raw ctx} (\_ => a.raw.var) (unwrap (MkPair []) tms)) + ~~ wrap (MkPair []) (map (\t => fromInitial a.raw t ctx) (unwrap (MkPair []) tms)) + .=.(cong (wrap _) $ bindTermsIsMap {a = project a.raw ctx} _ _) + ~~ wrap (MkPair []) (unwrap (MkPair []) (map (extendFunc (fromInitial a.raw) ctx) tms)) + .=.(cong (wrap _) $ mapUnwrap (MkPair []) tms) + ~~ map (extendFunc (fromInitial a.raw) ctx) tms + .=.(wrapUnwrap _) , varHomo = \_ => (a.algebra.equivalence _).reflexive , substHomo = \t, ctx, tm, tms => bindUnique' {v = isetoid (flip Elem _)} {a = projectAlgebra sig a _} (bindHomo (a.varFunc _) . bindHomo (indexFunc tms)) (a.substHomo1 ctx _ . bindHomo (a.varFunc _)) - (\i => - (a.algebra.equivalence _).transitive - (bindUnique - {v = isetoid (flip Elem _)} - {a = projectAlgebra sig 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) + (\i => CalcWith (a.setoid.index _) $ + |~ bindTerm {a = project a.raw _} (\_ => a.raw.var) (index tms i) + ~~ index (map (\_ => bindTerm {a = project a.raw _} (\_ => a.raw.var)) tms) i + .=<(indexMap {f = \_ => bindTerm {a = project a.raw _} (\_ => a.raw.var)} tms i) + ~~ a.raw.subst _ ctx (a.raw.var i) (map (\_ => bindTerm {a = project a.raw _} (\_ => a.raw.var)) tms) + ..<(a.algebra.substVarL ctx i _)) tm } |