@include logic.pg

section Magma

variable (G H : ★);
def binop (A : ★) := A → A → A;

def = := eq G;
infixl 1 =;

def ~ := eq H;
infixl 1 ~;

variable (* : binop G);
infixl 20 *;

variable (+ : binop H);
infixl 20 +;

variable (f : G → H);
hypothesis (f_homo : forall (a b : G), f (a * b) ~ f a * f b);

def *> (a b : G) := b * a;
infixl 20 *>;

section Semigroup

hypothesis (assocG : forall (a b c : G), a * (b * c) = a * b * c);
hypothesis (assocH : forall (a b c : H), a + (b + c) ~ a + b + c);

def assoc_op (a b c : G) : a *> (b *> c) = a *> b *> c := 
    eq_sym G (a *> b *> c) (a *> (b *> c)) (assocG c b a);

section Monoid

variable (e : G);
variable (eH : H);

hypothesis (id_lG : forall (a : G), e * a = a);
hypothesis (id_rG : forall (a : G), a * e = a);

hypothesis (id_lH : forall (a : H), e * a = a);
hypothesis (id_rH : forall (a : H), a * e = a);

def id_l_op : forall (a : G), e *> a = a := id_rG;
def id_r_op : forall (a : G), a *> e = a := id_lG;

def left_id_unique (a : G) (H : forall (b : G), a * b = b) : a = e :=
    eq_trans G a (a * e) e (eq_sym G (a * e) a (id_rG a)) (H e);

def right_id_unique (a : G) (H : forall (b : G), b * a = b) : a = e := #left_id_unique G (*>) e id_lG a H;

section Group

variable (i : G → G);
hypothesis (inv_lG : forall (a : G), i a * a = e);
hypothesis (inv_rG : forall (a : G), a * i a = e);

variable (j : H → H);
hypothesis (inv_lH : forall (a : H), j a * a ~ eH);
hypothesis (inv_rH : forall (a : H), a * j a ~ eH);

def left_inv_unique (a b : G) (h : b * a = e) : b = i a :=
    eq_trans G b (b * e) (i a)
        (eq_sym G (b * e) b (id_rG b))
        (eq_trans G (b * e) (b * (a * i a)) (i a)
            (eq_cong G G e (a * i a) ((*) b)
                (eq_sym G (a * i a) e (inv_rG a)))
            (eq_trans G (b * (a * i a)) (b * a * i a) (i a)
                (assocG b a (i a))
                (eq_trans G (b * a * i a) (e * i a) (i a)
                    (eq_cong G G (b * a) e ([z : G] z * i a) h)
                    (id_lG (i a)))));

def right_inv_unique (a b : G) (h : a * b = e) : b = i a :=
    #left_inv_unique G (*>) assoc_op e id_rG id_lG i inv_lG a b h;

def homo_preserve_inv (a : G) : f (i a) ~ j (f a) :=
    #left_inv_unique H (+) assocH eH id_lH id_rH j inv_rH (f a) (f (i a))
    (eq_trans H (f a * f (i a)) (f (a * i a)) 
    )
        -- WTS: f a * f (i a) ~ eH

def inverse_involutive (a : G) : i (i a) = a :=
    eq_sym G a (i (i a)) (right_inv_unique (i a) a (inv_lG a));

def shoes_and_socks (a b : G) : i (a * b) = i b * i a :=
    eq_sym G (i b * i a) (i (a * b))
    (right_inv_unique (a * b) (i b * i a)
    (let
        (under_ai (x y : G) (h : x = y) := eq_cong G G x y ([z : G] z * (i a)) h)
     in
        eq_trans G (a * b * (i b * i a)) (a * b * i b * i a) e
        (assocG (a * b) (i b) (i a))
        (eq_trans G (a * b * i b * i a) (a * (b * i b) * i a) e
            (under_ai (a * b * i b) (a * (b * i b)) (eq_sym G (a * (b * i b)) (a * b * i b) (assocG a b (i b))))
            (eq_trans G (a * (b * i b) * i a) (a * e * i a) e
                (eq_cong G G (b * i b) e (fun (x : G) => (a * x * i a)) (inv_rG b))
                (eq_trans G (a * e * i a) (a * i a) e
                    (under_ai (a * e) a (id_rG a))
                    (inv_rG a))))
     end));

