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.