$\newcommand{\cardinal}[1]{\abs{#1}}$ $\newcommand{\cardinal}[1]{\abs{#1}}$ $\newcommand{\ceil}[1]{\left\lceil #1 \right\rceil}$ $\newcommand{\floor}[1]{\left\lfloor #1 \right\rfloor}$ $\DeclareMathOperator*{\argmin}{arg\,min}$ $\newcommand{\abs}[1]{\left\lvert #1 \right\rvert}$ $\newcommand{\domain}[1]{\operatorname{dom}\left(#1\right)}$ $\newcommand{\range}[1]{\operatorname{range}\left(#1\right)}$
I am trying to prove some classic algorithms in computer science, e.g., binary search for first occurrence of an element in a sorted array. Here is my formalization of the problem:
Let $a$ be a non-decreasing sequence such that $\domain{a} = \mathbb{Z}^{+}$, $\range{a} \subseteq \mathbb{Z}$ and $x \in \mathbb{Z}$.
Let $f$ be a function such that $\domain{f} = \mathbb{Z}^{+} \times \left(\left\{-1\right\} \cup \mathbb{Z}^{+}\right)$ and $\range{f} \subseteq \mathbb{Z}$. Further, for any $l \in \mathbb{Z}^{+}$ and $h \in \left\{-1\right\} \cup \mathbb{Z}^{+}$,
if $l > h$, then $f\left(l, h\right) = -1$;
if $l \leq h$, (the first two points indicate that $\floor{\frac{l + h}{2}}$ is the element sought, and the third point indicate that $\floor{\frac{l + h}{2}}$ is not the element sought),
if $a\left(\floor{\frac{l + h}{2}}\right) = x$ and $\floor{\frac{l + h}{2}} = l$, then $f\left(l, h\right) = \floor{\frac{l + h}{2}}$;
if $a\left(\floor{\frac{l + h}{2}}\right) = x$ and $\floor{\frac{l + h}{2}} > l$ and $a\left(\floor{\frac{l + h}{2}} - 1\right) \neq x$, then $f\left(l, h\right) = \floor{\frac{l + h}{2}}$. \item if the above two conditions are not met, then
if $x > a\left(\floor{\frac{l + h}{2}}\right)$, $f\left(l, h\right) = f\left(\floor{\frac{l + h}{2}} + 1, h\right)$; \item if $x \leq a\left(\floor{\frac{l + h}{2}}\right)$, $f\left(l, h\right) = f\left(l, \floor{\frac{l + h}{2}} - 1\right)$.
For any $l, h \in \mathbb{Z}^{+}$ such that $l \leq h$, \begin{equation*} f\left(l, h\right) = \begin{cases} \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}},\ \textrm{there is some } s\ \textrm{such that } l \leq s \leq h \textrm{ and } a\left(s\right) = x,\\ -1,\ \textrm{there is no } s\ \textrm{such that } l \leq s \leq h \textrm{ and } a\left(s\right) = x. \end{cases} \end{equation*}
The following is my proof:
Let $P$ be the predicate that for any $n \in \mathbb{N}$, $P\left(n\right)$ if and only if for any $l, h$, if $h - l = n$, then \begin{equation*} f\left(l, h\right) = \begin{cases} \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}},\ \textrm{there is some } s\ \textrm{such that } l \leq s \leq h \textrm{ and } a\left(s\right) = x\\ -1,\ \textrm{there is no } s\ \textrm{such that } l \leq s \leq h \textrm{ and } a\left(s\right) = x \end{cases} \end{equation*} We use mathematical induction to prove that for any $n \in \mathbb{N}$, $P\left(n\right)$.
First we prove $P\left(0\right)$. In this case, $l = h$. Accordingly, \begin{equation*} \floor{\frac{l + h}{2}} = l. \end{equation*} First we assume that there is some $s$ such that $l \leq s \leq h$ and $a\left(s\right) = x$. In this case, it is clear that $a\left(l\right) = a\left(h\right) = x$. Back to definition of $f$, indeed, we have $l \leq h$. As \begin{equation*} \frac{l + h}{2} = \frac{l + l}{2} = l \end{equation*} and \begin{equation*} \frac{l + h}{2} = \frac{h + h}{2} = h, \end{equation*} \begin{equation*} a\left(\floor{\frac{l + h}{2}}\right) = a\left(l\right) = x. \end{equation*} By definition, we have $f\left(l, h\right) = \floor{\frac{l + h}{2}}$. Indeed, \begin{equation*} \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}} = \floor{\frac{l + h}{2}}. \end{equation*} As a result, we have $f\left(l, h\right) = \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}}$.
Next we assume that there is no $s$ such that $l \leq s \leq h$ and $a\left(s\right) = x$. In this case, \begin{equation*} f\left(l, h\right) = \begin{cases} f\left(l + 1, l\right) = -1,\ x > a\left(l\right)\\ f\left(l, l - 1\right) = -1,\ x \leq a\left(l\right). \end{cases} \end{equation*} We conclude that that in this case, $f\left(l, h\right) = -1$.
Consequently, $P\left(0\right)$ holds. Next, assume $n \in \mathbb{N}$ and for any $m$, if $m \leq n$, $P\left(m\right)$ holds. We wish to prove $P\left(n + 1\right)$. Let $l, h \in \mathbb{Z}$ such that $h - l = n + 1$. It is clear that $l < h$. Again, we divide our discussion into the following two major categories:
there is some $s$ such that $l \leq s \leq h$ and that $a\left(s\right) = x$;
there is no $s$ such that $l \leq s \leq h$ and that $a\left(s\right) = x$.
First, assume that there is some $s$ such that $l \leq s \leq h$ and that $a\left(s\right) = x$. Under this assumption, first assume that $a\left(\floor{\frac{l + h}{2}}\right) = x$ and $\floor{\frac{l + h}{2}} = l$. As $l < h$, we have $h = l + 1$. By definition, we have \begin{equation*} f\left(l, h\right) = l. \end{equation*} On the other hand, indeed, \begin{equation*} \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}} = l. \end{equation*} Thus, in this case, $f\left(l, h\right) = \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}}$. Next, assume that $a\left(\floor{\frac{l + h}{2}}\right) = x$ and $\floor{\frac{l + h}{2}} > l$ and $a\left(\floor{\frac{l + h}{2}} - 1\right) \neq x$. By definition, we have $f\left(l, h\right) = \floor{\frac{l + h}{2}}$. On the other hand, as $a$ is sorted, $a\left(\floor{\frac{l + h}{2}}\right) = x$ and $a\left(\floor{\frac{l + h}{2}} - 1\right) \neq x$, it is clear that \begin{equation*} \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}} = \floor{\frac{l + h}{2}}. \end{equation*} Thus, we have \begin{equation*} f\left(l, h\right) = \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}}. \end{equation*} Next, assume that the two conditions do not hold. We consider $x > a\left(\floor{\frac{l + h}{2}}\right)$ and $x \leq a\left(\frac{l + h}{2}\right)$. In the first case, we have \begin{equation*} f\left(l, h\right) = f\left(\floor{\frac{l + h}{2}} + 1, h\right). \end{equation*} It is clear that \begin{equation*} h - \left(\floor{\frac{l + h}{2}} + 1\right) \leq n. \end{equation*} By induction hypothesis, \begin{equation*} f\left(\floor{\frac{l + h}{2}} + 1, h\right) = \min\left\{s \vert \floor{\frac{l + h}{2}} + 1 \leq s \leq h \wedge a\left(s\right) = x\right\}. \end{equation*} On the other hand, as \begin{equation*} \floor{\frac{l + h}{2}} \neq \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}} \end{equation*} and \begin{equation*} x > a\left(\frac{l + h}{2}\right), \end{equation*} \begin{equation*} \floor{\frac{l + h}{2}} + 1 \leq \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}} \leq h. \end{equation*} Thus, \begin{equation*} \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}} = \min\left\{s \vert \floor{\frac{l + h}{2}} + 1 \leq s \leq h \wedge a\left(s\right) = x\right\}. \end{equation*} Consequently, in this case, \begin{equation*} f\left(l, h\right) = \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}}. \end{equation*} Next, assume that $x \leq a\left(\floor{\frac{l + h}{2}}\right)$. By definition, we have \begin{equation*} f\left(l, h\right) = f\left(l, \floor{\frac{l + h}{2}} - 1\right). \end{equation*} It is clear that \begin{equation*} \floor{\frac{l + h}{2}} - 1 - l \leq n. \end{equation*} Using induction hypothesis, we have \begin{equation*} f\left(l, \floor{\frac{l + h}{2}} - 1\right) = \min\left\{s \vert l \leq s \leq \floor{\frac{l + h}{2}} - 1 \wedge a\left(s\right) = x\right\}. \end{equation*} On the other hand, as \begin{equation*} \floor{\frac{l + h}{2}} \neq \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}} \end{equation*} and \begin{equation*} x \leq a\left(\floor{\frac{l + h}{2}}\right), \end{equation*} we have \begin{equation*} \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}} = \min\left\{s \vert l \leq s \leq \floor{\frac{l + h}{2}} - 1 \wedge a\left(s\right) = x\right\}. \end{equation*} Consequently, in this case, \begin{equation*} f\left(l, h\right) = \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}}. \end{equation*}
We conclude that if there is some $s$ such that $l \leq s \leq h$ and that $a\left(s\right) = x$ and $h - l = n + 1$, then \begin{equation*} f\left(l, h\right) = \min{\left\{s \vert l \leq s \leq h \wedge a\left(s\right) = x\right\}}. \end{equation*} Next, we assume there is no $s$ such that $l \leq s \leq h$ and that $a\left(s\right) = x$ and $h - l = n + 1$.
Under this assumption, by rule of contradiction, it is immediately clear that the first two conditions under $l \leq h$ cannot be met. We first assume that $x > a\left(\floor{\frac{l + h}{2}}\right)$. By definition, \begin{equation*} f\left(l, h\right) = f\left(l, \floor{\frac{l + h}{2}} - 1\right). \end{equation*} As there is no $s$ such that $l \leq s \leq h$ and $a\left(s\right) = x$, there is no $s$ such that $l \leq s \leq \floor{\frac{l + h}{2}}$ and $a\left(s\right) = x$. As \begin{equation*} \floor{\frac{l + h}{2}} - 1 - l \leq n, \end{equation*} by induction hypothesis, \begin{equation*} f\left(l, \floor{\frac{l + h}{2}} - 1\right) = -1. \end{equation*} Then indeed we have \begin{equation*} f\left(l, h\right) = -1. \end{equation*} Next, assume $x \leq a\left(\floor{\frac{l + h}{2}}\right)$. In this case, by definition, we have \begin{equation*} f\left(l, h\right) = f\left(l, \floor{\frac{l + h}{2}} - 1\right). \end{equation*} Again, it is clear that \begin{equation*} \floor{\frac{l + h}{2}} - 1 - l \leq n. \end{equation*} As there is no $s$ such that $l \leq s \leq h$ and $a\left(s\right) = x$, there is no $s$ such that $l \leq s \leq \floor{\frac{l + h}{2}} - 1$ and $a\left(s\right) = x$. Thus, by induction hypothesis, \begin{equation*} f\left(l, \floor{\frac{l + h}{2}} - 1\right) = -1. \end{equation*} Thus, \begin{equation*} f\left(l, h\right) = -1. \end{equation*}
We conclude that if there is no $s$ such that $l \leq s \leq h$ and $a\left(s\right) = x$, $f\left(l, h\right) = -1$.
Finally, we conclude that $P\left(0\right)$ and $P\left(n\right)$ leads to $P\left(n + 1\right)$. As a result, for any $n \in \mathbb{N}$, $P\left(n\right)$.
I would like verify this proof using mathematical induction on proof of an algorithm in compute science.