Require Export abmonoid_.
Require Export cgroup_.

Implicit Arguments On.

Module AbGroup_ <: Cat_Sig_.

Export Misc_.

Section Group_Theory.

Variable A:Type; add:A->A->A; zero:A; opp:A->A.

Record Group_Theory : Prop := {
  ax_add_assoc : (x,y,z:A) (add x (add y z))==(add (add x y) z);
  ax_add_commut : (x,y:A) (add x y)==(add y x);
  ax_zero_sx : (x:A) (add zero x)==x;
  ax_opp_sx : (x:A) (add (opp x) x)==zero
 }.

End Group_Theory.

Record Group_Data : Type := {
  group_carrier :> Type;
  add : group_carrier->group_carrier->group_carrier;
  zero : group_carrier;
  opp : group_carrier->group_carrier
 }.

Implicits zero [1].

Record Group : Type := {
  group_data :> Group_Data;
  group_theory :>
   (Group_Theory (!add group_data) (!zero group_data) (!opp group_data))
 }.

Definition Obj : Type := Group.

Section Group_Facts.

Variable A:Group.

Lemma add_assoc : (x,y,z:A) (add x (add y z))==(add (add x y) z).
Proof.
  Intros; Apply (ax_add_assoc A).
Qed.

Lemma add_commut : (x,y:A) (add x y)==(add y x).
Proof.
  Intros; Apply (ax_add_commut A).
Qed.

Lemma zero_sx : (x:A) (add zero x)==x.
Proof.
  Intros; Apply (ax_zero_sx A).
Qed.

Lemma opp_sx : (x:A) (add (opp x) x)==zero.
Proof.
  Intros; Apply (ax_opp_sx A).
Qed.

Hints Resolve add_assoc add_commut zero_sx opp_sx.

Lemma zero_dx : (x:A) (add x zero)==x.
Proof.
  Intros; Rewrite add_commut; Auto.
Qed.

Lemma opp_dx : (x:A) (add x (opp x))==zero.
Proof.
  Intros; Rewrite add_commut; Auto.
Qed.

Lemma add_sx_cancel : (x,y,z:A) (add x y)==(add x z) -> y==z.
Proof.
  Intros.
  Rewrite <- zero_sx with y.
  Rewrite <- zero_sx with z.
  Rewrite <- opp_sx with x.
  Do 2 Rewrite <- add_assoc.
  Rewrite H.
  Reflexivity.
Qed.

End Group_Facts.

Hints Resolve add_assoc add_commut zero_sx opp_sx add_sx_cancel zero_dx
  opp_dx.

Record Morph_Theory [A,B:Group; f:A->B] : Prop := {
  morph_add : (x,y:A) (f (add x y))==(add (f x) (f y));
  morph_opp : (x:A) (f (opp x))==(opp (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_add g).
  Rewrite (morph_add f).
  Reflexivity.
  Rewrite (morph_opp g).
  Rewrite (morph_opp 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 abmonoid_of_abgroup [A:Group] : AbMonoid_.Monoid.
Proof.
  Intros.
  Split with (AbMonoid_.Build_Monoid_Data (!add A) (!zero A)).
  Abstract NewDestruct (!group_theory A); Split; Simpl; Auto.
Defined.

Definition cgroup_of_abgroup [A:Group] : CGroup_.Group.
Proof.
  Intros.
  Split with (CGroup_.Build_Group_Data (!add A) (!zero A) (!opp A)).
  Abstract NewDestruct (!group_theory A); Split; Simpl; Auto.
Defined.