# Elementary algebra in Coq: Trivial group

## 2016-03-01

Recall our definition of groups in Coq from the last time:

``````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 is a record. You can construct a value of type `group` by providing a value for all the fields. By default, the constructor is called `Build_group`:

``````Build_group
: forall (G : Set) (id : G) (op : G -> G -> G) (inv : G -> G),
(forall x y z : G, op x (op y z) = op (op x y) z) ->
(forall x : G, op (inv x) x = id) ->
(forall x : G, op id x = x) -> group``````

This is also the reason why we didn’t include the right-hand side versions of `op_inv_l` and `op_id_l` into the definition of `group`. If we did, you’d have to provide proofs of the right-hand side laws when constructing a `group` value.

We can construct the trivial group over `unit`:

``````Example trivial_group : group.
refine (Build_group unit tt (fun _ _ => tt) (fun _ => tt) _ _ _).
- intros. auto.
- intros. auto.
- intros. destruct x. trivial.
Defined.``````

More interestingly, we can define the additive group of integers `Z`. Since Coq’s standard library contains a good set of properties for `Z`, defining the group is straightforward.

``````Require Import Coq.ZArith.BinInt.
Open Scope Z.