Contents

# Contents

## Idea

The decimal numeral representation of the natural numbers as strings of digits as familiar from school mathematics, with mathematical operations directly defined on the strings of digits.

## Definition

### In type theory

Let $D$ be the type of decimal digits, inductively generated by the terms $0:D$, $1:D$, $2:D$, $3:D$, $4:D$, $5:D$, $6:D$, $7:D$, $8:D$, and $9:D$. The decimal numeral representation of the natural numbers $\mathrm{Dec}$ is defined as the higher inductive type generated by the function

$(-):D \to \mathrm{Dec}$

the binary operation

$(-)(-):\mathrm{Dec} \times \mathrm{Dec} \to \mathrm{Dec}$
$p:\prod_{a:\mathrm{Dec}} \prod_{b:\mathrm{Dec}} \prod_{c:\mathrm{Dec}} (a b) c = a (b c)$

and the dependent function

$q:\prod_{a:\mathrm{Dec}} a = 0 a$

In Coq-syntax the decimal digits and the decimal representation of the natural numbers are the (higher) inductive types defined by

Inductive DecDigits : Type :=
| zero : DecDigits
| one : DecDigits
| two : DecDigits
| three : DecDigits
| four : DecDigits
| five : DecDigits
| six : DecDigits
| seven : DecDigits
| eight : DecDigits
| nine : DecDigits

Inductive Dec : Type :=
| digit : DecDigits -> Dec
| cat : Dec -> Dec -> Dec
| assoc : forall (a,b,c : DecDigits) cat cat a b c == cat a cat b c
| lead-zero : forall (a : Dec) a == cat digit zero a

### As a quotient set

Let

$\mathbb{10} \coloneqq \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1} \uplus \mathbb{1}$

be the disjoint union of 10 singletons, with an element $0 \in \mathbb{10}$ and let $\mathbb{10}^+$ be the free semigroup on $\mathbb{10}$. Then the set of decimal numeral representations of the natural numbers is the quotient set $\mathbb{10}^+/(a = 0 a)$.

## Properties

### Zero and successor

The decimal numeral representation of the natural numbers is a natural numbers object in Set: We define $0:\mathrm{Dec}$ to be $0$, and we inductively define the successor function $s:\mathrm{Dec} \to \mathrm{Dec}$ as

$s(a 0) \coloneqq a 1$
$s(a 1) \coloneqq a 2$
$s(a 2) \coloneqq a 3$
$s(a 3) \coloneqq a 4$
$s(a 4) \coloneqq a 5$
$s(a 5) \coloneqq a 6$
$s(a 6) \coloneqq a 7$
$s(a 7) \coloneqq a 8$
$s(a 8) \coloneqq a 9$
$s(a 9) \coloneqq s(a) 0$

### Inequalities

The denial inequality tight apartness relation $\neq$ called not equal to is inductively defined for decimal numeral representations of the natural numbers in the same way that it is inductively defined for natural numbers:

$0 \neq 0 \coloneqq \mathbb{0}$
$0 \neq s(n) \coloneqq \mathbb{1}$
$s(m) \neq 0 \coloneqq \mathbb{1}$
$s(m) \neq s(n) \coloneqq m \neq n$

The total order relation $\leq$ called less than or equal to is inductively defined for decimal numeral representations of the natural numbers in the same way that it is inductively defined for natural numbers:

$0 \leq 0 \coloneqq \mathbb{1}$
$0 \leq s(n) \coloneqq \mathbb{1}$
$s(m) \leq 0 \coloneqq \mathbb{0}$
$s(m) \leq s(n) \coloneqq m \leq n$

The opposite total order $\geq$ called greater than or equal to is inductively defined as

$0 \geq 0 \coloneqq \mathbb{1}$
$0 \geq s(n) \coloneqq \mathbb{0}$
$s(m) \geq 0 \coloneqq \mathbb{1}$
$s(m) \geq s(n) \coloneqq m \geq n$

The strict linear order relation $\lt$ called less than is inductively defined for decimal numeral representations of the natural numbers in the same way that it is inductively defined for natural numbers:

$0 \lt 0 \coloneqq \mathbb{0}$
$0 \lt s(n) \coloneqq \mathbb{1}$
$s(m) \lt 0 \coloneqq \mathbb{0}$
$s(m) \lt s(n) \coloneqq m \lt n$

