From 8b37faa18434c12817cde53681307fb4a444ac63 Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Wed, 31 Jul 2019 17:05:24 +0200 Subject: [PATCH 1/2] Add morphism tactic --- idris-ct.nix | 1 + src/Tactics.idr | 2 + src/Tactics/Morphism.idr | 92 ++++++++++++++++++++++++++++++++++++ src/Tactics/MorphismTest.idr | 41 ++++++++++++++++ 4 files changed, 136 insertions(+) create mode 100644 src/Tactics.idr create mode 100644 src/Tactics/Morphism.idr create mode 100644 src/Tactics/MorphismTest.idr diff --git a/idris-ct.nix b/idris-ct.nix index 6c5d1b8..7cd1d84 100644 --- a/idris-ct.nix +++ b/idris-ct.nix @@ -27,6 +27,7 @@ idrisPackages.build-idris-package { idrisDeps = with idrisPackages; [ contrib + pruviloj ]; meta = { diff --git a/src/Tactics.idr b/src/Tactics.idr new file mode 100644 index 0000000..ab4ac56 --- /dev/null +++ b/src/Tactics.idr @@ -0,0 +1,2 @@ +import public Pruviloj.Core +import public Tactics.Morphism diff --git a/src/Tactics/Morphism.idr b/src/Tactics/Morphism.idr new file mode 100644 index 0000000..46464f2 --- /dev/null +++ b/src/Tactics/Morphism.idr @@ -0,0 +1,92 @@ +-- 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) + +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 diff --git a/src/Tactics/MorphismTest.idr b/src/Tactics/MorphismTest.idr new file mode 100644 index 0000000..7ab0618 --- /dev/null +++ b/src/Tactics/MorphismTest.idr @@ -0,0 +1,41 @@ +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 + -- intros morphism :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. + ={ ?h }= + -- 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 _ (mapObj fun2 a) (mapObj fun3 a) (mapObj fun3 b) (comp2 a) (mapMor fun3 a b f)))) (%runElab morphism) }= + (compose _ _ _ _ (comp1 a) (compose _ _ _ _ (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) From d4639830c03a2aeef2395ea7f32424079feb730d Mon Sep 17 00:00:00 2001 From: FabrizioRomanoGenovese Date: Thu, 1 Aug 2019 17:26:25 +0200 Subject: [PATCH 2/2] Liveshare stuff added. --- src/Tactics/Morphism.idr | 8 +++++++- src/Tactics/MorphismTest.idr | 12 ++++++++---- 2 files changed, 15 insertions(+), 5 deletions(-) diff --git a/src/Tactics/Morphism.idr b/src/Tactics/Morphism.idr index 46464f2..dcb6df3 100644 --- a/src/Tactics/Morphism.idr +++ b/src/Tactics/Morphism.idr @@ -1,3 +1,5 @@ +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 @@ -33,6 +35,11 @@ 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 @@ -57,7 +64,6 @@ 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 diff --git a/src/Tactics/MorphismTest.idr b/src/Tactics/MorphismTest.idr index 7ab0618..3b31a00 100644 --- a/src/Tactics/MorphismTest.idr +++ b/src/Tactics/MorphismTest.idr @@ -1,3 +1,5 @@ +module Tactics.MorphismTest + import Basic.Category import Basic.Functor import Basic.NaturalTransformation @@ -26,10 +28,12 @@ naturalTransformationCompositionTest cat1 cat2 fun1 fun2 fun3 -- 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. - ={ ?h }= + ={ %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 _ (mapObj fun2 a) (mapObj fun3 a) (mapObj fun3 b) (comp2 a) (mapMor fun3 a b f)))) (%runElab morphism) }= - (compose _ _ _ _ (comp1 a) (compose _ _ _ _ (comp2 a) (mapMor fun3 a b f))) + -- ={ 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) }= @@ -38,4 +42,4 @@ naturalTransformationCompositionTest cat1 cat2 fun1 fun2 fun3 (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) + QED) \ No newline at end of file