Introduce more equational reasoning.

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
   }