#Contents# * table of contents {:toc} ## Idea ## The decimal numbers as familiar from school mathematics. ## Definition ## The type of **decimal numbers**, denoted $\mathbb{Z}[1/10]$, is defined as the [[higher inductive type]] generated by: * A function $(-)/10^{(-)}:\mathbb{Z} \times \mathbb{N} \rightarrow \mathbb{Z}[1/10]$. The integer $a:\mathbb{Z}$ represents the integer if one ignores the decimal separator in the decimal numeral representation of the decimal number, and the natural number $b:\mathbb{N}$ represents the number of digits to the left of the final digit where the decimal separator ought to be placed after in the decimal numeral representation of the decimal number. * A dependent product of functions between identities representing that equivalent decimals are equal: $$equivdec : \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{N}} \prod_{c:\mathbb{Z}} \prod_{d:\mathbb{N}} (a \cdot 10^d = c \cdot 10^b) \to (a/10^b = c/10^d)$$ (i.e. 1.00 = 1.000 with decimal numeral representations) * A set-truncator $$\tau_0: \prod_{a:\mathbb{Z}[1/10]} \prod_{b:\mathbb{Z}[1/10]} isProp(a=b)$$ ## Mathematical structures on the decimal numbers ## ### Ring structure on the decimal numbers ### #### Zero #### We define *zero* $0:\mathbb{Z}[1/10]$ to be the following: $$0 \coloneqq 0/10^0$$ #### Addition #### We define *addition* $(-)+(-):\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ to be the following: $$a/10^b + c/10^d \coloneqq (a \cdot 10^d + c \cdot 10^b)/10^{(b + d)}$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$. #### Negation #### We define *negation* $-(-):\mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ to be the following: $$-(a/10^b) \coloneqq (-a)/10^b$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$. #### Subtraction #### We define *subtraction* $(-)-(-):\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ to be the following: $$a/10^b - c/10^d \coloneqq (a \cdot 10^d - c \cdot 10^b)/10^{(b + d)}$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$. #### One #### We define *one* $1:\mathbb{Z}[1/10]$ to be the following: $$1 \coloneqq 1/10^0$$ #### Multiplication #### We define *multiplication* $(-)\cdot(-):\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ to be the following: $$a/10^b \cdot c/10^d \coloneqq (a \cdot c)/10^{(b + d)}$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$. #### Exponentiation #### We define *exponentiation* $(-)^{(-)}:\mathbb{Z}[1/10] \times \mathbb{N} \to \mathbb{Z}[1/10]$ to be the following: $$(a/10^b)^n \coloneqq (a^n)/10^{(b \cdot n)}$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, $n:\mathbb{N}$. ### Sign ### #### Positive sign #### We define the dependent type *is positive*, denoted as $isPositive(a/10^b)$, to be the following: $$isPositive(a/10^b) \coloneqq a \gt 0$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, dependent types $m\gt n$ indexed by $m, n:\mathbb{Z}$. #### Negative sign #### We define the dependent type *is negative*, denoted as $isNegative(a/10^b)$, to be the following: $$isNegative(a/10^b) \coloneqq \Vert a \lt 0$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, dependent types $m\gt n$ indexed by $m, n:\mathbb{Z}$. #### Zero sign #### We define the dependent type *is zero*, denoted as $isZero(a/10^b)$, to be the following: $$isZero(a/10^b) \coloneqq a = 0$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$. #### Non-positive sign #### We define the dependent type *is non-positive*, denoted as $isNonPositive(a/10^b)$, to be the following: $$isNonPositive(a/10^b) \coloneqq isPositive(a/10^b) \to \emptyset$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$. #### Non-negative sign #### We define the dependent type *is non-negative*, denoted as $isNonNegative(a/10^b)$, to be the following: $$isNonNegative(a/10^b) \coloneqq isNegative(a/10^b) \to \emptyset$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$. #### Non-zero sign #### We define the dependent type *is non-zero*, denoted as $isNonZero(a/10^b)$, to be the following: $$isNonNegative(a/10^b) \coloneqq \Vert isPositive(a/10^b) + isNegative(a/10^b) \Vert$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$. ### Order structure on the decimal numbers ### #### Less than #### We define the dependent type *is less than*, denoted as $a/10^b \lt c/10^d$, to be the following: $a/10^b \lt c/10^d \coloneqq isPositive(c/10^d - a/10^b)$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$. #### Greater than #### We define the dependent type *is greater than*, denoted as $a/10^b \gt c/10^d$, to be the following: $a/10^b \gt c/10^d \coloneqq isNegative(c/10^d - a/10^b)$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$. #### Apart from #### We define the dependent type *is apart from*, denoted as $a/10^b # c/10^d$, to be the following: $a/10^b # c/10^d \coloneqq isNonZero(c/10^d - a/10^b)$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$. #### Less than or equal to #### We define the dependent type *is less than or equal to*, denoted as $a/10^b \leq c/10^d$, to be the following: $a/10^b \lt c/10^d \coloneqq isNonNegative(c/10^d - a/10^b)$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$. #### Greater than or equal to #### We define the dependent type *is greater than or equal to*, denoted as $a/10^b \geq c/10^d$, to be the following: $a/10^b \geq c/10^d \coloneqq isNonPositive(c/10^d - a/10^b)$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$. ### Pseudolattice structure on the decimal numbers ### #### Ramp #### We define the *ramp function* $ramp:\mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ to be the following: $$ramp(a/10^b) \coloneqq ramp(a)/10^b$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, $ramp:\mathbb{Z} \to \mathbb{Z}$. #### Minimum #### We define the *minimum* $min:\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ to be the following: $$min(a/10^b,c/10^d) \coloneqq a/10^b - ramp(a/10^b - c/10^d)$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$. #### Maximum #### We define the *maximum* $max:\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ to be the following: $$max(a/10^b,c/10^d) \coloneqq a/10^b + ramp(c/10^d - a/10^b)$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$. #### Absolute value #### We define the *absolute value* $\vert(-)\vert:\mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ to be the following: $$\vert a/10^b \vert \coloneqq max(a/10^b, -a/10^b)$$ for $a:\mathbb{Z}$, $b:\mathbb{N}$. ## Properties ## TODO: Show that the decimal numbers are a ordered Heyting integral domain with decidable equality, decidable apartness, and decidable linear order, and that the decimal numbers are a Heyting integral subdomain of the rational numbers. 10 is a unit term. Thus this is true: $$sci : \prod_{a:\mathbb{Z}[1/10]} (0 \lt a) \times \sum_{b:\mathbb{Z}} (1 \leq a \cdot 10^b) \times (a \cdot 10^b \lt 10)$$ this forms the basis of scientific notation. ## See also ## * [[higher inductive type]] * [[natural numbers]] * [[integers]] * [[rational numbers]] * [[real numbers]]