Elementary algebra in Coq: Defining a group

When I was first learning about theorem provers, one of the first things I wanted to do was to formalize some of the things I had learned about abstract algebra. Abstract algebra should be easy to formalize, since it’s so axiomatic.

How would you formalize groups, then? One of the ways is to use structures (records):

Structure group :=
  {
    G :> Set;

    id : G;
    op : G -> G -> G;
    inv : G -> G;

    op_assoc : forall (x y z : G), op x (op y z) = op (op x y) z;
    op_inv_l : forall (x : G), id = op (inv x) x;
    op_id_l : forall (x : G), x = op id x
  }.

This record contains the underlying set G, the group operations and also witnesses of the group axioms. Now you can state theorems for all groups with forall (X : group) and you have access to the axioms. :> means a coercion from the group to the underlying set, so if you have group X, you can write g : X instead of g : G X.

You can make some of the arguments implicit and define a notation to make the theorems easier to state.¹

Arguments id {g}.
Arguments op {g} _ _.
Arguments inv {g} _.

Notation "x <.> y" := (op x y) (at level 50, left associativity).

Now we can state and prove a simple theorem, namely that in all groups, $f \circ f = f$ implies $f$ is the identity element.

Theorem square_is_unique (G : group) :
  forall (f : G), f <.> f = f -> f = id.
Proof.
  intros f H1.
  rewrite <- (op_id_l G f), <- (op_inv_l G f), <- op_assoc. 
  f_equal.
  assumption.
Qed.

Note that I defined group with only left-hand side version of op_inv_l and op_id_l. Deriving the right-hand versions is left as an exercise for the reader.

Update 2016-02-27: Simplified the proof for square_is_unique. The original version is here.