\documentclass{article}
\usepackage{amssymb}

\newtheorem{proposition}{Proposition}
\newenvironment{proof}{\trivlist \item[\hskip \labelsep{\bf Proof$\,$}]}{\rlap{$\sqcap$}$\sqcup$\par}


\def\N{\mathbb{N}}
\def\R{\mathbb{R}}
\def\Rnn{\R_{\ge 0}}
\def\DIV{\mathbin{\mbox{\tt DIV}}}

\begin{document}

\title{The $\mu$-inverse for the HOL Light reals}
\author{Freek Wiedijk}
\date{}
\maketitle

\begin{abstract}\noindent
We present an alternative definition of the multiplicative inverse
for the real numbers as formalized in John Harrison's HOL Light system.
\end{abstract}

\section{Defining the real numbers}

The two common ways to define the real numbers from the rational numbers
are by means of Cauchy sequences or by means of Dedekind cuts.
Both methods for defining the real numbers have many variations.
(For instance,
lazy streams of digits are a way to code Cauchy sequences, and
Conway's way to represent numbers \cite{con:76} are a variation on
the theme of Dedekind cuts.)

\section{Nearly-multiplicative functions}

In \cite{har:98} John Harrison defined the non-negative real numbers
$\Rnn$ as equivalence classes of certain sequences $(a_n)$
called {\em nearly-multiplicative functions.}
These sequences are sequences of {\em natural numbers},%
\footnote{So the reals are defined
without first defining the rational numbers or even the integers.}
such that the sequence of rationals
$$\left({a_n\over n}\right)$$
is a Cauchy sequence with a convergence rate proportional to $1/n$.
Specifically it satisfies, for some $a\in\Rnn$ and $B\in\R_{>0}$
(which both depend on the sequence):
$$\left|{a_n\over n} - a\right|\le {B\over n}$$
or, equivalently:
$$\left|{a_n - a n}\right|\le B$$
So $(a_n)$ is a nearly-multiplicative function corresponding to the
real number $a$
if $a_n$ is, up to a bounded `error', equal to $a n$.
If one draws the graph of such a sequence, it stays within a straight `band'
of finite width.

There are two different ways to characterize these sequences
without mentioning rational or real numbers, so just in terms of
natural number arithmetic.
Those are the requirements of {\em near-multiplicativity\/}:
$$\exists B\in\N.\,\forall m,n\in\N.\,\left|n a_m - m a_n\right|\le B\left(m + n\right)$$
(which is the Cauchy-sequence property
$$\exists B\in\N.\,\forall m,n\in\N.\,\left|{a_m\over m} - {a_n\over n}\right|\le B\Big({1\over m} + {1\over n}\Big)$$
if one divides both sides by $m n$),
and of {\em near-additivity\/}:
$$\exists B'\in\N.\,\forall m,n\in\N.\,\left|a_{m+n} - (a_m + a_n)\right|\le B'$$
These two requirements are the same, as is shown in \cite{har:98}.

\section{Equivalence and embedding of the naturals}

The {\em equivalence\/} of two nearly-multiplicative sequences is defined by:
$$\begin{array}{rcl}
(a_n)\sim\left(b_n\right)
&\Leftrightarrow&
\exists C.\,\left|a_n - b_n\right|\le C
\end{array}$$
Two nearly-multiplicative sequences represent the same non-negative real
number in $\Rnn$ if and only if they are equivalent.

For each natural number $k\in\N$ there exists a nearly-multiplicative sequence
$k^*$ representing it in $\Rnn$, which is defined by
$$\left(k^*\right)_n = k n$$
In particular:
$$(0^*)_n = 0$$
and:
$$(1^*)_n = n$$

\section{Arithmethical operations}

The addition on the non-negative real numbers in terms of nearly-multiplicative
sequences is defined by:
$$(a + b)_n = a_n + b_n$$

