Let $n$ be a positive integer and $f \colon \{1,\dots,n\} \to \mathbb{R}$ be a decreasing function with $f(1) \ge 1$. We are interested in finding the largest number $k\in \{1,\dots,n\}$ such that $f(k) \ge 1$.
It is not possible to analytically find the largest $k$ by solving the inequality $f(k) \ge 1$. I realized that we can use Binary Search Algorithm to find $k$. It is a good option because the number of operations required to find $k$ in the worst case is bounded by $\mathcal{O}(\log n)$. Here is how I write a binary search algorithm for this problem: \begin{align} &l \gets 1\\ &u \gets n\\ &\texttt{while }\ \ l \le u\\ & \ \ \ \ \ \ \ \ \ \ m \gets \left\lfloor \frac{l+u}{2} \right\rfloor\\ & \ \ \ \ \ \ \ \ \ \ \texttt{if }\ \ f(m) \ge 1\\ & \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ l \gets m + 1\\ & \ \ \ \ \ \ \ \ \ \ \texttt{else }\\ & \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ u \gets m - 1\\ & \ \ \ \ \ \ \ \ \ \ \texttt{end if }\\ &\texttt{end while }\\ &\texttt{return }\ u \end{align} The algorithm terminates by giving $u$ as the largest $k\in \{1,\dots,n\}$ satisfying $f(k) \ge 1$. Solving a few numerical examples, I think the algorithm works properly. However, I want to know how we can prove that for any given $n$ and $f(\cdot)$ it gives a correct result. Any suggestions? Basically, I'm looking for a rigorous proof that why the sequence of numbers assigned to $u$ converges to the largest $k\in \{1,\dots,n\}$ satisfying $f(k) \ge 1$.
As I mentioned in my comment to another answer the current algorithm has some non-intuitive behavior (upper limit is less than lower limit on loop exit). For the sake of reasoning, IMO eliminating non-intuitive behavior helps.
I suggest writing the algorithm recursively and then show that if an invocation with a particular set of inputs is correct, then an invocation with that set plus an additional element is correct. In other words use induction. Here is a useful post on the subject: https://stackoverflow.com/questions/9538562/general-proof-strategies-to-show-correctness-of-recursive-functions.
As an example:
\begin{align} \ &\text{// make sure at least one element is } \geq 1\\ \ &\text{assert } f(0) \geq 1\\ \ &bs(1, upper, middleOut)\\ \\ \ \text{fun}& \text{ction bs( lower, upper, middleOut)}\\ & \text{// middleOut is an output parameter}\\ & \text{assert } lower \leq upper\\ &\text{if } lower = upper\\ &\ \ \ \text{if } f(lower) \geq 1 \\ &\ \ \ \ \ \ \text{return }f(lower)\\ &\ \ \ \text{else}\\ &\ \ \ \ \ \ \text{return }f(lower-1)\\ &\ \ \ \text{end if}\\ &\text{end if}\\ \\ &middleOut \gets (lower+upper)/2\\ &\text{if }f(middleOut) \geq 1\\ &\ \ \ \text{return } bs(middleOut+1, upper, middleOut)\\ &\text{else}\\ &\ \ \ \text{return } bs(lower, middleOut, middleOut, result)\\ &\text{end if} \end{align}
The recursion termination part at the beginning is clearly correct. First it ensures the function stops. Either $lower$ increases or $upper$ decreases on each recursion, so eventually they equal each other (or else first assert is hit, which means there is a bug)
Functionally it's correct also. If we are searching an array slice of length one (ie $upper = lower$), the array slice either has it's one element $\geq 1$ or else it doesn't and the element proceeding slice is $\geq 1$ (this assertion is proved by examining recursive code and noting that $f(1) \geq 1$).
The recursive code is invoked if $lower < upper$. On each invocation $middleOut$ is set: $lower \leq middleOut < upper$ (the $\leq$ is because the divide by two rounds down). Thus $middleOut$ is always within expected range.
$lower$ is always set $\leq upper$, because when it increases, it increases to $middleOut+1$ and since $middleOut < upper$ then $middleOut+1 \leq upper$.
There are two cases to consider to show $upper$ is always set $\geq lower$. First case is if $lower < middleOut$ then $upper \gets middleOut$. This ensures $lower < upper$. Second case is if $lower = middleOut$. In this case $upper \gets middleOut$ and $lower = upper$
Case 1) If $f(middleOut) \geq 1$ then the desired element's index $\geq middleOut$. Invoking the binary search again as $bs(middleOut+1,upper,middleOut)$ either finds the desired element in the range $middleOut+1$ to $upper$ or else all elements in that range are $< 1$. When $bs(middleOut+1,upper,middleOut)$ finally terminates, it either returns the desired element from the range, or else the element immediately before the range.
Case 2) If $f(middleOut) < 1$ then the desired element's index $< middleOut$. Invoking the binary search again as $bs(lower, middleOut,middleOut)$ finds the desired element.
So in both cases if $bs$ works with a set of numbers, then $bs$ works with a superset of those numbers.