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 interface1:
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 + 0
= y + (x + z)
= (y + x) + z
= 0 + 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 xand 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.
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.
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:
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).