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 lefthand side version of op_inv_l
and
op_id_l
. Deriving the righthand versions is left as an exercise for the
reader.
Update 20160227: Simplified the proof for square_is_unique
. The original
version is here.

You could also set up some hints for
auto
andautorewrite
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. ↩︎