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.^{1}

```
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.

You could also set up some hints for

↩`auto`

and`autorewrite`

to make the theorems easier to prove. My CoqIDE just crashed and ate my hints, so they will have to wait for the next time.