Michi’s blog » Blog Archive » Coq and simple group theory

Coq and simple group theory

August 5th, 2007

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)^-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.

3 People had this to say...

John Armstrong Said...

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.

August 5th, 2007 at 22:41

Michi Said...

Yeah, it is in the bit
Hypothesis rinv : forall x : U, m x (i x) = e.
which states the inverse condition, with the implicit diagonal Δ(x) = (x,x).

August 5th, 2007 at 22:47

Carnival of Math #18 « JD2718 Said...

[...] Blog Coq and simple group theory (see title) “Trying to make the time until my flight leaves tomorrow go by, I played around a [...]

October 6th, 2007 at 17:00

Want your say?

post navigation

about: Michi is a recent PhD working in homological algebra and applied algebraic topology. This blog is his outlet for texts with some manner of thought put into them. Over at his LiveJournal intimate details and streams of consciousness might be found.
Not all here is mathematics. All here, though, are my personal thoughts and opinions. Please read the about page (linked above) for more details.
This blog uses statcounter.com for logging and traffic analysis. In order to identify return visitors, this site will issue a cookie on viewing the blog.

Travel plans