1 The natural numbers
Everything starts with the natural numbers. Since lean already has a type of natural numbers, we define our own copy, called \(\mathrm{MyNat}\), from scratch. To make sure we do not secretly use results that are already in mathlib, the file defining \(\mathrm{MyNat}\) does not import any mathematics.
1.1 Definition
We define \(\mathrm{MyNat}\) as the inductive type with two constructors:
a term \(0\) (called zero);
for every \(n \in \mathrm{MyNat}\), a term \(\mathrm{succ}(n)\) (the successor of \(n\)).
In other words, every natural number is obtained from \(0\) by applying the successor function a finite number of times. We write \(1\) for \(\mathrm{succ}(0)\).
We define addition on \(\mathrm{MyNat}\) by recursion on the second argument:
We define multiplication on \(\mathrm{MyNat}\) by recursion on the second argument:
1.2 Commutative semiring structure
All the lemmas of this section are proved by induction, using the recursive definitions of addition and multiplication. Note that \(a + 0 = a\) and \(a * 0 = 0\) hold by definition, while the symmetric statements \(0 + a = a\) and \(0 * a = 0\) need a proof.
For all \(a\) in \(\mathrm{MyNat}\) we have \(0 + a = a\).
By induction on \(a\).
Addition on \(\mathrm{MyNat}\) is associative.
By induction on the last variable.
Addition on \(\mathrm{MyNat}\) is commutative.
By induction.
For all \(a\), \(b\) and \(c\) in \(\mathrm{MyNat}\) we have \(a * (b + c) = a * b + a * c\).
By induction on \(c\).
For all \(a\), \(b\) and \(c\) in \(\mathrm{MyNat}\) we have \((a + b) * c = a * c + b * c\).
By induction on \(c\).
Multiplication on \(\mathrm{MyNat}\) is associative.
By induction, using left distributivity.
Multiplication on \(\mathrm{MyNat}\) is commutative.
By induction.
For all \(a\) in \(\mathrm{MyNat}\) we have \(1 * a = a\).
By induction, recalling that \(1 = \mathrm{succ}(0)\).
\(\mathrm{MyNat}\) with addition and multiplication is a commutative semiring.
We collect all the lemmas above: addition is associative and commutative with neutral element \(0\), multiplication is associative and commutative with neutral element \(1\), multiplication distributes over addition and \(0\) is absorbing for multiplication.
In \(\mathrm{MyNat}\) we have \(0 \neq 1\).
The constructors \(\mathrm{zero}\) and \(\mathrm{succ}\) are distinct, and \(1 = \mathrm{succ}(0)\).
Let \(a\) and \(b\) in \(\mathrm{MyNat}\) be such that \(a \neq 0\) and \(b \neq 0\). Then \(a * b \neq 0\).
If \(a \neq 0\) and \(b \neq 0\) we can write \(a = \mathrm{succ}(a')\) and \(b = \mathrm{succ}(b')\), and then \(a * b = \mathrm{succ}(a' * b' + a' + b')\) is a successor, hence nonzero.
1.3 The order
Let \(a\) and \(b\) in \(\mathrm{MyNat}\). We write \(a \leq b\) if there exists a natural number \(x\) such that
The relation \(\leq \) on \(\mathrm{MyNat}\) is reflexive.
We can take \(x = 0\).
The relation \(\leq \) on \(\mathrm{MyNat}\) is transitive.
If \(b = a + x\) and \(c = b + y\) then \(c = a + (x + y)\).
The relation \(\leq \) on \(\mathrm{MyNat}\) is antisymmetric.
If \(b = a + x\) and \(a = b + y\) then \(a = a + (x + y)\), so \(x + y = 0\) and hence \(x = y = 0\), giving \(a = b\).
The order \(\leq \) on \(\mathrm{MyNat}\) is total.
By induction one shows that for all \(a\) and \(b\) either \(a \leq b\) or \(b \leq a\).
We have that \(\mathrm{MyNat}\) with \(\leq \) is a linear order.
Clear from the lemmas above.
1.4 Interaction between the order and the algebraic structure
Let \(a\), \(b\) and \(c\) in \(\mathrm{MyNat}\) be such that \(a \leq b\). Then \(a + c \leq b + c\).
Let \(x\) be such that \(b = a + x\). The same \(x\) shows that \(a + c \leq b + c\).
Let \(a\), \(b\) and \(c\) in \(\mathrm{MyNat}\) be such that \(0 {\lt} c\) and \(a {\lt} b\). Then \(c * a {\lt} c * b\).
Write \(b = a + x\) with \(x \neq 0\). Then \(c * b = c * a + c * x\) with \(c * x \neq 0\), so \(c * a {\lt} c * b\).
Let \(a\), \(b\) and \(c\) in \(\mathrm{MyNat}\) be such that \(0 {\lt} c\) and \(a {\lt} b\). Then \(a * c {\lt} b * c\).
Identical to the previous lemma using commutativity of multiplication.