The opposite strict linear order $\gt$ called greater than is inductively defined as

$0 \gt 0 \coloneqq \mathbb{0}$
$0 \gt s(n) \coloneqq \mathbb{0}$
$s(m) \gt 0 \coloneqq \mathbb{1}$
$s(m) \gt s(n) \coloneqq m \gt n$

### Number of digits

Each decimal numeral representation has an associated number of digits, a function $\mathrm{numDigits}:\mathrm{Dec} \to \mathrm{Dec}$ inductively defined as

$\mathrm{numDigits}(0) \coloneqq 0$
$\mathrm{numDigits}(1) \coloneqq 1$
$\mathrm{numDigits}(2) \coloneqq 1$
$\mathrm{numDigits}(3) \coloneqq 1$
$\mathrm{numDigits}(4) \coloneqq 1$
$\mathrm{numDigits}(5) \coloneqq 1$
$\mathrm{numDigits}(6) \coloneqq 1$
$\mathrm{numDigits}(7) \coloneqq 1$
$\mathrm{numDigits}(8) \coloneqq 1$
$\mathrm{numDigits}(9) \coloneqq 1$

and for every decimal numeral representation $a \neq 0$,

$\mathrm{numDigits}(a 0) \coloneqq s(\mathrm{numDigits}(a))$
$\mathrm{numDigits}(a 1) \coloneqq s(\mathrm{numDigits}(a))$
$\mathrm{numDigits}(a 2) \coloneqq s(\mathrm{numDigits}(a))$
$\mathrm{numDigits}(a 3) \coloneqq s(\mathrm{numDigits}(a))$
$\mathrm{numDigits}(a 4) \coloneqq s(\mathrm{numDigits}(a))$
$\mathrm{numDigits}(a 5) \coloneqq s(\mathrm{numDigits}(a))$
$\mathrm{numDigits}(a 6) \coloneqq s(\mathrm{numDigits}(a))$
$\mathrm{numDigits}(a 7) \coloneqq s(\mathrm{numDigits}(a))$
$\mathrm{numDigits}(a 8) \coloneqq s(\mathrm{numDigits}(a))$
$\mathrm{numDigits}(a 9) \coloneqq s(\mathrm{numDigits}(a))$

We define the type of decimal numeral representations with $n$-digits as the fiber of $\mathrm{numDigits}$ at $n$:

$representationsWithNumDigits(n) \coloneqq \sum_{a:\mathrm{Dec}} \mathrm{numDigits}(a) = n$

Addition $(-)+(-):D \times D \to \mathrm{Dec}$ of two digits is inductively defined as

