# Idris Algebra

A **semigroup** is a set equipped with a binary operation that is **associative**. This operation is usually called “addition”, though it may actually be something else. In **Idris**, this can expressed with an interface^{1}:

A **monoid** is a semigroup with a **neutral** element, an element that doesn’t change another element when “added” to it:

The **inverse** of an element `x`

is an element `x'`

such that `x <+> x' = neutral`

. It can be proved that in a monoid, an element can only have one inverse:

Informally, this proof says:

`y`

`= y + 0`

`= y + (x + z)`

`= (y + x) + z`

`= 0 + z`

`= z`

A **group** is a monoid in which every element has an inverse:

In this definition, only a **right inverse** is required. Some definitions also call for a **left inverse**, but the existence of a left inverse can instead be derived with a little effort:

In a group, the **inverse of the inverse** of an element is just that element, or more briefly, `-(-x) = x`

. This is a consquence of the **unique inverse theorem**, since `x`

and `-(-x)`

are both inverses of `-x`

:

The **Latin square property** says that for any two elements `a, b`

in a group, there exist `x, y`

such that `a + x = b`

and `y + a = b`

have solutions (unique ones, in fact):

An **abelian group** is a group in which the operation is **commutative**:

A **ring** is an abelian group equipped with another operation, usually called “multiplication”. This operation is associative, and it **distributes** over addition:

In a ring, **multiplying by zero** (that is, the additive identity element) results in zero:

In a ring, a **positive** times a **negative** is negative, and two negatives multiplied together are positive:

A **ring with unity** is a ring with a **multiplicative identity**, i.e. “one”. Terminology is not universally agreed upon here. Some definitions require rings to have a multiplicative identity, and refer to a ring *without* unity as a **“rng”** (a ring without “i”). I think that name is funnier, but it is arguably harder to read.

In a ring with unity, `x * -1 = -x = -1 * x`

:

A **commutative ring** is a ring with commutative multiplication. It doesn’t need to have a unity:

A **field** is a commutative ring with unity whose nonzero elements have **multiplicative inverses**:

The “nonzero” qualifier makes the multiplicative inverse operation somewhat involved: it takes as inputs **both** an element `x`

**and** a **proof** that `x /= 0`

. I don’t yet know of a simple and ergonomic way to use it.

The proofs up to now have been fairly short. Longer proofs come into play when considering **complex numbers**. Normally complex numbers are considered as pairs of real numbers, but in general it’s possible to restrict one’s view to complex numbers over a particular set. In that case, complex numbers are just pairs of elements of that set:

**Adding two complex numbers is easy**: add the real components, then add the imaginary components, then pair up the results, and that’s it. It is easy to prove that complex numbers formed out of numbers that form a semigroup themselves form a semigroup:

Similar reasoning proves the same for monoids and groups.

Complex numbers over rings are much trickier, because **complex multiplication is trickier**: `(a, b) * (c, d) = (ac - bc, ad + bc)`

. Multiplication and addition interact, and there are inverses.

With a lot of effort, it can be proved that the **complex numbers of elements of a ring themselves form a ring**; for example, the subset of complex numbers whose real and imaginary components are both integers. The proofs of distributivity are manageable, but the proof of associativity is real nasty. **It is one of the longest Idris proofs that I have seen.** That is partly due to inherent complexity and partly due to inelegance. It could be cleaned up and shortened.

Here are the proofs in full.

# Exercises

- Clean up and shorten the
**horribly complicated**ring associativity proof. - Some of the proofs here were initially implemented by
**Sventimir**. Later, I came around and reworked them to be shorter and less verbose. One of those initial proofs was left untouched.**Identify it**. - A
**left group**is a semigroup with a left neutral element and left inverses for every element; a**right group**is a semigroup with a right neutral element and right inverses for every element. Prove (in Idris, obviously) that every left group is a right group, and vice versa. - [Extra credit] Fix the interface resolution bug described in
^{1}.

# Footnotes

^{1} The interfaces described here are not exactly what is currently used in Idris. Instead, for each structure, there are **two interfaces**, a **“plain”** version and a **“verified”** version. The plain version is strictly syntactic, defining only operations and elements that need to exist, while the verified version states relations that are expected to hold. In the case of `Semigroup`

, the interfaces are these:

See **“Why Aren’t Idris Interfaces Verified?”** for more details.

**In theory** it should be possible to rewrite these proofs with the split plain / verified interfaces, but **in reality** doing this makes the typechecker reject the proofs. It seems to be a **bug** in compiler’s interface resolution or whatever it’s called, and it is **frustrating**.

This provides an **additional argument** in favor of unifying the interfaces: **it’s hard to deal with complicated hierarchies**, so interfaces should be fewer and simpler.

If you want to compile this code yourself, you will need to use **this branch** (associated with **this PR**).