Elementary Group Theory in Coq

group_theory.v

Require Import Notations.
Generalizable All Variables.
Require Import Setoid.

Class Group {A : Type}(comp: A -> A -> A)(inv: A -> A)(iden: A) := {
  assoc: forall a b c : A, comp a (comp b c) = comp (comp a b) c;
  left_id: forall a : A, comp iden a = a;
  right_id: forall a : A, comp a iden = a;
  left_inv: forall a : A, comp (inv a) a = iden;
  right_inv: forall a : A, comp a (inv a) = iden
}.

Section Elementary_Group_Theory. 

Context `{G:Group A comp inv iden}.

Infix "o" := comp (at level 50).
Notation "a '" := (inv a) (at level 100).

Ltac grp_rw :=
  rewrite (@left_id A comp inv iden G) ||
  rewrite (@right_id A comp inv iden G)||
  rewrite (@assoc A comp inv iden G).

Ltac grp_simpl := repeat grp_rw.

Theorem only_idem_is_id : forall g, ((g o g) = g) -> (g = iden).
Proof.
  intros.
  rewrite <- (@left_inv _ _ _ _ G g).
  rewrite <- H at 3.
  grp_simpl.
  rewrite -> (@left_inv _ _ _ _ G g).
  grp_simpl.
  reflexivity.
Qed.

Theorem cancellation : forall a b c, (a o b = a o c) -> (b = c).
Proof.
  intros.
  rewrite <- (left_id b).
  rewrite <- (left_id c).
  rewrite <- (@left_inv _ _ _ _ G a).
  rewrite <- assoc.
  rewrite <- assoc.
  rewrite <- H.
  reflexivity.
Qed.

End Elementary_Group_Theory.