Playing with formalizing some stuff from Abstract Algebra in Coq.

group_theory.v

(* This is just something I started playing around with. *)
(* The proofs are probably very inefficient and bad. *)
(* Next steps are to be more pedantically accurate in the hierarchy (e.g. *)
(* semigroup, magma, etc.) and also begin formalizing subgroups. *)
(* If I keep having fun, I might start on formalizing some category theory *)
(* stuff as I go, too. *)

Require Import ZArith.
Require Import String.
Require Import Basics.
Require Import Program.Combinators.


(* Every group is a monoid (every monoid is a semigroup is a magma, but let's *)
(* not get carried away. *)
Class Monoid (A : Type) (dot : A -> A -> A) (zero : A) :=
  { dot_assoc : forall x y z : A,
                  dot x (dot y z) = dot (dot x y) z;
    zero_left : forall x, dot zero x = x;
    zero_right : forall x, dot x zero = x
  }.

Definition dot `{Monoid} := dot.
Definition zero `{Monoid} := zero.

Infix "<+>" := dot (at level 50, left associativity).

Class Group {G} `(Monoid G) (inverse : G -> G) :=
  { inverse_left : forall x : G, dot (inverse x) x = zero;
    inverse_right : forall x : G, dot x (inverse x) = zero
  }.

Definition inverse `{Group} := inverse.

(* Useful for 1.1.24(1) below. *)
Lemma unique_unop `{Group} :
  forall x y z,
    dot x y = z -> x = dot z (inverse y).
  intros.
  rewrite <- H1.
  rewrite <- dot_assoc.
  rewrite inverse_right.
  rewrite zero_right.
  trivial.
Qed.

(* These are from Theorem 1.1.24 in Papantonopoulou. *)
(* 1.1.24(1) *)
Theorem identity_unique `{Group} :
  forall e x, dot e x = x -> e = zero.
Proof.
  intros.
  rewrite (unique_unop e x x).
  rewrite inverse_right.
  reflexivity.
  assumption.
Qed.

(* 1.1.24(2) *)
Theorem inverse_unique `{Group} :
  forall a b,
    a <+> b = zero -> a = inverse b /\ b = inverse a.
Proof.
  intros.
  assert ((a <+> b) <+> inverse b = zero <+> inverse b).
  rewrite H1.
  reflexivity.
  assert (inverse a <+> (a <+> b) = inverse a <+> zero).
  rewrite H1.
  reflexivity.
  rewrite <- dot_assoc in H2.
  rewrite inverse_right in H2.
  rewrite zero_right in H2.
  rewrite zero_left in H2.
  rewrite dot_assoc in H3.
  rewrite inverse_left in H3.
  rewrite zero_left in H3.
  rewrite zero_right in H3.
  split.
  assumption.
  assumption.
Qed.

(* 1.1.24(3) *)
Theorem inv_inv `{Group} :
  forall x, inverse (inverse x) = x.
Proof.
  intros.
  transitivity (dot (inverse (inverse x)) (dot (inverse x) x)).
  rewrite inverse_left.
  rewrite zero_right.
  reflexivity.
  rewrite dot_assoc.
  rewrite inverse_left.
  rewrite zero_left.
  reflexivity.
Qed.

(* 1.1.24(4) *)
Theorem inverse_over_product `{Group} :
  forall a b, inverse (a <+> b) = inverse b <+> inverse a.
Proof.
  intros.
  assert (a <+> b <+> (inverse b <+> inverse a) = zero) as Q.
  assert ((a <+> b) <+> (inverse b <+> inverse a)
          = a <+> (b <+> inverse b) <+> inverse a) as Q
      by (repeat rewrite dot_assoc; reflexivity).
  rewrite Q.
  rewrite inverse_right.
  assert (a <+> zero = a).
  rewrite zero_right.
  reflexivity.
  rewrite H1.
  rewrite inverse_right.
  reflexivity.
  destruct (inverse_unique _ _ Q).
  symmetry in H2 .
  assumption.
Qed.

(* TODO: 1.1.24(5) - Cancellation Laws *)
Theorem cancel_left `{Group} :
  forall a b y,
    y <+> a = y <+> b -> a = b.
Proof.
  admit. (* TODO!! *)
Qed.

Theorem cancel_right `{Group} :
  forall a b y,
    a <+> y = b <+> y -> a = b.
Proof.
  admit. (* TODO!! *)
Qed.



(* And here we play with the above machinery because it's fun! *)



(* This is useless since N can't form a group. *)
Instance monoid_nats : Monoid nat plus 0.
Proof.
  split.
  intros.
  apply Plus.plus_assoc.
  apply Plus.plus_0_l.
  apply Plus.plus_0_r.
Qed.

(* This is useless for us too - The free monoid over strings + string concat. *)
(* I couldn't find a built-in exported theorem for associativity of append. *)
Instance monoid_str_concat : Monoid string append EmptyString.
Proof.
  split.
  intros.
  induction x.
  simpl.
  trivial.
  simpl.
  rewrite IHx.
  trivial.
  trivial.
  intros.
  induction x.
  simpl.
  trivial.
  simpl.
  rewrite IHx.
  trivial.
Qed.

(* Functions form a monoid under composition. *)
Instance monoid_functions {A} : Monoid (A -> A) compose id.
Proof.
  split.
  intros.
  rewrite compose_assoc.
  trivial.
  intros.
  rewrite compose_id_left.
  trivial.
  intros.
  rewrite compose_id_right.
  trivial.
Qed.

(* They only form a group if they are all isomorphisms in the respective *)
(* category (bijections in Set). So we can't say much here. *)

Instance monoid_ints : Monoid Z Z.add Z0.
Proof.
  split.
  intros.
  apply Z.add_assoc.
  apply Z.add_0_l.
  apply Z.add_0_r.
Qed.

Instance group_ints : Group monoid_ints Z.opp.
Proof.
  split.
  intros.
  rewrite Z.add_comm.
  rewrite Z.add_opp_diag_r.
  reflexivity.
  intros.
  rewrite Z.add_comm.
  rewrite Z.add_opp_diag_l.
  reflexivity.
Qed.