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:

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.

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:

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:

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:

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

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:

intros.

apply (lcocancel x).

rewrite rinv.

apply H.

Qed.

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

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:

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.

You don’t explicitly specify a diagonal map, but it’s implicit somewhere — maybe in Coq itself. You can’t state the inverse conditions without “duplicating” the variable so you can invert one copy.