Rewriting in simple theorem proof

Question

I wrote a definition of group in Idris:

data Group: Type -> Type where
    Unit: (x: t) -> Group t
    (*): Group t -> Group t -> Group t
    Inv: Group t -> Group t
postulate
    assoc: (a : Group t) -> (b : Group t) -> (c : Group t) -> ((a*b)*c = a*(b*c))
postulate
    neutralL: (x: t) -> (a : Group t) -> a * Unit x = a
postulate
    neutralR: (x: t) -> (a : Group t) -> Unit x * a = a
postulate
    invUnitL: (x: t) -> (a : Group t) -> a * (Inv a) = Unit x
postulate
    invUnitR: (x: t) -> (a : Group t) -> (Inv a) * a = Unit x

Then I proved a couple of simple propositions:

cong : (a : Group t) -> (b : Group t) -> (c: Group t) -> a = b -> a*c = b*c
cong a b c post = rewrite post in Refl

neutralL1: (x: t) -> (a : Group t) -> a = a * Unit x
neutralL1 x a = rewrite neutralL x a in Refl

neutralR1: (x: t) -> (a : Group t) -> a = Unit x * a
neutralR1 x a = rewrite neutralR x a in Refl

However, I have a problem with proving that there is only one unit element:

singleUnit : (x: t) -> (y: t) -> (Unit x = Unit y)

I tried various expressions using a general idea, that Unit x = (by neutralL1 y (Unit x)) = Unit x * Unit y = (by neutralR x (Unit y)) = Unit y, but with no success:

singleUnit x y = rewrite neutralL1 y (Unit x) in neutralR x (Unit y)
singleUnit x y = rewrite neutralL1 y (Unit x) in rewrite neutralR x (Unit y) in Refl
singleUnit x y = rewrite neutralR x (Unit y) in neutralL1 y (Unit x)
singleUnit x y = rewrite neutralR x (Unit y) in rewrite neutralL1 y (Unit x) in Refl

How can I prove this? I have a feeling, that the problem here is related to substitution of complex expressions, like Unit x * Unit y.

Answer 1

Unfortunately, this definition of a group won't work. In general, you have to be very careful introducing new axioms (postulates).

E.g. it's easy to see that neutralL violates the principle of disjointness of (different) data constructors, i.e. Constr1 <data> != Constr2 <data>.

starAndUnitAreDisjoint : (*) a (Unit x) = a -> Void
starAndUnitAreDisjoint Refl impossible

Now we can prove false:

contradiction : Void
contradiction = starAndUnitAreDisjoint $ neutralL Z (Unit Z)

Finita la commedia!

What you actually want is a record or a typeclass, see e.g. contrib/Control/Algebra.idr and contrib/Interfaces/Verified.idr. In addition, Agda versions are syntactically pretty close to Idris (agda-stdlib/src/Algebra.agda and probably the Abstract Algebra in Agda tutorial) -- you might want to have a look at them.