\noindent
For multiplication there are two choices for a `natural' definition:
\begin{itemize}
\item Either one defines it by:
$$(ab)_n = a_n b_n \DIV n$$
(where $\DIV$ is division in the natural numbers.)
\item Alternatively, one can define it by:
$$(ab)_n = a_{b_n}$$
This works, because $a_{b_n}$ is close to $a(b_n)$ which is close to $a (b n)$
which is $(a b) n$.
With this definition proving that multiplication is commutative (which is
done in \cite{har:98}) becomes non-trivial.
\end{itemize}

\noindent
Analogously there are two ways to define multiplicative inverse for
nearly-multiplicative functions.
\begin{itemize}
\item
Either one defines:
$$(a^{-1})_n = {n^2} \DIV {a_n}$$
\item
Alternatively, one can define:
$$(a^{-1})_n = \mu m.\,a_m\ge n$$
(The notation $\mu m.\,P(m)$ means `the least $m\in\N$ for which $P(m)$ holds.')
So $(a^{-1})_n$ is the first position where the graph
of $a_m$ `crosses' the line of constant height $n$.
This definition has the property that:
$$\left(1^*\right)^{-1} = 1^*$$
(which is a reason to have in this definition $\ge$ instead of $>$.)
\end{itemize}

\noindent
Both these definitions need to specify what happens when the sequence
represents the real number $0$.
\begin{itemize}
\item
If the inverse is defined in the first way, the inverse of a sequence
$(a_n)\sim 0^*$ won't be a nearly-multiplicative sequence (it will grow
at least quadratically.)
In \cite{har:98} the result of the division for that case is {\em defined\/} to
be the nearly-multiplicative sequence $0^*$ representing $0$ in $\Rnn$.
\item
If the inverse is defined in the second way, we will get the expression
$\mu m.\,\bot$ (because for sufficiently large $n$, no $a_m$ will be greater than $n$.)
If we define:
$$\mu m.\,\bot = 0$$
to make the $\mu$ operator total, then this will lead to a
total multiplicative inverse, and we will automatically (so not by definition)
get:
$$\left(0^*\right)^{-1} = 0^*$$
\end{itemize}

\section{The properties of the inverse}

In \cite{har:98} the inverse is defined according to the first approach
(although multiplication is defined according to the second!),
and the second way to define the multiplicative inverse is not even mentioned.
We will now show how to prove the basic properties of the inverse
if it is defined according to the second approach. 
This theory has been formalized using the HOL Light system.%
\footnote{This formalization is on the Web at
{\tt <http://www.cs.kun.nl/\~{}freek/notes/muinv.ml>}}

We first present the HOL Light definitions of the $\mu$ operator and of the $\mu$-inverse:
\begin{quote}
\begin{verbatim}
parse_as_binder "mu";;
let mu = new_definition
  `(mu) P = (@n. P n /\ (!m. m < n ==> ~P m) \/
                 (n = 0) /\ (!m. ~P m))`;;
let muinv = new_definition
  `muinv(x) = afn(\n. mu m. fn x m >= n)`;;
\end{verbatim}
\end{quote}

\noindent
When in the rest of this note we write ${}^{-1}$ we refer to this \verb|muinv| function.
The propositions that follow show that it
is well defined and that it behaves like a multiplicative inverse.
The propositions are labelled with their name in the HOL Light formalization.

In the following, $a = (a_n)$ is a nearly-multiplicative function.

\begin{proposition}[$= \mbox{\tt MUINV\_TO\_0}$]
If $a\sim 0^*$, then there exists some $N$ such that 
$(a^{-1})_n = 0$ for all $n\ge N$.
\end{proposition}
\begin{proof}
Because $a\sim 0^*$, there is a $B$ with $a_n\le B$ for all $n\in\N$.
Take $N = B+1$, then for $n\ge N$ clearly $a_m \ge n$ can't happen and so is equivalent to $\bot$
and so $(a^{-1})_n = \mu m.\,a_m\ge n = \mu m.\,\bot = 0$.
\end{proof}

\begin{proposition}[$= \mbox{\tt MUINV\_EQ\_0}$]
If $a\sim 0^*$, then $a^{-1}\sim 0^*$.
\end{proposition}
\begin{proof}
Take $N$ as in the previous proposition.
$(a^{-1})_n$ is bounded on $n < N$
(because it only takes finitely many values there)
and is zero for $n\ge N$, so it is
bounded everywhere, and so $a^{-1}\sim 0^*$.
\end{proof}

\bigskip\noindent
This is about all there is to say about the case that $a\sim 0^*$.
So in the rest of this note, suppose that $a\not\sim 0^*$.
This means that $a_n$ can get arbitrarily big, so the $\mu$ in
the definition of ${}^{-1}$ will never be degenerated.

\begin{proposition}[$= \mbox{\tt NADD\_CLOSE}$]
\label{close}
For some $B$ we have that:
$$\begin{array}{c}
a_0\le B\\
a_n\le a_{n-1} + B
\end{array}$$
\end{proposition}
So this says that the $a_n$ can't jump up too far.
\begin{proof}
Directly from the property of near additivity.
\end{proof}

\begin{proposition}[$= \mbox{\tt MUINV\_CLOSE'}$]
\label{inv}
For some $B$:
$$n\le a_{(a^{-1})_n}\le n + B$$
\end{proposition}
\begin{proof}
Take $B$ as in the previous proposition.
Let $m = (a^{-1})_n$, and suppose that $m > 0$.
Then because $m$ is the smallest number with
$n\ge a_m$, we have:
$$a_{m-1} < n\le a_m$$
From this and the inequalities of the previous proposition the
required inequalities follow.

The case $m = 0$ is similar.
\end{proof}

\begin{proposition}[$= \mbox{\tt MUINV\_LINV}$]
The function $a^{-1}$ is the multiplicative inverse of $a$, i.e.:
$$a^{-1}\cdot a\sim a\cdot a^{-1}\sim 1^*$$
\end{proposition}
\begin{proof}
Directly from the previous proposition (because multiplication is function composition
and $\sim$ is bounded difference.)
\end{proof}

\begin{proposition}[$= \mbox{\tt MUINV\_UBOUND\_ALL}$]
The function
$(a^{-1})_n$ is bounded by a linear function, so there exists a $B$ such that:
$$(a^{-1})_n\le Bn$$
\end{proposition}
\begin{proof}
It is enough to show that $(a^{-1})_n$ will be bounded for
sufficiently large $n$.
This follows using proposition \ref{close} and the fact that
$a_n$ is bounded from below, which means that there is an $A$ such that:
$$n\le A a_n$$
(It can be shown that $B = 2A$ is a sufficient estimate.)
\end{proof}

\begin{proposition}[$= \mbox{\tt MUINV\_NADD}$]
The function $(a^{-1})_n$ is a nearly-multiplicative function.
\end{proposition}
\begin{proof}
From proposition \ref{inv} follows that the difference between
$|n (a^{-1})_m - m (a^{-1})_n|$ and
$|a_{(a^{-1})_n} (a^{-1})_m - a_{(a^{-1})_m} (a^{-1})_n|$ is bounded
by a multiple of $|(a^{-1})_m + (a^{-1})_n|$.
Furthermore because $a$ is a nearly-multiplicative function,
$|a_{(a^{-1})_n} (a^{-1})_m - a_{(a^{-1})_m} (a^{-1})_n|$
is also bounded by a multiple of
$|(a^{-1})_m + (a^{-1})_n|$.
Together this gives that $|n (a^{-1})_m - m (a^{-1})_n|$
is bounded by a multiple of $|(a^{-1})_m + (a^{-1})_n|$.
But then by the previous proposition it is bounded by a multiple of $|m + n|$.
\end{proof}

\section{Relevance}

We presented an alternative way to define the multiplicative inverse for
the real numbers in John Harrison's HOL Light system.
Although this alternative definition is elegant and corresponds more closely to the multiplication
of the system than the current definition of inverse,
its theory is not substantially simpler.
Also because once the key properties of inverse
have been proved no use is made of its definition, it really doesn't matter
which definition one uses.

%\bibliographystyle{plain}
%\bibliography{muinv}

\begin{thebibliography}{1}

\bibitem{con:76}
J.H. Conway.
\newblock {\em On Numbers and Games}.
\newblock Academic Press, New York, 1976.

\bibitem{har:98}
J.R. Harrison.
\newblock {\em Theorem Proving with the Real Numbers}.
\newblock Springer-Verlag, Berlin, Heidelberg, New York, 1998.

\end{thebibliography}

\end{document}