group_defined_structure.v

Structure group M := {
  id : M;
  bin : M -> M -> M;
  inverse : M -> M;
  assoc : forall x y z, bin x (bin y z) = bin (bin x y) z;
  idR : forall g, bin g id = g;
  idL : forall g, bin id g = g;
  invR : forall g, bin g (inverse g) = id;
  invL : forall g, bin (inverse g) g = id
}.

Structure hom M G M' G' := {
  f : M -> M';
  hom_law : forall x y, f (bin M G x y) = bin M' G' (f x) (f y)
}.

Lemma both_sides_L : forall {M : Type} (bin : M -> M -> M) (x y z : M),
  x = y -> bin z x = bin z y.
Proof.
  intros.
  rewrite H.
  reflexivity.
Qed.

Example hom_id_map_id : forall {M M' : Type} (G : group M) (G' : group M') (h : hom M G M' G'),
  f M G M' G' h (id M G) = id M' G'.
Proof.
  intros.
  assert (f M G M' G' h (id M G) = f M G M' G' h (bin M G (id M G) (id M G)))
    as f_id_G_eq_f__id_G_id_G
    by (rewrite (idR M G (id M G)); reflexivity).

  rewrite (hom_law M G M' G' h (id M G) (id M G)) in f_id_G_eq_f__id_G_id_G.
  rename f_id_G_eq_f__id_G_id_G into f_id_G_eq_f_id_G_f_id_G.

  apply (both_sides_L (bin M' G') (f M G M' G' h (id M G)) (bin M' G' (f M G M' G' h (id M G)) (f M G M' G' h (id M G))) (inverse M' G' (f M G M' G' h (id M G))))
    in f_id_G_eq_f_id_G_f_id_G.
  rename f_id_G_eq_f_id_G_f_id_G into inv_f_id_G_f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.

  rewrite (assoc M' G' (inverse M' G' (f M G M' G' h (id M G))) (f M G M' G' h (id M G)) (f M G M' G' h (id M G)))
    in inv_f_id_G_f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.

  rewrite (invL M' G' (f M G M' G' h (id M G)))
    in inv_f_id_G_f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.
  rename inv_f_id_G_f_id_G_eq_inv_f_id_G_f_id_G_f_id_G
    into f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.

  rewrite (idL M' G' (f M G M' G' h (id M G))) in f_id_G_eq_inv_f_id_G_f_id_G_f_id_G.
  symmetry.
  assumption.
Qed.