Group theory in Idris

Group.idr

import public Data.ZZ

record IsGroup (x : Type) ((*) : x -> x -> x) (e : x) where
  constructor PrfGrp
  associative : (a : x) -> (b : x) -> (c : x) -> a * (b * c) = (a * b) * c
  identity : (a : x) -> (a * e = a, e * a = a)
  inverse : (a : x) -> (a' : x ** (a * a' = e, a' * a = e))

intIsGroup : IsGroup ZZ (+) (Pos Z)
intIsGroup = let assocInt = plusAssociativeZ
                 identInt = \n => (plusZeroRightNeutralZ n, plusZeroLeftNeutralZ n)
                 invInt = \n => (negate n ** (plusNegateInverseLZ n, plusNegateInverseRZ n))
             in  PrfGrp assocInt identInt invInt

record IsAbelianGroup (x : Type)  ((*) : x -> x -> x) (e : x) where
  constructor PrfAbelianGrp
  prfIsGrp : IsGroup x (*) e
  commutative : (a : x) -> (b : x) -> a * b = b * a
  
intIsAbelianGroup : IsAbelianGroup ZZ (+) (Pos Z)
intIsAbelianGroup = let prfIsGroup = intIsGroup
                        commutative = plusCommutativeZ
                    in  PrfAbelianGrp prfIsGroup commutative