+0123456789
0$0 + 0 \coloneqq 0$$0 + 1 \coloneqq 1$$0 + 2 \coloneqq 2$$0 + 3 \coloneqq 3$$0 + 4 \coloneqq 4$$0 + 5 \coloneqq 5$$0 + 6 \coloneqq 6$$0 + 7 \coloneqq 7$$0 + 8 \coloneqq 8$$0 + 9 \coloneqq 9$
1$1 + 0 \coloneqq 1$$1 + 1 \coloneqq 2$$1 + 2 \coloneqq 3$$1 + 3 \coloneqq 4$$1 + 4 \coloneqq 5$$1 + 5 \coloneqq 6$$1 + 6 \coloneqq 7$$1 + 7 \coloneqq 8$$1 + 8 \coloneqq 9$$1 + 9 \coloneqq 10$
2$2 + 0 \coloneqq 2$$2 + 1 \coloneqq 3$$2 + 2 \coloneqq 4$$2 + 3 \coloneqq 5$$2 + 4 \coloneqq 6$$2 + 5 \coloneqq 7$$2 + 6 \coloneqq 8$$2 + 7 \coloneqq 9$$2 + 8 \coloneqq 10$$2 + 9 \coloneqq 11$
3$3 + 0 \coloneqq 3$$3 + 1 \coloneqq 4$$3 + 2 \coloneqq 5$$3 + 3 \coloneqq 6$$3 + 4 \coloneqq 7$$3 + 5 \coloneqq 8$$3 + 6 \coloneqq 9$$3 + 7 \coloneqq 10$$3 + 8 \coloneqq 11$$3 + 9 \coloneqq 12$
4$4 + 0 \coloneqq 4$$4 + 1 \coloneqq 5$$4 + 2 \coloneqq 6$$4 + 3 \coloneqq 7$$4 + 4 \coloneqq 8$$4 + 5 \coloneqq 9$$4 + 6 \coloneqq 10$$4 + 7 \coloneqq 11$$4 + 8 \coloneqq 12$$4 + 9 \coloneqq 13$
5$5 + 0 \coloneqq 5$$5 + 1 \coloneqq 6$$5 + 2 \coloneqq 7$$5 + 3 \coloneqq 8$$5 + 4 \coloneqq 9$$5 + 5 \coloneqq 10$$5 + 6 \coloneqq 11$$5 + 7 \coloneqq 12$$5 + 8 \coloneqq 13$$5 + 9 \coloneqq 14$
6$6 + 0 \coloneqq 6$$6 + 1 \coloneqq 7$$6 + 2 \coloneqq 8$$6 + 3 \coloneqq 9$$6 + 4 \coloneqq 10$$6 + 5 \coloneqq 11$$6 + 6 \coloneqq 12$$6 + 7 \coloneqq 13$$6 + 8 \coloneqq 14$$6 + 9 \coloneqq 15$
7$7 + 0 \coloneqq 7$$7 + 1 \coloneqq 8$$7 + 2 \coloneqq 9$$7 + 3 \coloneqq 10$$7 + 4 \coloneqq 11$$7 + 5 \coloneqq 12$$7 + 6 \coloneqq 13$$7 + 7 \coloneqq 14$$7 + 8 \coloneqq 15$$7 + 9 \coloneqq 16$
8$8 + 0 \coloneqq 8$$8 + 1 \coloneqq 9$$8 + 2 \coloneqq 10$$8 + 3 \coloneqq 11$$8 + 4 \coloneqq 12$$8 + 5 \coloneqq 13$$8 + 6 \coloneqq 14$$8 + 7 \coloneqq 15$$8 + 8 \coloneqq 16$$8 + 9 \coloneqq 17$
9$9 + 0 \coloneqq 9$$9 + 1 \coloneqq 10$$9 + 2 \coloneqq 11$$9 + 3 \coloneqq 12$$9 + 4 \coloneqq 13$$9 + 5 \coloneqq 14$$9 + 6 \coloneqq 15$$9 + 7 \coloneqq 16$$9 + 8 \coloneqq 17$$9 + 9 \coloneqq 18$

### Arithmetic left shifts

There is a binary operation $(-) \ll (-):\mathrm{Dec} \times \mathrm{Dec} \to \mathrm{Dec}$ called the arithmetic left shift inductively defined as

$a \ll 0 \coloneqq a$
$a \ll s(b) \coloneqq (a \ll b) 0$

This binary operation is also called multiplication by a power of ten.

Arithmetic left shifts of digits is left distributive over addition: given $a:D$, $b:D$, and $c:\mathrm{Dec}$, $a \ll c + b \ll c = (a + b) \ll c$.

### Digit decompositions

Given a decimal numeral representation $b$, there exists functions $\mathrm{digitsNotLast}:\mathrm{Dec} \to \mathrm{Dec}$ and $\mathrm{lastDigit}:\mathrm{Dec} \to D$ such that

$b = \mathrm{digitsNotLast}(b) \mathrm{lastDigit}(b)$

and

$\mathrm{numDigits}(b) = s(\mathrm{digitsNotLast}(b))$

### Addition of general decimal representations

Given a decimal numeral representation $b$ such that $\mathrm{lastDigit}(b) = 0$, the sum of $b$ and a digit $d$ is defined as

$b + d \coloneqq \mathrm{digitsNotLast}(b) d$

Given two decimal numeral representations of the natural numbers $a_0 d_0$ and $a_1 d_1$ with $d_0$ and $d_1$ being digits and $a_0$ and $a_1$ being decimal numeral representations, addition is inductively defined as

$a_0 d_0 + a_1 d_1 \coloneqq (a_0 + a_1) 0 + (d_0 + d_1)$

The decimal numeral representation of the natural numbers is a commutative monoid object in Set:

$0 + a d = 0 + a 0 + d = a 0 + d = a d$
$a d + 0 = a 0 + d + 0 = a 0 + d = a d$