Why a binary search algorithm works? 
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$.
 A: Hint: let $k \in \{ 1, \ldots, n \}$ be the solution to the problem. Prove that the $\texttt{while}$ loop has the following invariant: $l-1 \leqslant k \leqslant u$ and that $u-l$ decreases, hence the algorithm stops.
A: This is a very basic computer science result wrapped up in lot of mathematical notation. Basically, you have $n$ elements in an array and each entry corresponds to the sample of the function at that index. Thus, if $i$ is the position, then $f(i)$ is the value. It is already given that $f(i)$ is a decreasing function. Thus $f(i)>f(i+1)$ for all $i$. Thus $f(1)$ is the largest. Basically, the array is already sorted for you. Now, if it wasn't, to find the largest element in an array is a linear operation, i.e. order of $O(n)$.
A: 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. 
