Require Export monoid.

Implicit Arguments On.

Module Group <: Cat_Sig.

Export Misc.

Section Group_Theory.

Variable A:Type; mul:A->A->A; one:A; inv:A->A.

Record Group_Theory : Prop := {
  ax_mul_assoc : (x,y,z:A) (mul x (mul y z))==(mul (mul x y) z);
  ax_one_sx : (x:A) (mul one x)==x;
  ax_inv_sx : (x:A) (mul (inv x) x)==one
 }.

End Group_Theory.

Record Group_Data : Type := {
  group_carrier :> Type;
  mul : group_carrier->group_carrier->group_carrier;
  one : group_carrier;
  inv : group_carrier->group_carrier
 }.

Implicits one [1].

Record Group : Type := {
  group_data :> Group_Data;
  group_theory :>
   (Group_Theory (!mul group_data) (!one group_data) (!inv group_data))
 }.

Definition Obj : Type := Group.

Section Group_Facts.

Variable A:Group.

Lemma mul_assoc : (x,y,z:A) (mul x (mul y z))==(mul (mul x y) z).
Proof.
  Intros; Apply (ax_mul_assoc A).
Qed.

Lemma one_sx : (x:A) (mul one x)==x.
Proof.
  Intros; Apply (ax_one_sx A).
Qed.

Lemma inv_sx : (x:A) (mul (inv x) x)==one.
Proof.
  Intros; Apply (ax_inv_sx A).
Qed.

Hints Resolve mul_assoc one_sx inv_sx.

Lemma mul_sx_cancel : (x,y,z:A) (mul x y)==(mul x z) -> y==z.
Proof.
  Intros.
  Rewrite <- one_sx with y.
  Rewrite <- one_sx with z.
  Rewrite <- inv_sx with x.
  Do 2 Rewrite <- mul_assoc.
  Rewrite H.
  Reflexivity.
Qed.

Lemma one_dx : (x:A) (mul x one)==x.
Proof.
  Intros; Apply mul_sx_cancel with (inv x).
  Rewrite mul_assoc.
  Rewrite inv_sx; Auto.
Qed.

Hints Resolve one_dx.

Lemma inv_dx : (x:A) (mul x (inv x))==one.
Proof.
  Intros; Apply mul_sx_cancel with (inv x).
  Rewrite mul_assoc.
  Rewrite inv_sx.
  Transitivity (inv x); Auto.
Qed.

End Group_Facts.

Hints Resolve mul_assoc one_sx inv_sx mul_sx_cancel one_dx inv_dx.

Record Morph_Theory [A,B:Group; f:A->B] : Prop := {
  morph_mul : (x,y:A) (f (mul x y))==(mul (f x) (f y));
  morph_inv : (x:A)(f (inv x))==(inv (f x))
 }.

Record Group_Morph [A,B:Group] : Type := {
  morph_data :> A->B;
  morph_theory :> (Morph_Theory morph_data)
 }.

Definition Morph [A,B:Group] : Type := (Group_Morph A B).

Lemma morph_extens : (A,B:Group; f,g:(Morph A B))
 ((x:A)(f x)==(g x)) -> f==g.
Proof.
  NewDestruct f; NewDestruct g; Simpl; Intros.
  Assert U : morph_data0 == morph_data1.
  Apply nondep_extensionality; Assumption.
  NewDestruct U.
  Assert U : morph_theory0 == morph_theory1.
  Apply proof_irrelevance.
  NewDestruct U.
  Reflexivity.
Qed.

Section morph_comp.

Variable A,B,C:Group.

Variable f:(Morph B C); g:(Morph A B).

Local h [x:A] : C := (f (g x)).

Remark h_th : (Morph_Theory h).
Proof.
  Unfold h; Split; Intros.
  Rewrite (morph_mul g).
  Rewrite (morph_mul f).
  Reflexivity.
  Rewrite (morph_inv g).
  Rewrite (morph_inv f).
  Reflexivity.
Qed.

Definition morph_comp : (Morph A C).
Proof.
  Split with h;
  Apply h_th.
Defined.

End morph_comp.

Definition morph_id [A:Group] : (Morph A A).
Proof.
  Intros.
  Split with [x:A]x.
  Abstract Split; Auto.
Defined.

Implicits morph_id [1].

Lemma morph_comp_assoc : (A,B,C,D:Group)
 (h:(Morph C D); g:(Morph B C); f:(Morph A B))
 (morph_comp h (morph_comp g f))==(morph_comp (morph_comp h g) f).
Proof.
  Intros; Apply morph_extens; Trivial.
Qed.

Lemma morph_id_sx : (A,B:Group; f:(Morph A B))
 (morph_comp morph_id f)==f.
Proof.
  Intros; Apply morph_extens; Trivial.
Qed.

Lemma morph_id_dx : (A,B:Group; f:(Morph A B))
 (morph_comp f morph_id)==f.
Proof.
  Intros; Apply morph_extens; Trivial.
Qed.

Definition monoid_of_group [A:Group] : Monoid.Monoid.
Proof.
  Intros.
  Split with (Monoid.Build_Monoid_Data (!mul A) (!one A)).
  Abstract NewDestruct (!group_theory A); Split; Simpl; Auto.
Defined.