monoidy.idr

module monoidy

%default total 

class Monoidy a where 
  mempty : a
  mappend : a -> a -> a
  left_neutrality : (x : a) -> (mappend mempty x = x)
  right_neutrality : (x : a) -> (mappend x mempty = x)
  associativity : (x, y, z : a) -> (mappend x (mappend y z) = mappend (mappend x y) z)

appendAssociative2 : (l : List a) -> (c : List a) -> (r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r
appendAssociative2 [] c r = refl
appendAssociative2 (x :: xs) c r = cong $ appendAssociative2 xs c r

instance Monoidy (List a) where
  mempty = []
  mappend [] y = y
  mappend (x :: xs) y = x :: (mappend xs y)

  left_neutrality x = refl
  right_neutrality [] = refl
  right_neutrality (x :: xs) with (right_neutrality xs)
    | rn = cong {f = blowme} rn where
         blowme : (List a) -> (List a)
         blowme xs = x :: xs

--   |-- monoidy.idr line 24 col 17:
--   |   When elaborating right hand side of monoidy.List a instance of monoidy.Monoidy, method right_neutrality:
--   |   When elaborating an application of function Prelude.Basics.cong:
--   |           Can't unify
--   |                   mappend xs mempty = xs
--   |           with
--   |                   mappend xs [] = xs
--   |           
--   |           Specifically:
--   |                   Can't unify
--   |                           mappend xs mempty
--   |                   with
--   |                           mappend xs []

  associativity [] y z = refl
  associativity (x :: xs) y z with (associativity xs y z)
      | ass = cong {f = blowme} ass where
         blowme : (List a) -> (List a)
         blowme xs = x :: xs

--   monoidy.idr line 44 col 20:
--       When elaborating right hand side of monoidy.List a instance of monoidy.Monoidy, method associativity:
--       When elaborating an application of function Prelude.Basics.cong:
--               Can't unify
--                       mappend xs (mappend y z) = mappend (mappend xs y) z
--               with
--                       mappend xs (List a instance of monoidy.Monoidy, method mappend a y z) = mappend (mappend xs y) z
--               
--               Specifically:
--                       Can't unify
--                               mappend xs (mappend y z)
--                       with
--                               mappend xs (List a instance of monoidy.Monoidy, method mappend a y z)
--  


instance (Monoidy a) => Monoidy (Maybe a) where
  mempty = Nothing

  mappend Nothing y = y
  mappend (Just x) Nothing = Just x
  mappend (Just x) (Just y) = Just (mappend x y)

  left_neutrality = \x => refl
  right_neutrality Nothing = refl
  right_neutrality (Just x) = refl
  associativity Nothing y z = refl
  associativity (Just x) Nothing z = refl
  associativity (Just x) (Just y) Nothing = refl
  associativity (Just x) (Just y) (Just z) = let a_assoc = (associativity x y z) in rewrite a_assoc in refl

Just using (++) for mappend, seems to work on semigroup:

module Semi

class Semigroupy a where
  mappend : a -> a -> a
  associativity : (x, y, z : a) -> mappend x (mappend y z) = mappend (mappend x y) z

appendAssociative2 : (x, y, z : List a) -> x ++ (y ++ z) = (x ++ y) ++ z
appendAssociative2 [] y z = refl
appendAssociative2 (x :: xs) y z = cong $ appendAssociative2 xs y z

instance Semigroupy (List a) where
  mappend = (++)
  associativity = appendAssociative2

I'll try it w/ your recursive def of mappend.