Elementary algebra in Coq: Trivial group

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

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.