Module group

Require Export monoid.

Implicit Arguments On.

Record Group_Theory [A:Type; op:A->A->A; id:A; iv:A->A] : Prop := {
  group_assoc : (x,y,z:A)(op x (op y z))==(op (op x y) z);
  group_sx_id : (x:A)(op id x)==x;
  group_sx_iv : (x:A)(op (iv x) x)==id
}.
Hints Resolve Build_Group_Theory : grp.

Section PPP.
  Variables A:Type; op:A->A->A; id:A; iv:A->A.
  Definition A_of_Group_Theory [AT:(Group_Theory op id iv)] : Type := A.
  Definition Op_of_Group_Theory [AT:(Group_Theory op id iv)] : A->A->A := op.
  Definition Id_of_Group_Theory [AT:(Group_Theory op id iv)] : A := id.
  Definition Iv_of_Group_Theory [AT:(Group_Theory op id iv)] : A->A := iv.
End PPP.

Section Group_Theory_Facts.
  Variables A:Type; op:A->A->A; id:A; iv:A->A.
  Hypothesis AT : (Group_Theory op id iv).

  Lemma group_sx_cancel :
    (x,y,z:A) (op x y)==(op x z) -> y==z.
  Proof.
    NewDestruct AT; Intros.
    Transitivity (op (iv x) (op x y)).
    Rewrite (group_assoc AT); Rewrite (group_sx_iv AT); Auto.
    Rewrite H.
    Rewrite (group_assoc AT); Rewrite (group_sx_iv AT); Auto.
  Qed.

  Lemma group_dx_id : (x:A)(op x id)==x.
  Proof.
    Decompose Record AT.
    Simpl; Intros.
    Apply group_sx_cancel with (iv x).
    Rewrite (group_assoc AT); Rewrite group_sx_iv0; Auto.
  Qed.
  Hints Resolve group_dx_id.

  Lemma group_dx_iv : (x:A)(op x (iv x))==id.
  Proof.
    NewDestruct AT; Simpl; Intros.
    Apply group_sx_cancel with (iv x).
    Rewrite (group_assoc AT).
    Rewrite (group_sx_iv AT).
    Transitivity (iv x); Auto.
  Qed.
  Hints Resolve group_dx_iv.

  Lemma group_iv_inj : (x,y:A)(iv x)==(iv y)->x==y.
  Proof.
    Decompose Record AT.
    Intros.
    Apply group_sx_cancel with (iv x).
    Rewrite group_sx_iv0; Rewrite H; Auto.
  Qed.
  Hints Resolve group_iv_inj.

  Lemma group_iv_id : (iv id)==id.
  Proof.
    Apply group_sx_cancel with id.
    Rewrite group_dx_iv; Auto.
  Qed.
  Hints Resolve group_iv_id.

  Lemma group_iv_iv : (x:A)(iv (iv x))==x.
  Proof.
    Decompose Record AT.
    Intros.
    Apply group_sx_cancel with (iv x).
    Rewrite group_sx_iv0; Auto.
  Qed.
  Hints Resolve group_iv_iv.

  Lemma group_iv_op : (x,y:A)(iv (op x y))==(op (iv y) (iv x)).
  Proof.
    Decompose Record AT.
    Intros.
    Apply group_sx_cancel with (op x y).
    Rewrite group_dx_iv.
    Transitivity (op x (op (op y (iv y)) (iv x))).
    Rewrite group_dx_iv; Rewrite (group_sx_id AT); Auto.
    Do 3 Rewrite (group_assoc AT); Reflexivity.
  Qed.
  Hints Resolve group_iv_op.

  Lemma group_dx_cancel :
    (x,y,z:A) (op y x)==(op z x) -> y==z.
  Proof.
    Intros.
    Transitivity (op (op y x) (iv x)).
    Rewrite <- (group_assoc AT); Rewrite group_dx_iv; Auto.
    Rewrite H.
    Rewrite <- (group_assoc AT); Rewrite group_dx_iv; Auto.
  Qed.

  Lemma group_id_sx_char : (x,y:A) (op x y)==y -> x==id.
  Proof.
    NewDestruct AT; Intros.
    Apply group_dx_cancel with y.
    Transitivity y; Auto.
  Qed.

  Lemma group_id_dx_char : (x,y:A) (op y x)==y -> x==id.
  Proof.
    Intros.
    Apply group_sx_cancel with y.
    Transitivity y; Auto.
  Qed.

  Lemma group_iv_sx_char : (x,y:A) (op x y)==id -> x==(iv y).
  Proof.
    NewDestruct AT; Intros.
    Apply group_dx_cancel with y.
    Transitivity id; Auto.
  Qed.

  Lemma group_iv_dx_char : (x,y:A) (op y x)==id -> x==(iv y).
  Proof.
    Intros.
    Apply group_sx_cancel with y.
    Transitivity id; Auto.
  Qed.

  Lemma group_switch : (x,y:A) (op x y)==id -> (op y x)==id.
  Proof.
    NewDestruct AT; Intros.
    Apply group_sx_cancel with (iv y).
    Rewrite (group_assoc AT).
    Rewrite (group_sx_iv AT).
    Rewrite (group_sx_id AT).
    Rewrite group_dx_id.
    Apply group_dx_cancel with y.
    Transitivity id; Auto.
  Qed.
End Group_Theory_Facts.

Lemma group_theory_monoid :
  (A:Type; op:A->A->A; id:A; iv:A->A; AT:(Group_Theory op id iv))
  (Monoid_Theory op id).
Proof.
Intros; Split.
Apply (group_assoc AT).
Apply (group_sx_id AT).
Apply (group_dx_id AT).
Qed.
Hints Resolve group_theory_monoid : grp.

Coercion group_theory_monoid : Group_Theory >-> Monoid_Theory.

