-- --------------------------------------------------------------------------------------------------------------
-- |                                            BASIC LOGIC                                                     |
-- --------------------------------------------------------------------------------------------------------------

@include logic.pg

-- --------------------------------------------------------------------------------------------------------------
-- |                                        BASIC DEFINITIONS                                                   |
-- --------------------------------------------------------------------------------------------------------------

section BasicDefinitions

    -- note we leave off the type ascriptions for most of these, as the type isn't
    -- very interesting
    -- I'd always strongly recommend including the type ascriptions for theorems

    -- Fix some set A
    variable (A : ★);

    -- a unary operation is a function `A → A`
    def unop := A → A;

    -- a binary operation is a function `A → A → A`
    def binop := A → A → A;

    -- fix some binary operation `op`
    variable (* : binop);
    infixl 20 *;

    -- it is associative if ...
    def assoc := forall (a b c : A), eq A (a * (b * c)) ((a * b) * c);

    -- fix some element `e`
    variable (e : A);

    -- it is a left identity with respect to binop `op` if `∀ a, e * a = a`
    def id_l := forall (a : A), eq A (e * a) a;

    -- likewise for right identity
    def id_r := forall (a : A), eq A (a * e) a;

    -- an element is an identity element if it is both a left and right identity
    def id := id_l ∧ id_r;

    -- b is a left inverse for a if `b * a = e`
    -- NOTE: we don't require `e` to be an identity in this definition.
    --       this definition is purely for convenience's sake
    def inv_l (a b : A) := eq A (b * a) e;

    -- likewise for right inverse
    def inv_r (a b : A) := eq A (a * b) e;

    -- and full-on inverse
    def inv (a b : A) := inv_l a b ∧ inv_r a b;

end BasicDefinitions

-- --------------------------------------------------------------------------------------------------------------
-- |                                      ALGEBRAIC STRUCTURES                                                  |
-- --------------------------------------------------------------------------------------------------------------

-- a set `S` with binary operation `op` is a semigroup if its operation is associative
def semigroup (S : ★) (op : binop S) : ★ := assoc S op;

section Monoid

    -- Let `M` be a set with binary operation `op` and element `e`.
    variable (M : ★) (op : binop M) (e : M);

    -- We'll use `*` as an infix shorthand for `op`
    def * (a b : M) := op a b;
    infixl 50 *;

    -- a set `M` with binary operation `op` and element `e` is a monoid 
    def monoid : ★ := (semigroup M op) ∧ (id M op e);

    -- Suppose `(M, *, e)` is a monoid
    hypothesis (Hmonoid : monoid);

    -- some "getters" for `monoid` so we don't have to do a bunch of very verbose
    -- and-eliminations every time we want to use something
    def id_lm : id_l M op e :=
        and_elim_l (id_l M op e) (id_r M op e)
            (and_elim_r (semigroup M op) (id M op e) Hmonoid);

    def id_rm : id_r M op e :=
        and_elim_r (id_l M op e) (id_r M op e)
            (and_elim_r (semigroup M op) (id M op e) Hmonoid);

    def assoc_m : assoc M op := and_elim_l (semigroup M op) (id M op e) Hmonoid;

    -- now we can prove that, for any monoid, if `a` is a left identity, then it
    -- must be "the" identity
    def monoid_id_l_implies_identity (a : M) (H : id_l M op a) : eq M a e :=
            -- WTS a = a * e = e
            -- we can use `eq_trans` to glue proofs of `a = a * e` and `a * e = e` together
            eq_trans M a (a * e) e

                -- first, `a = a * e`, but we'll use `eq_sym` to flip it around
                (eq_sym M (a * e) a
                    -- now the goal is to show `a * e = a`, which follows immediately from `id_r`
                    (id_rm a))

                -- now we need to show that `a * e = e`, but this immediately follows from `H`
                (H e);

    -- the analogous result for right identities
    def monoid_id_r_implies_identity (a : M) (H : id_r M op a) : eq M a e :=
            -- this time, we'll show `a = e * a = e`
            eq_trans M a (e * a) e

                -- first, `a = e * a`
                (eq_sym M (e * a) a
                    -- this time, it immediately follows from `id_l`
                    (id_lm a))

                -- and `e * a = e`
                (H e);

end Monoid

