Tactic morphism

idris-ct.nix

@@ -27,6 +27,7 @@ idrisPackages.build-idris-package {
 
   idrisDeps = with idrisPackages; [
     contrib
+    pruviloj
   ];
 
   meta = {

src/Tactics.idr

@@ -0,0 +1,2 @@
+import public Pruviloj.Core
+import public Tactics.Morphism

src/Tactics/Morphism.idr

@@ -0,0 +1,98 @@
+module Tactics.Morphism
+
+-- The `morphism` tactic is defined here
+-- Note that in general, idris's inference algorithm needs help with it, so use it either as
+-- %runElab morphism
+-- or
+-- the (f = g) (%runElab morphism)
+
+import Basic.Category
+import Language.Reflection.Elab
+import Pruviloj.Core
+
+%language ElabReflection
+%access public export
+
+data MorphismExpr : (cat : Category) -> obj cat -> obj cat -> Type where
+  IdExpr : (a : obj cat) -> MorphismExpr cat a a
+  CompExpr : MorphismExpr cat a b -> MorphismExpr cat b c -> MorphismExpr cat a c
+  OtherExpr : mor cat a b -> MorphismExpr cat a b
+
+data MorphismPath : (cat : Category) -> obj cat -> obj cat -> Type where
+  Nil : MorphismPath cat a a
+  (::) : mor cat a b -> MorphismPath cat b c -> MorphismPath cat a c
+
+(++) : MorphismPath cat a b -> MorphismPath cat b c -> MorphismPath cat a c
+(++) [] q = q
+(++) (f :: fs) q = f :: (fs ++ q)
+
+unquoteExpr : MorphismExpr cat a b -> mor cat a b
+unquoteExpr (IdExpr a) = identity _ a
+unquoteExpr (CompExpr f g) = compose _ _ _ _ (unquoteExpr f) (unquoteExpr g)
+unquoteExpr (OtherExpr f) = f
+
+unquotePath : MorphismPath cat a b -> mor cat a b
+unquotePath [] = identity _ _
+unquotePath (f :: fs) = compose _ _ _ _ f (unquotePath fs)
+
+-- does the "heavy lifting" by converting to a canonical form, e.g.:
+-- assume f, g and h are morphisms
+-- exprToPath (CompExpr (OtherExpr f) (CompExpr (OtherExpr g) (OtherExpr h))) = [f, g, h]
+-- exprToPath (CompExpr (CompExpr (OtherExpr f) (OtherExpr g)) (OtherExpr h)) = [f, g, h]
+
+exprToPath : MorphismExpr cat a b -> MorphismPath cat a b
+exprToPath (IdExpr a) = []
+exprToPath (CompExpr f g) = exprToPath f ++ exprToPath g
+exprToPath (OtherExpr f) = [f]
+
+unquotePathApp : (p : MorphismPath cat a b) -> (q : MorphismPath cat b c)
+              -> unquotePath (p ++ q) = compose _ _ _ _ (unquotePath p) (unquotePath q)
+unquotePathApp [] q = sym $ leftIdentity _ _ _ (unquotePath q)
+unquotePathApp (f :: fs) q = rewrite unquotePathApp fs q in associativity _ _ _ _ _ _ _ _
+
+unquoteTriangle : (f : MorphismExpr cat a b) -> unquotePath (exprToPath f) = unquoteExpr f
+unquoteTriangle (IdExpr a) = Refl
+unquoteTriangle (CompExpr f g) =
+  rewrite unquotePathApp (exprToPath f) (exprToPath g) in
+  rewrite unquoteTriangle f in
+  rewrite unquoteTriangle g in Refl
+unquoteTriangle (OtherExpr f) = rightIdentity _ _ _ _
+
+proveEq : (f : MorphismExpr cat a b) -> (g : MorphismExpr cat a b)
+       -> unquotePath (exprToPath f) = unquotePath (exprToPath g) -> unquoteExpr f = unquoteExpr g
+proveEq f g hyp =
+  rewrite sym $ unquoteTriangle f in
+  rewrite sym $ unquoteTriangle g in hyp
+
+reifyExpr : Raw -> Elab ()
+reifyExpr `(identity ~cat ~a) = exact `(IdExpr {cat=~cat} ~a)
+reifyExpr `(compose ~cat ~a ~b ~c ~f ~g) = do
+  [l, r] <- refine `(CompExpr {cat=~cat} {a=~a} {b=~b} {c=~c})
+  inHole l (reifyExpr f)
+  inHole r (reifyExpr g) *> skip
+reifyExpr tm = (refine (Var `{OtherExpr}) `andThen` exact tm) *> skip
+
+morphism : Elab ()
+morphism =
+  case !(compute *> getGoal) of
+    (_, `((=) {A=mor ~catl ~al ~bl} {B=mor ~catr ~ar ~br} ~e1 ~e2)) => do
+
+      l <- gensym "L"
+      r <- gensym "R"
+
+      [catl', al', bl', catr', ar', br'] <- traverse forget [catl, al, bl, catr, ar, br]
+
+      remember l `(MorphismExpr ~catl' ~al' ~bl'); reifyExpr !(forget e1)
+      remember r `(MorphismExpr ~catr' ~ar' ~br'); reifyExpr !(forget e2)
+
+      equiv `((=) {A=_} {B=_}
+        (unquoteExpr {cat=~catl'} {a=~al'} {b=~bl'} ~(Var l))
+        (unquoteExpr {cat=~catr'} {a=~ar'} {b=~br'} ~(Var r)))
+
+      andThen (refine `(proveEq {cat=~catl'} {a=~al'} {b=~bl'} ~(Var l) ~(Var r))) reflexivity
+      skip
+
+
+test : (f : mor cat a b) -> (g : mor cat b c) -> (h : mor cat c d)
+    -> compose _ _ _ _ f (compose _ _ _ _ g h) = compose _ _ _ _ (compose _ _ _ _ f g) h
+test f g h = %runElab morphism

src/Tactics/MorphismTest.idr

@@ -0,0 +1,45 @@
+module Tactics.MorphismTest
+
+import Basic.Category
+import Basic.Functor
+import Basic.NaturalTransformation
+import Syntax.PreorderReasoning
+import Tactics
+
+%language ElabReflection
+
+naturalTransformationCompositionTest :
+     (cat1, cat2 : Category)
+  -> (fun1, fun2, fun3 : CFunctor cat1 cat2)
+  -> NaturalTransformation cat1 cat2 fun1 fun2
+  -> NaturalTransformation cat1 cat2 fun2 fun3
+  -> NaturalTransformation cat1 cat2 fun1 fun3
+naturalTransformationCompositionTest cat1 cat2 fun1 fun2 fun3
+  (MkNaturalTransformation comp1 comm1)
+  (MkNaturalTransformation comp2 comm2) =
+    MkNaturalTransformation
+      (\a => compose cat2 (mapObj fun1 a) (mapObj fun2 a) (mapObj fun3 a) (comp1 a) (comp2 a))
+      (\a, b, f =>
+        (compose cat2 _ _ _ (compose cat2 _ _ _ (comp1 a) (comp2 a)) (mapMor fun3 a b f))
+        -- I did tests at the following equality. If you run :elab h <RET>
+        -- intros <RET> morphism <RET> :qed, the goal gets solved. However, if
+        -- you paste the corresponding code into the hole, it just runs forever.
+        -- `%runElab morphism` in place of the hole should also work, but has
+        -- the same issue. Similar behaviour can be seen elsewhere, where it
+        -- runs fine interactively, but when used in a file it requires extra
+        -- annotations or sometimes doesn't work at all.
+          ={ %runElab morphism }=
+        -- The following line works, but that's of course not really what we want
+          -- ={ the ((compose _ _ _ _ (compose _ _ _ _ (comp1 a) (comp2 a)) (mapMor fun3 a b f)) = 
+          --         (compose _ _ _ _ (comp1 a) (compose _ _ _ _ (comp2 a) (mapMor fun3 a b f)))) 
+          --        (%runElab morphism) }=
+        (compose _ _ _ _ (comp1 a) (compose _ (mapObj fun2 a) (mapObj fun3 a) (mapObj fun3 b) (comp2 a) (mapMor fun3 a b f)))
+          ={ cong $ comm2 a b f }=
+        (compose cat2 _ _ _ (comp1 a) (compose cat2 _ _ _ (mapMor fun2 _ _ f) (comp2 b)))
+          ={ associativity cat2 _ _ _ _ (comp1 a) (mapMor fun2 a b f) (comp2 b) }=
+        (compose cat2 _ _ _ (compose cat2 _ _ _ (comp1 a) (mapMor fun2 _ _ f)) (comp2 b))
+          ={ cong {f = \h => compose cat2 _ _ _ h (comp2 b)} $ comm1 a b f }=
+        (compose cat2 _ _ _ (compose cat2 _ _ _ (mapMor fun1 a b f) (comp1 b)) (comp2 b))
+          ={ sym $ associativity cat2 _ _ _ _ (mapMor fun1 _ _ f) (comp1 b) (comp2 b) }=
+        (compose cat2 _ _ _ (mapMor fun1 _ _ f) (compose cat2 _ _ _ (comp1 b) (comp2 b)))
+      QED)