Record Group_Data : Type := {
  group_carrier :> Type;
  op : group_carrier->group_carrier->group_carrier;
  id : group_carrier;
  iv : group_carrier->group_carrier
}.

Syntactic Definition is_a_group := [GD:Group_Data]
  (Group_Theory (!op GD) (id GD) (!iv GD)).

Record Group : Type := {
  group_data :> Group_Data;
  group_theory :>
    (Group_Theory (!op group_data) (id group_data) (!iv group_data))
}.
Hints Resolve group_theory : grp.

Section Group_Facts.
  Variable G : Group.
  
  Definition op_assoc := (group_assoc G).
  Definition op_sx_id := (group_sx_id G).
  Definition op_sx_iv := (group_sx_iv G).
  Definition op_dx_id := (group_dx_id G).
  Definition op_dx_iv := (group_dx_iv G).
  Definition iv_op := (group_iv_op G).
  Definition iv_iv := (group_iv_iv G).
  Definition op_switch := (group_switch G).

  Definition id_sx_char := (group_id_sx_char G).
  Definition id_dx_char := (group_id_dx_char G).
  Definition iv_sx_char := (group_iv_sx_char G).
  Definition iv_dx_char := (group_iv_dx_char G).
End Group_Facts.

Hints Resolve op_assoc op_sx_id op_sx_iv op_dx_id op_dx_iv iv_op
  iv_iv op_sx_iv iv_sx_char iv_dx_char : grp.

Hint Rewrite [op_sx_id op_sx_iv op_dx_id op_dx_iv iv_op iv_iv] in grp.

Record Group_Morph [A,B:Group_Data] : Type := {
  group_morph_carrier :> A->B;
  group_morph_op :> (x,y:A)
    (group_morph_carrier (op x y))==
      (op (group_morph_carrier x) (group_morph_carrier y))
}.
Hints Resolve group_morph_op : grp.

Lemma group_morph_extensionality : (A,B:Group_Data; f,g:(Group_Morph A B))
  ((x:A)(f x)==(g x)) -> f==g.
Proof.
  NewDestruct f; NewDestruct g; Intros.
  Assert group_morph_carrier0==group_morph_carrier1.
  Apply nondep_extensionality; Trivial.
  NewDestruct H0.
  Assert group_morph_op0==group_morph_op1.
  Apply proof_irrelevance.
  NewDestruct H0.
  Reflexivity.
Qed.

Section group_morph_facts.
  Variable A,B:Group.
  Variable f:(Group_Morph A B).
  Variable x:A.

  Lemma group_morph_id : (f (id A))==(id B).
  Proof.
    Apply (group_id_sx_char B) with (f (id A)).
    Rewrite <- (group_morph_op f).
    Rewrite (group_sx_id A); Reflexivity.
  Qed.

  Lemma group_morph_iv : (f (iv x))==(iv (f x)).
  Proof.
    Apply (group_iv_dx_char B).
    Rewrite <- (group_morph_op f).
    Rewrite (group_dx_iv A).
    Apply group_morph_id.
  Qed.
End group_morph_facts.

Section Group_Morph_Comp.
  Variable A, B, C : Group.
  Variable g : (Group_Morph B C).
  Variable f : (Group_Morph A B).

  Syntactic Definition h := [x:A](g (f x)).

  Remark h_th : (x,y:A) (h (op x y))==(op (h x) (h y)).
  Proof.
  Simpl; Intros.
  Rewrite (group_morph_op f).
  Rewrite (group_morph_op g).
  Reflexivity.
  Qed.

  Definition group_morph_comp : (Group_Morph A C).
  Proof.
  Split with h.
  Apply h_th.
  Defined.

  Lemma group_morph_comp_eq : (x:A)
   (group_morph_comp x)==(g (f x)).
  Proof.
  Reflexivity.
  Qed.
End Group_Morph_Comp.

Hints Resolve group_morph_comp_eq : grp.

Record CGroup_Theory [A:Type; op:A->A->A; id:A; iv:A->A] : Prop := {
  cgroup_group_theory :> (Group_Theory op id iv);
  cgroup_comm : (x,y:A)(op x y)==(op y x)
}.
Hints Resolve Build_CGroup_Theory cgroup_group_theory : grp.

Lemma cgroup_iv_op :
  (A:Type; op:A->A->A; id:A; iv:A->A; AT:(CGroup_Theory op id iv))
  (x,y:A) (iv (op x y))==(op (iv x) (iv y)).
Proof.
Intros.
Rewrite (group_iv_op AT).
Apply (cgroup_comm AT).
Qed.
Hints Resolve cgroup_iv_op : grp.

Record CGroup_Data : Type := {
  cgroup_carrier :> Type;
  add : cgroup_carrier->cgroup_carrier->cgroup_carrier;
  zero : cgroup_carrier;
  opp : cgroup_carrier->cgroup_carrier
}.

Syntactic Definition is_a_cgroup := [GD:CGroup_Data]
  (CGroup_Theory (!add GD) (zero GD) (!opp GD)).

Record CGroup : Type := {
  cgroup_data :> CGroup_Data;
  cgroup_theory :>
    (CGroup_Theory (!add cgroup_data) (zero cgroup_data)
      (!opp cgroup_data))
}.
Hints Resolve group_theory : grp.

Lemma add_assoc : (G:CGroup; x,y,z:G)
  (add x (add y z))==(add (add x y) z).
Proof.
Intros; Simpl; Apply (group_assoc G).
Qed.
Hints Resolve add_assoc : grp.

Lemma add_sx_zero : (G:CGroup; x:G)
  (add (zero G) x)==x.
Proof.
Intros; Simpl; Apply (group_sx_id G).
Qed.
Hints Resolve add_sx_zero : grp.