Arithmetic of natural numbers
A search for terms like
arithmetic and
natural on
hackage reveals no shortage of libraries for handling the arithmetic
of natural numbers. How is this library any different some of the
others? It has a particular purpose: providing a foundation on top on
which other libraries may define types indexed by sizes. This uses
GHC's non-inductively-defined
GHC.TypeNats.Nat. As a rule, this
does not use
unsafeCoerce internally anywhere.
Perhaps the most direct competitor to `natural-arithmetic` is a
typechecker plugin like
type-nat-solver. The big difference is
that `type-nat-solver` can really only be used in application code,
not in library code. This is because libraries should not require the
presence of typechecker plugins. Technically, they can (you could
document it), but many developers will not use libraries that have
unusual install procedures like this.
This library, in places, requires users to use the
TypeApplications language extension. This is done when a number
is only need at the type level (without a runtime witness).
This library uses a non-minimal core, providing redundant primitives
in
Arithmetic.Lt and
Arithmetic.Lte. This is done in the
interest of making it easy for user to assemble proofs. Recall that
proof assembly is done by hand rather than by an SMT solver, so
removing some tediousness from this is helpful to users.
This library provides left and variants variants of several functions.
For example,
Arithmetic.Lte provides both
substituteL
and
substituteR. This is only done when there are two variants
of a function. For substitution, this is the case because we have `b =
c, a ≤ b ==> a ≤ c` and `a = c, a ≤ b ==> c ≤ b`. So, we provide
both
substituteL and
substituteR. However, for addition
of inequalities, we have four possible variants: `a ≤ b, c ≤ d ==>
a + c ≤ b + d`, `a ≤ b, c ≤ d ==> c + a ≤ b + d`, `a ≤ b, c ≤ d
==> a + c ≤ d + b`, `a ≤ b, c ≤ d ==> c + a ≤ d + b`.
Consequently, we only provide a single
plus function, and users
must use
Arithmetic.Plus.commutative to further manipulate the
inequality.
Here are the proof-manipulation vocabulary used by this library. Many
of these terms are not standard, but we try to be consistent in this
library:
- Weaken: Increase an upper bound without changing the bounded
value
- Increment: Increase an upper bound along with the bounded
value
- Decrement: Decrease an upper bound along with the bounded
value
- Substitute: Replace a number with an equal number