Trying to make the time until my flight leaves tomorrow go by, I played around a bit with the proof assistant Coq. And after wrestling a LOT with the assistant, I ended up being able to prove some pretty basic group theory results.

And this is how it goes:

Section Groups.

Variable U : Set.
Variable m : U -> U -> U.
Variable i : U -> U.
Variable e : U.

Hypothesis ass : forall x y z : U, m x (m y z) = m (m x y) z.
Hypothesis runit : forall x : U, m x e = x.
Hypothesis rinv : forall x : U, m x (i x) = e.

This sets the stage. It defines a group as a group object in Set, but without the diagonal map. It produces a minimal definition - the left identity and inverse follow from the right ones, which we shall prove immediately.

First off, the right unit is the only idempotent in the group.

Lemma unit_uniq : forall x : U, m x x = x -> x = e.
intros.
rewrite <- runit with x.
rewrite <- (rinv x).
rewrite ass.
rewrite H.
reflexivity.
Qed.

Now, intros. is a way to automatically name all hypotheses in the statement. reflexivity tells us that if we could derive A=A, then we're done. And rewrite applies a known result everywhere that it could possibly could be applied. The arrows tell us which direction the equalities should be employed.

Now, our right inverse is a left inverse:

Lemma linv : forall x : U, m (i x) x = e.
intros.
apply unit_uniq.
rewrite <- ass with (i x) x (m (i x) x).
rewrite ass with x (i x) x.
rewrite rinv.
rewrite ass.
rewrite runit.
reflexivity.

and our right unit is a left unit:

Lemma lunit : forall x : U, m e x = x.
intros.
rewrite <- (rinv x).
rewrite <- ass.
rewrite linv.
rewrite runit.
reflexivity.
Qed.

In a group, we have cancellation laws. We can remove left and right multiplied factors:

Lemma lcancel: forall x y z : U, y = z -> m x y = m x z.
intros.
replace y with z.
reflexivity.
Qed.

Lemma rcancel: forall x y z : U, x = y -> m x z = m y z.
intros.
replace x with y.
reflexivity.
Qed.

and we can add them again

Lemma lcocancel: forall x y z : U, m x y = m x z -> y = z.
intros.
rewrite <- lunit.
rewrite <- (lunit y).
rewrite <- (linv x).
rewrite <- ass.
rewrite <- ass.
rewrite H.
reflexivity.
Qed.

Lemma rcocancel: forall x y z : U, m x z = m y z -> x = y.
intros.
rewrite <- runit.
rewrite <- (runit x).
rewrite <- (rinv z).
rewrite ass.
rewrite ass.
rewrite H.
reflexivity.
Qed.

There's most probably something obscure going on with the proof model in Coq: I often get the feeling that I run backwards when I write the proofs. Thus, the result we need to be able to perform a cancellation when we're rewriting our proof goal is y = z -> m x y = m x z and not the other way around, which surprises me a bit.

The inverses are unique:

Lemma inv_uniq: forall x y : U, m x y = e -> y = i x.
intros.
apply (lcocancel x).
rewrite rinv.
apply H.
Qed.

and the well known product rule (xy):sup:-1=y^-1x^-1 holds:

Lemma prod_inv: forall x y : U, i (m x y) = m (i y) (i x).
intros.
apply (lcocancel (m x y)).
rewrite rinv.
rewrite <- ass.
rewrite ass with y (i y) (i x).
rewrite rinv.
rewrite lunit.
symmetry  in |- *; apply rinv.
Qed.

Finally, a slightly larger theorem is the statement that if all elements of a group have order 2, then the group is commutative. This is, in Coq, the following argument:

Theorem ord2_comm: (forall x : U, m x x = e) -> (forall y z : U, m y z = m z y).
intros.
rewrite <- (runit z).
symmetry  in |- *.
rewrite <- lunit.
replace (m e (m y (m z e))) with (m (m z z) (m y (m z (m y y)))).
 rewrite ass.
   rewrite ass.
   rewrite ass.
   apply rcancel.
   rewrite <- ass.
   rewrite <- ass with z z y.
   rewrite <- ass with z (m z y) (m z y).
   rewrite H.
   reflexivity.
 rewrite H.
   rewrite H.
   reflexivity.
Qed.

It doesn't really end up being more legible than if I had written it out myself, but it is machine checkable, and not THAT far from being legible as well. If you step through, you certainly do realize the mapping between Coq and pen-n-paper pretty immediately.

Sometime in the future, I'll sit down and do some category theory and topology in Coq. I think the 5-lemma and other diagram chases will end up being amusing.