Elementary algebra in Coq: Trivial group

In this series, I'm taking small steps towards understanding Coq.

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.

Example Z_add_group : group.
  refine (Build_group Z (0 : Z) Z.add Z.opp Z.add_assoc Z.add_opp_diag_l _).
  - trivial.
Defined.

Comments or questions? Tweet to me or send me an e-mail.