perga/examples/algebra.pg

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

@include logic.pg

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

-- 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

-- a unary operation on a set `A` is a function `A -> A`
unop (A : *) := A -> A;

-- a binary operation on a set `A` is a function `A -> A -> A`
binop (A : *) := A -> A -> A;

-- a binary operation is associative if ...
assoc (A : *) (op : binop A) :=
    forall (a b c : A), eq A (op a (op b c)) (op (op a b) c);

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

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

-- an element is an identity element if it is both a left and right identity
id (A : *) (op : binop A) (e : A) := and (id_l A op e) (id_r A op e);

-- 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
inv_l (A : *) (op : binop A) (e : A) (a b : A) := eq A (op b a) e;

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

-- and full-on inverse
inv (A : *) (op : binop A) (e : A) (a b : A) := and (inv_l A op e a b) (inv_r A op e a b);

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

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

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

-- 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
id_lm (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : 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);

id_rm (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : 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);

assoc_m (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e) : 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
monoid_id_l_implies_identity
    (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e)
    (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 (op a e) e

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

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

-- the analogous result for right identities
monoid_id_r_implies_identity
    (M : *) (op : binop M) (e : M) (Hmonoid : monoid M op e)
    (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 (op e a) e

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

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

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

group (G : *) (op : binop G) (e : G) (i : unop G) : * :=
    and (monoid G op e)
        (has_inverses G op e i);

-- more "getters"
monoid_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : monoid G op e :=
    and_elim_l (monoid G op e) (has_inverses G op e i) Hgroup;

assoc_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : assoc G op :=
    assoc_m G op e (monoid_g G op e i Hgroup);

id_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : id_l G op e :=
    id_lm G op e (and_elim_l (monoid G op e) (has_inverses G op e i) Hgroup);

id_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) : id_r G op e :=
    id_rm G op e (and_elim_l (monoid G op e) (has_inverses G op e i) Hgroup);

inv_g (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i)  : forall (a : G), inv G op e a (i a) :=
    and_elim_r (monoid G op e) (has_inverses G op e i) Hgroup;

inv_lg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_l G op e a (i a) :=
    and_elim_l (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g G op e i Hgroup a);

inv_rg (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a : G) : inv_r G op e a (i a) :=
    and_elim_r (inv_l G op e a (i a)) (inv_r G op e a (i a)) (inv_g G op e i Hgroup a);

left_inv_unique (G : *) (op : binop G) (e : G) (i : unop G) (Hgroup : group G op e i) (a b : G) (h : inv_l G op e 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 (op b e) (i a)
    -- b = b * e
    (eq_sym G (op b e) b (id_rg G op e i Hgroup b))
    -- b * e = a^-1
    (eq_trans G (op b e) (op b (op a (i a))) (i a)
        --b * e = b * (a * a^-1)
        (eq_cong G G e (op a (i a)) (op b)
            -- e = a * a^-1
            (eq_sym G (op a (i a)) e (inv_rg G op e i Hgroup a)))
        -- b * (a * a^-1) = a^-1
        (eq_trans G (op b (op a (i a))) (op (op b a) (i a)) (i a)
            -- b * (a * a^-1) = (b * a) * a^-1
            (assoc_g G op e i Hgroup b a (i a))
            -- (b * a) * a^-1 = a^-1
            (eq_trans G (op (op b a) (i a)) (op e (i a)) (i a)
                -- (b * a) * a^-1 = e * a^-1
                (eq_cong G G (op b a) e (fun (x : G) => op x (i a)) h)
                -- e * a^-1 = a^-1
                (id_lg G op e i Hgroup (i a)))));