I am trying to formalize groups in Coq. I want to be as general as possible. I'm trying to do something, but I'm not very happy with it. I have found various implementations, and I do not know which one to choose.
For example, I found this:
https://people.cs.umass.edu/~arjun/courses/cs691pl-spring2014/assignments/groups.html
(* The set of the group. *)
Parameter G : Set.
(* The binary operator. *)
Parameter f : G -> G -> G.
(* The group identity. *)
Parameter e : G.
(* The inverse operator. *)
Parameter i : G -> G.
(* For readability, we use infix <+> to stand for the binary operator. *)
Infix "<+>" := f (at level 50, left associativity).
(* The operator [f] is associative. *)
Axiom assoc : forall a b c, a <+> b <+> c = a <+> (b <+> c).
(* [e] is the right-identity for all elements [a] *)
Axiom id_r : forall a, a <+> e = a.
(* [i a] is the right-inverse of [a]. *)
Axiom inv_r : forall a, a <+> i a = e.
but why does the author use axioms rather than definitions? Moreover, I do not like some parameters at the top level.
In the CoqArt book, I found this implementation:
Record group : Type :=
{A : Type;
op : A→A→A;
sym : A→A;
e : A;
e_neutral_left : ∀ x:A, op e x = x;
sym_op : ∀ x:A, op (sym x) x = e;
op_assoc : ∀ x y z:A, op (op x y) z = op x (op y z)}.
In this definition, I believe that the definition should specialize, because if I want to define monodes, I will redefine op_assoc or neutral. Beyond this, for some theorems I do not need to use groups. For example, if I want to indicate that right_inverse matches left_inverse if the law is associative.
Another question is good axioms for groups:- use the neutral element as an axiom or left neutral element
- use inverse element as axiom or left inverse
What is more convenient to work with?
Finally, if I want to read some other theorems, I probably want to have syntactic sugar to use binary operation and inverse elements. What are your tips for having convenient notation for groups?
At the moment, I have done this:
Definition binary_operation {S:Set} := S -> S -> S.
Definition commutative {S:Set} (dot:binary_operation) := forall (a b:S), dot a b = dot b a.
Definition associative {S:Set} (dot:binary_operation) := forall (a b c:S), dot (dot a b) c = dot a (dot b c).
Definition left_identity {S:Set} (dot:binary_operation) (e:S) := forall a:S, (dot e a) = a.
Definition right_identity {S:Set} (dot:binary_operation) (e:S) := forall a:S, (dot a e) = a.
Definition identity {S:Set} (dot: binary_operation) (e:S) := left_identity dot e /\ right_identity dot e.
Definition left_inv {S:Set} (dot:binary_operation) (a' a e:S) := identity dot e -> dot a' a = e.
Definition right_inv {S:Set} (dot:binary_operation) (a' a e:S) := identity dot e -> dot a a' = e.
Definition inv {S:Set} (dot:binary_operation) (a' a e:S) := left_inv dot a' a e /\ right_inv dot a' a e.
Coq, , : https://github.com/tmiya/coq/blob/master/group/group2.v