Proving Groups with Idris

Exactly a year ago, in one of my previous posts, we proved Monoid laws with Idris. We’ll do the same with Groups.

A Group is an algebraic structure defined on a set G with an operation * denoted , which satisfies these laws:

1. – closure
2. – associativity
3. – identity
4. – inverse

Note that a Group is just a Monoid with an inverse. To abstract them in Idris, we will use a type constraint on our previously defined ProvenMonoid:

interface (ProvenMonoid m) => ProvenGroup m where
    minverse : m -> m
    inverseProofL : (a : m) -> mappend a (minverse a) = Main.mempty
    inverseProofR : (a : m) -> mappend (minverse a) a = Main.mempty

We will mathematically prove that is a Group:

1. Adding any two integers produces an integer
2. We use induction on c. Base case is trivial, so we proceed to use the inductive hypothesis as follows:
3. since
4.

We will do the same proof in Idris. First, we’ll prove that the operation forms a Monoid. We’ll use Data.ZZ for that since we want to use integers, not naturals. For this, you will have to run the REPL as idris test.idr -p contrib:

implementation ProvenMonoid ZZ where
    mappend x y = x + y
    mempty      = Pos Z

    assocProof  = plusAssociativeZ
    idProofL    = plusZeroLeftNeutralZ
    idProofR    = plusZeroRightNeutralZ

Pretty similar to naturals. What about Group?

implementation ProvenGroup ZZ where
    minverse      = negate

    inverseProofL = plusNegateInverseLZ
    inverseProofR = plusNegateInverseRZ

Cool stuff, right? 🙂