Michi’s blog

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:

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.

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:

and our right unit is a left unit:

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

and we can add them again

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:

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

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:

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.

• previous post
• next post

• FRA-Lagen och falska positiver  9
  Fredrik Reinfilth, Dag, Michi, Dag, Gustaf, Michi [...]
• A vision for collaborative mathematics platforms  7
  Dan Drake, Nathaniel Dean, Michi, Ben Webster, Nathan Dunfield, Joachim Breitner [...]
• AMS and mathjobs.org are made of awesome  2
  Michi, Ben Webster
• Restarting high school topology  1
  John Armstrong
• Tour dates  5
  sigfpe, Charles, John Palmieri, Michi, Charles
• Introduction to Algebraic Geometry (2 in a series)  1
  lhrrwcc

• Blogroll

  • Andart
  • Michi’s moat

• Family

  • Fragmented Visions

• Mathematician blogs

  • - d -
  • 3d pancakes
  • A mathematician’s scratchpad
  • A neighbourhood of infinity
  • Antimeta
  • Blog of a math teacher
  • eon
  • Epsilon Delta
  • Few but ripe
  • Good Math, Bad Math
  • Gooseania
  • Halfway There
  • Learning Curves
  • Maths weblog
  • Numerical Notes
  • Tall Dark and Mysterious
  • The real sqrt
  • Think Again