section Group

    variable (G : ★) (op : binop G) (e : G) (i : unop G);

    def * (a b : G) := op a b;
    infixl 50 *;

    -- groups are just monoids with inverses
    def has_inverses : ★ := forall (a : G), inv G op e a (i a);

    def group : ★ := (monoid G op e) ∧ has_inverses;

    hypothesis (Hgroup : group);

    -- more "getters"
    def monoid_g : monoid G op e := and_elim_l (monoid G op e) has_inverses Hgroup;
    def assoc_g : assoc G op := assoc_m G op e monoid_g;
    def id_lg : id_l G op e := id_lm G op e (and_elim_l (monoid G op e) has_inverses Hgroup);
    def id_rg : id_r G op e := id_rm G op e (and_elim_l (monoid G op e) has_inverses Hgroup);
    def inv_g : forall (a : G), inv G op e a (i a) := and_elim_r (monoid G op e) has_inverses Hgroup;
    def left_inverse (a b : G)  := inv_l G op e a b;
    def right_inverse (a b : G) := inv_r G op e a b;
    def inv_lg (a : G) : left_inverse a (i a)  := and_elim_l (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g a);
    def inv_rg (a : G) : right_inverse a (i a) := and_elim_r (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g a);

    -- An interesting theorem: left inverses are unique, i.e. if b * a = e, then b = a^-1
    def left_inv_unique (a b : G) (h : left_inverse a b) : eq G b (i a) :=
        -- b = b * e
        --   = b * (a * a^-1)
        --   = (b * a) * a^-1
        --   = e * a^-1
        --   = a^-1
        eq_trans G b (b * e) (i a)
        -- b = b * e
        (eq_sym G (b * e) b (id_rg b))
        -- b * e = a^-1
        (eq_trans G (b * e) (b * (a * i a)) (i a)
            --b * e = b * (a * a^-1)
            (eq_cong G G e (a * i a) (op b)
                -- e = a * a^-1
                (eq_sym G (a * i a) e (inv_rg a)))
            -- b * (a * a^-1) = a^-1
            (eq_trans G (b * (a * i a)) (b * a * i a) (i a)
                -- b * (a * a^-1) = (b * a) * a^-1
                (assoc_g b a (i a))
                -- (b * a) * a^-1 = a^-1
                (eq_trans G (b * a * i a) (e * i a) (i a)
                    -- (b * a) * a^-1 = e * a^-1
                    (eq_cong G G (b * a) e (fun (x : G) => x * i a) h)
                    -- e * a^-1 = a^-1
                    (id_lg (i a)))));

    -- And so are right inverses
    def right_inv_unique (a b : G) (h : right_inverse a b) : eq G b (i a) :=
        -- b = e * b
        --   = (a^-1 * a) * b
        --   = a^-1 * (a * b)
        --   = a^-1 * e
        --   = a^-1
        eq_trans G b (e * b) (i a)
        -- b = e * b
        (eq_sym G (e * b) b (id_lg b))
        -- e * b = a^-1
        (eq_trans G (e * b) (i a * a * b) (i a)
            -- e * b = (a^-1 * a) * b
            (eq_cong G G e (i a * a) (fun (x : G) => x * b)
                -- e = (a^-1 * a)
                (eq_sym G (i a * a) e (inv_lg a)))

            -- (a^-1 * a) * b = a^-1
            (eq_trans G (i a * a * b) (i a * (a * b)) (i a)
                -- (a^-1 * a) * b = a^-1 * (a * b)
                (eq_sym G (i a * (a * b)) (i a * a * b) (assoc_g (i a) a b))

                -- a^-1 * (a * b) = a^-1
                (eq_trans G (i a * (a * b)) (i a * e) (i a)
                    -- a^-1 * (a * b) = a^-1 * e
                    (eq_cong G G (a * b) e (op (i a)) h)

                    -- a^-1 * e = a^-1
                    (id_rg (i a)))));

    -- the classic shoes and socks theorem, namely that (a * b)^-1 = b^-1 * a^-1
    def shoes_and_socks (a b : G) : eq 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)
        -- WTS: (a * b) * (b^-1 * a^-1) = e
        (let
            -- helper function to prove that x * a^-1 = y * a^-1 given x = y
            (under_ai (x y : G) (h : eq G x y) := eq_cong G G x y (fun (z : G) => z * (i a)) h)
         in
            -- (a * b) * (b^-1 * a^-1) = ((a * b) * b^-1) * a^-1
            --                         = (a * (b * b^-1)) * a^-1
            --                         = (a * e) * a^-1
            --                         = a * a^-1
            --                         = e
            eq_trans G (a * b * (i b * i a)) (a * b * i b * i a) e
            -- (a * b) * (b^-1 * a^-1) = ((a * b) * b^-1) * a^-1
            (assoc_g (a * b) (i b) (i a))
            -- ((a * b) * b^-1) * a^-1 = e
            (eq_trans G (a * b * i b * i a) (a * (b * i b) * i a) e
                -- ((a * b) * b^-1) * a^-1 = (a * (b * b^-1)) * a^-1
                (under_ai (a * b * i b) (a * (b * i b)) (eq_sym G (a * (b * i b)) (a * b * i b) (assoc_g a b (i b))))

                -- (a * (b * b^-1)) * a^-1 = e
                (eq_trans G (a * (b * i b) * i a) (a * e * i a) e
                    -- (a * (b * b^-1)) * a^-1 = (a * e) * a^-1
                    (eq_cong G G (b * i b) e (fun (x : G) => (a * x * i a)) (inv_rg b))

                    -- (a * e) * a^-1 = e
                    (eq_trans G (a * e * i a) (a * i a) e
                        -- (a * e) * a^-1 = a * a^-1
                        (under_ai (a * e) a (id_rg a))

                        -- a * a^-1 = e
                        (inv_rg a))))
         end));

end Group