Skip to content

Instantly share code, notes, and snippets.

@david-christiansen

david-christiansen/Monoid.idr

Last active January 25, 2018 02:27
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save david-christiansen/066ad771212b2f20ea40 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save david-christiansen/066ad771212b2f20ea40 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. david-christiansen revised this gist Sep 19, 2015. 1 changed file with 32 additions and 8 deletions.
    40 changes: 32 additions & 8 deletions Monoid.idr
    View file
    Original file line number Diff line number Diff line change
    @@ -38,7 +38,6 @@ namespace Tactics

    ||| A representation of monoids with proofs
    class IsMonoid a where
    constructor MkMonoidOps
    neut : a
    op : a -> a -> a
    neutLeftId : (x : a) -> neut `op` x = x
    @@ -53,12 +52,18 @@ instance IsMonoid () where
    assoc () () () = Refl

    instance IsMonoid Nat where
    neut = Z
    op = plus
    neutLeftId _ = Refl
    neutRightId = plusZeroRightNeutral
    assoc = plusAssociative

    neut = Z
    op = plus
    neutLeftId _ = Refl
    neutRightId = plusZeroRightNeutral
    assoc = plusAssociative

    instance [multMonoid] IsMonoid Nat where
    neut = 1
    op = mult
    neutLeftId = multOneLeftNeutral
    neutRightId = multOneRightNeutral
    assoc = multAssociative

    ||| An abstract characterization of a monoidal expression as a syntax tree
    data MonoidExpr a =
    @@ -165,6 +170,21 @@ natPlusAsMonoid =
    newTy cls tm = tm


    ||| Convert Nat multiplication expressions to monoid expressions,
    ||| returning the type class dictionary used to get the right
    ||| equalities.
    natMultAsMonoid : Elab Raw
    natMultAsMonoid =
    do equiv (newTy !goalType)
    return `(multMonoid)

    where newTy : Raw -> Raw
    newTy `(mult ~j ~k) = `(op @{multMonoid} ~(newTy j) ~(newTy k))
    newTy `(S Z) = `(neut @{multMonoid})
    newTy (RApp f x) = RApp (newTy f) (newTy x)
    newTy (RBind n b tm) = RBind n (newTy <$> b) (newTy tm)
    newTy tm = tm

    test1 : (IsMonoid a) =>
    (w,x,y,z : a) ->
    (( w `op` x) `op` (y `op` z)) = (w `op` (x `op` (y `op` (z `op` neut))))
    @@ -177,5 +197,9 @@ test2 x y z = %runElab (do dict <- natPlusAsMonoid
    asMonoid dict
    search)


    test3 : (x,y,z : Nat) ->
    (x * ((y * 1) * x)) * 1 = x * y * x
    test3 x y z = %runElab (do dict <- natMultAsMonoid
    asMonoid dict
    search)

  2. david-christiansen revised this gist Sep 19, 2015. 1 changed file with 23 additions and 23 deletions.
    46 changes: 23 additions & 23 deletions Monoid.idr
    View file
    Original file line number Diff line number Diff line change
    @@ -39,64 +39,64 @@ namespace Tactics
    ||| A representation of monoids with proofs
    class IsMonoid a where
    constructor MkMonoidOps
    zero : a
    neut : a
    op : a -> a -> a
    zeroLeftId : (x : a) -> zero `op` x = x
    zeroRightId : (x : a) -> x `op` zero = x
    neutLeftId : (x : a) -> neut `op` x = x
    neutRightId : (x : a) -> x `op` neut = x
    assoc : (x, y, z : a) -> op x (op y z) = op (op x y) z

    instance IsMonoid () where
    zero = ()
    neut = ()
    op () () = ()
    zeroLeftId () = Refl
    zeroRightId () = Refl
    neutLeftId () = Refl
    neutRightId () = Refl
    assoc () () () = Refl

    instance IsMonoid Nat where
    zero = Z
    neut = Z
    op = plus
    zeroLeftId _ = Refl
    zeroRightId = plusZeroRightNeutral
    neutLeftId _ = Refl
    neutRightId = plusZeroRightNeutral
    assoc = plusAssociative


    ||| An abstract characterization of a monoidal expression as a syntax tree
    data MonoidExpr a =
    ZERO | VAR a | OP (MonoidExpr a) (MonoidExpr a)
    NEUT | VAR a | OP (MonoidExpr a) (MonoidExpr a)

    ||| Recover a monoid value from a reflected tree
    interpExpr : (IsMonoid a) => MonoidExpr a -> a
    interpExpr ZERO = zero
    interpExpr NEUT = neut
    interpExpr (VAR x) = x
    interpExpr (OP x y) = op (interpExpr x) (interpExpr y)

    ||| We can also interpret lists using the monoid operations
    interpList : (IsMonoid a) => List a -> a
    interpList [] = zero
    interpList [] = neut
    interpList (x :: xs) = op x $ interpList xs

    ||| Normalize a monoid expression into a list
    flattenExpr : MonoidExpr a -> List a
    flattenExpr ZERO = []
    flattenExpr NEUT = []
    flattenExpr (VAR x) = [x]
    flattenExpr (OP x y) = flattenExpr x ++ flattenExpr y

    ||| List appending is justified using monoid associativity
    opAppend : (IsMonoid a) => (xs, ys : List a) ->
    op (interpList xs) (interpList ys) = interpList (xs ++ ys)
    opAppend [] ys = zeroLeftId _
    opAppend [] ys = neutLeftId _
    opAppend (x :: xs) ys =
    rewrite sym $ opAppend xs ys in
    sym $ assoc x (interpList xs) (interpList ys)

    ||| Flattening and interpretation commute
    flattenOk : (IsMonoid a) => (e : MonoidExpr a) -> interpExpr e = interpList (flattenExpr e)
    flattenOk ZERO = Refl
    flattenOk (VAR x) = sym $ zeroRightId x
    flattenOk (OP x y) with (flattenOk x)
    flattenOk (OP x y) | flatX with (flattenOk y)
    flattenOk (OP x y) | flatX | flatY =
    rewrite flatX in rewrite flatY in opAppend (flattenExpr x) (flattenExpr y)
    flattenOk NEUT = Refl
    flattenOk (VAR x) = sym $ neutRightId x
    flattenOk (OP x y) =
    rewrite flattenOk x in
    rewrite flattenOk y in
    opAppend (flattenExpr x) (flattenExpr y)


    ||| Flattening preserves interpretation according to the monoid laws
    @@ -115,7 +115,7 @@ reifyExpr `(op {a=~a} @{~dict} ~x ~y) =
    solve
    focus l; reifyExpr x
    focus r; reifyExpr y
    reifyExpr `(zero {a=~a} @{~dict}) = do fill `(ZERO {a=~a}); solve
    reifyExpr `(neut {a=~a} @{~dict}) = do fill `(NEUT {a=~a}); solve
    reifyExpr tm = do [_, (_, h)] <- apply (Var `{VAR}) [(True, 0), (False, 1)]
    solve
    focus h; fill tm
    @@ -155,7 +155,7 @@ natPlusAsMonoid =

    where newTy : Raw -> Raw -> Raw
    newTy cls `(plus ~j ~k) = `(op {a=Nat} @{~cls} ~(newTy cls j) ~(newTy cls k))
    newTy cls `(Z) = `(zero {a=Nat} @{~cls})
    newTy cls `(Z) = `(neut {a=Nat} @{~cls})
    -- this next case is necessary to undo computation of plus's
    -- first arg and get it into a form that the monoid equality
    -- solver can figure out
    @@ -167,7 +167,7 @@ natPlusAsMonoid =

    test1 : (IsMonoid a) =>
    (w,x,y,z : a) ->
    (( w `op` x) `op` (y `op` z)) = (w `op` (x `op` (y `op` (z `op` zero))))
    (( w `op` x) `op` (y `op` z)) = (w `op` (x `op` (y `op` (z `op` neut))))
    test1 @{dict} w x y z = %runElab (asMonoid (Var `{dict}) *> search)


  3. david-christiansen created this gist Sep 19, 2015.
    181 changes: 181 additions & 0 deletions Monoid.idr
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,181 @@
    import Language.Reflection.Elab

    namespace Tactics

    ||| Restrict a polymorphic type to () for contexts where it doesn't
    ||| matter. This is nice for sticking `debug` in a context where
    ||| Idris can't solve the type.
    simple : {m : Type -> Type} -> m () -> m ()
    simple x = x

    ||| Replace the current goal with one that's definitionally
    ||| equal. Return the name of the new goal, and ensure that it's
    ||| focused.
    |||
    ||| @ newGoal A type that is equivalent to the current goal
    equiv : (newGoal : Raw) -> Elab TTName
    equiv newGoal = do h <- gensym "goal"
    claim h newGoal
    fill (Var h); solve
    focus h
    return h

    ||| Remember a term built with elaboration for later use. If the
    ||| current goal is `h`, then `remember n ty` puts a fresh hole at
    ||| the front of the queue, with the old goal `h` second. The
    ||| contents of this hole end up let-bound in the scope of
    ||| `h`. Return the name of the new hole, in case it will be used
    ||| later.
    |||
    ||| @ n the name to be used to save the term
    ||| @ ty the type to inhabit
    remember : (n : TTName) -> (ty : Raw) -> Elab TTName
    remember n ty = do todo <- gensym "rememberThis"
    claim todo ty
    letbind n ty (Var todo)
    focus todo
    return todo

    ||| A representation of monoids with proofs
    class IsMonoid a where
    constructor MkMonoidOps
    zero : a
    op : a -> a -> a
    zeroLeftId : (x : a) -> zero `op` x = x
    zeroRightId : (x : a) -> x `op` zero = x
    assoc : (x, y, z : a) -> op x (op y z) = op (op x y) z

    instance IsMonoid () where
    zero = ()
    op () () = ()
    zeroLeftId () = Refl
    zeroRightId () = Refl
    assoc () () () = Refl

    instance IsMonoid Nat where
    zero = Z
    op = plus
    zeroLeftId _ = Refl
    zeroRightId = plusZeroRightNeutral
    assoc = plusAssociative


    ||| An abstract characterization of a monoidal expression as a syntax tree
    data MonoidExpr a =
    ZERO | VAR a | OP (MonoidExpr a) (MonoidExpr a)

    ||| Recover a monoid value from a reflected tree
    interpExpr : (IsMonoid a) => MonoidExpr a -> a
    interpExpr ZERO = zero
    interpExpr (VAR x) = x
    interpExpr (OP x y) = op (interpExpr x) (interpExpr y)

    ||| We can also interpret lists using the monoid operations
    interpList : (IsMonoid a) => List a -> a
    interpList [] = zero
    interpList (x :: xs) = op x $ interpList xs

    ||| Normalize a monoid expression into a list
    flattenExpr : MonoidExpr a -> List a
    flattenExpr ZERO = []
    flattenExpr (VAR x) = [x]
    flattenExpr (OP x y) = flattenExpr x ++ flattenExpr y

    ||| List appending is justified using monoid associativity
    opAppend : (IsMonoid a) => (xs, ys : List a) ->
    op (interpList xs) (interpList ys) = interpList (xs ++ ys)
    opAppend [] ys = zeroLeftId _
    opAppend (x :: xs) ys =
    rewrite sym $ opAppend xs ys in
    sym $ assoc x (interpList xs) (interpList ys)

    ||| Flattening and interpretation commute
    flattenOk : (IsMonoid a) => (e : MonoidExpr a) -> interpExpr e = interpList (flattenExpr e)
    flattenOk ZERO = Refl
    flattenOk (VAR x) = sym $ zeroRightId x
    flattenOk (OP x y) with (flattenOk x)
    flattenOk (OP x y) | flatX with (flattenOk y)
    flattenOk (OP x y) | flatX | flatY =
    rewrite flatX in rewrite flatY in opAppend (flattenExpr x) (flattenExpr y)


    ||| Flattening preserves interpretation according to the monoid laws
    monoidReflection : (IsMonoid a) => (x, y : MonoidExpr a) ->
    interpList (flattenExpr x) = interpList (flattenExpr y) ->
    interpExpr x = interpExpr y
    monoidReflection x y prf = rewrite flattenOk x in
    rewrite flattenOk y in
    prf

    ||| This tactic takes a reflected Idris expression and fills the
    ||| current hole with that expression's representation as a `MonoidExpr`
    reifyExpr : Raw -> Elab ()
    reifyExpr `(op {a=~a} @{~dict} ~x ~y) =
    do [(_, l), (_, r)] <- apply `(OP {a=~a}) [(False, 1), (False, 1)]
    solve
    focus l; reifyExpr x
    focus r; reifyExpr y
    reifyExpr `(zero {a=~a} @{~dict}) = do fill `(ZERO {a=~a}); solve
    reifyExpr tm = do [_, (_, h)] <- apply (Var `{VAR}) [(True, 0), (False, 1)]
    solve
    focus h; fill tm
    solve
    reifyExpr _ = empty -- for fast totality checking

    ||| Given a reflected IsMonoid type class instance dictionary, use it
    ||| to normalize a goal that is an equality of monoid expressions.
    asMonoid : (dict : Raw) -> Elab ()
    asMonoid dict =
    case !goalType of
    `((=) {A=~A} {B=~B} ~e1 ~e2) =>
    do l <- gensym "L"
    r <- gensym "R"

    remember l `(MonoidExpr ~A); reifyExpr e1
    remember r `(MonoidExpr ~B); reifyExpr e2

    equiv `((=) {A=~A} {B=~B}
    (interpExpr {a=~A} @{~dict} ~(Var l))
    (interpExpr {a=~B} @{~dict} ~(Var r)))

    [(_, h)] <-
    apply `(monoidReflection {a=~A} @{~dict} ~(Var l) ~(Var r)) [(True, 0)]

    solve
    focus h

    ||| Convert Nat addition expressions to monoid expressions, returning the
    ||| type class dictionary in order to get the right equalities.
    natPlusAsMonoid : Elab Raw
    natPlusAsMonoid =
    do cls <- gensym "cls"
    remember cls `(IsMonoid Nat); resolveTC `{natPlusAsMonoid}
    equiv (newTy (Var cls) !goalType)
    return (Var cls)

    where newTy : Raw -> Raw -> Raw
    newTy cls `(plus ~j ~k) = `(op {a=Nat} @{~cls} ~(newTy cls j) ~(newTy cls k))
    newTy cls `(Z) = `(zero {a=Nat} @{~cls})
    -- this next case is necessary to undo computation of plus's
    -- first arg and get it into a form that the monoid equality
    -- solver can figure out
    newTy cls `(S ~k) = `(op {a=Nat} @{~cls} 1 ~(newTy cls k))
    newTy cls (RApp f x) = RApp (newTy cls f) (newTy cls x)
    newTy cls (RBind n b tm) = RBind n (newTy cls <$> b) (newTy cls tm)
    newTy cls tm = tm


    test1 : (IsMonoid a) =>
    (w,x,y,z : a) ->
    (( w `op` x) `op` (y `op` z)) = (w `op` (x `op` (y `op` (z `op` zero))))
    test1 @{dict} w x y z = %runElab (asMonoid (Var `{dict}) *> search)


    test2 : (x, y, z : Nat) ->
    plus (plus (plus z 13) z) (plus x (plus y Z)) = z `plus` (13 `plus` ((z `plus` x) `plus` y))
    test2 x y z = %runElab (do dict <- natPlusAsMonoid
    asMonoid dict
    search)