def cancel_l (a b c : G) (h : a * b = a * c) : b = c :=
    eq_trans G b (e * b) c
        (eq_sym G (e * b) b (id_lG b))
        (eq_trans G (e * b) (i a * a * b) c
            (eq_cong G G e (i a * a) ([x : G] x * b)
                (eq_sym G (i a * a) e (inv_lG a)))
            (eq_trans G (i a * a * b) (i a * (a * b)) c
                (eq_sym G (i a * (a * b)) (i a * a * b) (assocG (i a) a b))
                (eq_trans G (i a * (a * b)) (i a * (a * c)) c
                    (eq_cong G G (a * b) (a * c) ((*) (i a)) h)
                    (eq_trans G (i a * (a * c)) (i a * a * c) c
                        (assocG (i a) a c)
                        (eq_trans G (i a * a * c) (e * c) c
                            (eq_cong G G (i a * a) e ([x : G] x * c) (inv_lG a))
                            (id_lG c))))));

def cancel_r (a b c : G) (h : b * a = c * a) : b = c :=
    #cancel_l G (*>) assoc_op e id_rG i inv_rG a b c h;

def abelian : ★ := forall (a b : G), a * b = b * a;

def left_right_cancel : (forall (x y z : G), x * y = z * x → y = z) → abelian :=
    fun (h : forall (x y z : G), x * y = z * x → y = z) (a b : G) =>
        h (i a) (a * b) (b * a)
        (eq_trans G (i a * (a * b)) (i a * a * b) (b * a * i a)
            (assocG (i a) a b)
            (eq_trans G (i a * a * b) (e * b) (b * a * i a)
                (eq_cong G G (i a * a) e ([x : G] x * b) (inv_lG a))
                (eq_trans G (e * b) b (b * a * i a)
                    (id_lG b)
                    (eq_trans G b (b * e) (b * a * i a)
                        (eq_sym G (b * e) b (id_rG b))
                        (eq_trans G (b * e) (b * (a * i a)) (b * a * i a)
                            (eq_cong G G e (a * i a) ((*) b) (eq_sym G (a * i a) e (inv_rG a)))
                            (assocG b a (i a)))))));

def inv_distrib_abelian : (forall (a b : G), i (a * b) = i a * i b) → abelian :=
    fun (h : forall (a b : G), i (a * b) = i a * i b) (a b : G) =>
        eq_trans G (a * b) (i (i a) * b) (b * a)
            (eq_cong G G a (i (i a)) ([x : G] x * b) (eq_sym G (i (i a)) a (inverse_involutive a)))
            (eq_trans G (i (i a) * b) (i (i a) * i (i b)) (b * a)
                (eq_cong G G b (i (i b)) ((*) (i (i a))) (eq_sym G (i (i b)) b (inverse_involutive b)))
                (eq_trans G (i (i a) * i (i b)) (i (i b * i a)) (b * a)
                    (eq_sym G (i (i b * i a)) (i (i a) * i (i b)) (shoes_and_socks (i b) (i a)))
                    (eq_trans G (i (i b * i a)) (i (i b) * i (i a)) (b * a)
                        (h (i b) (i a))
                        (eq_trans G (i (i b) * i (i a)) (b * i (i a)) (b * a)
                            (eq_cong G G (i (i b)) b ([x : G] x * i (i a)) (inverse_involutive b))
                            (eq_cong G G (i (i a)) a ((*) b) (inverse_involutive a))))));

def order_two (a : G) : a * a = e → a = i a := right_inv_unique a a;

def all_order_two_abelian : (forall (a : G), a * a = e) → abelian :=
    fun (h : forall (a : G), a * a = e) =>
        inv_distrib_abelian (fun (a b : G) =>
            (eq_trans G (i (a * b)) (a * b) (i a * i b)
                (eq_sym G (a * b) (i (a * b)) (order_two (a * b) (h (a * b))))
                (eq_trans G (a * b) (a * i b) (i a * i b)
                    (eq_cong G G b (i b) ((*) a) (order_two b (h b)))
                    (eq_cong G G a (i a) ([x : G] x * i b) (order_two a (h a))))));

end Group
end Monoid
end Semigroup
end Magma