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.