Prove the term algebras form an initial algebra.

1 files changed, 361 insertions, 0 deletions

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