Loop Invariant for First-True Binary Search

Hello again. In the previous lesson, you chose a half-open search interval $[lo,hi)$ for a first-true search and gave it a contract: return the first index where a monotone predicate becomes true, or $n$ if it never does.

This lesson makes that contract durable during the loop. A loop invariant is the precise statement that remains true before the first iteration and after every iteration. For binary search, it is the difference between a template you remember and an algorithm you can safely adapt under pressure.

By the end, you will be able to state the invariant for a half-open first-true search over integer indices, interpret each part, and use it to inspect a trace for correctness.

---

The object we must not lose: the boundary

Let $P$ be a monotone predicate over indices $0$ through $n-1$:

$$P(0),P(1),\dots ,P(n-1)=[F,F,\dots ,F,T,T,\dots ,T]$$

Define the answer, the boundary $b$, as:

$$b=\min \left(\{i\in \{0,\dots ,n-1\}:P(i)\}\cup \{n\}\right)$$

Thus $b$ is always in $[0,n]$:

• $b=0$ when all elements are true.
• $b=n$ when all elements are false.
• Otherwise, $b$ is the first valid index satisfying $P$.

For a sorted vector a and target x, a standard example is:

$$P(i)\equiv a[i]\ge x$$

Then $b$ is the position returned by std::lower_bound.

Binary search does not need to know $b$ directly. It needs to preserve the fact that $b$ remains among the positions still possible.

---

The half-open first-true invariant

For the half-open formulation, initialize:

int lo = 0;
int hi = n;

and continue while:

while (lo < hi)

The full loop invariant is:

$$0\le lo\le hi\le n$$ $$\forall i\in [0,lo),P(i)=\text{false}$$ $$\forall i\in [hi,n),P(i)=\text{true}$$

Read this as a three-part claim.

Part	Meaning
$0\le lo\le hi\le n$	The bounds form a valid half-open subinterval of the index domain.
Every index before lo is false	The first true cannot be to the left of lo.
Every index from hi onward is true	The first true cannot be to the right of hi.

The unresolved indices are those in:

$$[lo,hi)$$

But the boundary itself is a position, not necessarily an element index. Therefore the invariant says the answer satisfies:

$$lo\le b\le hi$$

This is the compact “candidate containment” form of the invariant.

First-true invariant: lo never passes the first true position, and hi never falls before it.

The more detailed false-prefix and true-suffix version is usually better when proving updates. The compact version is excellent for quickly checking whether an implementation has discarded the answer.

---

Why empty regions make the invariant work

The initial state is:

$$lo=0,hi=n$$

At that moment:

• The false region $[0,lo)$ is $[0,0)$, which is empty.
• The true region $[hi,n)$ is $[n,n)$, also empty.
• The possible boundary interval is $[0,n]$, so every legal answer is still possible.

Statements about every element in an empty interval are automatically true. This is called vacuous truth, and it is doing useful engineering work here: no special branch is required for all-true, all-false, or empty inputs.

For an empty vector:

$$n=0,lo=hi=0$$

The loop does not run. The invariant already implies:

$$b=0$$

which is exactly the correct insertion position.

---

---

A concrete invariant trace

Consider this predicate:

$$[P(0),P(1),P(2),P(3),P(4)]=[F,F,F,T,T]$$

The boundary is:

$$b=3$$

Use the usual midpoint:

$$mid=lo+\lfloor \frac{hi-lo}{2}\rfloor$$

The trace below emphasizes what has been proved, rather than merely recording variables.

State	lo	hi	Known false indices	Known true indices	Boundary still possible at
Initially	0	5	none	none	$0$ through $5$
After testing mid = 2, false	3	5	$0,1,2$	none	$3$ through $5$
After testing mid = 4, true	3	4	$0,1,2$	$4$	$3$ through $4$
After testing mid = 3, true	3	3	$0,1,2$	$3,4$	$3$ only

At the final state:

$$lo=hi=3$$

Since the invariant says $lo\le b\le hi$, it forces:

$$b=3$$

Notice what never appears in this reasoning: “we happened to save the best answer seen so far.” The bounds themselves encode all the information needed to recover the answer.

---

The midpoint is evidence, not just a location

At the start of every loop iteration, the guard gives:

$$lo<hi$$

With the half-open midpoint formula,

$$mid=lo+\lfloor \frac{hi-lo}{2}\rfloor$$

we have:

$$lo\le mid<hi$$

So mid is always a valid array index. In particular, although hi may equal $n$, the predicate is never evaluated at $P(n)$.

Now consider what each predicate result proves.

When $P(mid)$ is false

Monotonicity says every index at or before mid is false:

$$\forall i\le mid,P(i)=\text{false}$$

Therefore the first true position cannot be at mid or to its left. The lower bound can move to:

$$lo=mid+1$$

The false-prefix portion of the invariant becomes larger, while hi stays unchanged. Crucially, $b$ remains in the allowed interval.

When $P(mid)$ is true

Monotonicity says every index from mid onward is true:

$$\forall i\ge mid,P(i)=\text{true}$$

The midpoint might itself be the first true index, so it cannot be discarded. The upper bound becomes:

$$hi=mid$$

The true-suffix portion of the invariant becomes larger, and the boundary remains possible because it may equal the new hi.

These updates will be derived formally in the next lesson. For now, recognize their invariant-level meaning:

Observation	New fact established	Bound that moves
$P(mid)$ is false	All positions through mid are false	lo = mid + 1
$P(mid)$ is true	All positions from mid are true	hi = mid

This is why hi = mid is correct in a half-open first-true loop, while lo = mid would be wrong in the false case: it would retain an index already proved false and can fail to make progress.

---

---

Two equivalent ways to state the invariant

When writing a proof or explaining your solution in an interview, choose one of these forms, then be ready to translate between them.

1. Classification form

$$0\le lo\le hi\le n$$ $$\forall i<lo,P(i)=\text{false}$$ $$\forall i\ge hi\text{ with }i<n,P(i)=\text{true}$$

This form states exactly what the algorithm has learned about the domain. It is best for deriving and checking updates.

2. Boundary-containment form

Let $b$ be the first true position, with $b=n$ if no true index exists. Then:

$$0\le lo\le b\le hi\le n$$

This form states that the answer remains bracketed. It is concise and makes the termination argument almost immediate.

The two forms are equivalent because $P$ is monotone. For example, if all indices before lo are false, then $b$ cannot be less than lo. If all actual indices from hi onward are true, then $b$ cannot exceed hi.

A strong explanation often states both:

All indices before lo are known false and all indices from hi onward are known true; equivalently, the first true boundary remains in the closed position interval $[lo,hi]$.

Be precise about the subtle contrast:

• The unresolved element interval is half-open: $[lo,hi)$.
• The possible boundary positions form a closed interval: $[lo,hi]$.

That one-character difference explains many apparent off-by-one mysteries.

---

Diagnosing invariant mistakes

A loop can look plausible while maintaining an invariant too weak or simply wrong.

Mistake 1: “The answer is inside the unresolved array interval”

One might say:

$$b\in [lo,hi)$$

This fails when hi itself is the correct boundary position. For example, with all false values:

$$P=[F,F,F]$$

the correct answer is $b=n=3$. Initially hi = 3, but $3\notin [0,3)$.

The correct statement is:

$$b\in [lo,hi]$$

The answer is a position, so it may equal the exclusive endpoint of the unresolved element interval.

Mistake 2: evaluating the predicate at hi

Because hi can equal $n$, this is invalid:

if (P(hi)) {
    // ...
}

The invariant guarantees only that indices in $[hi,n)$ are true when they exist. It does not define $P(n)$.

Mistake 3: treating “known true” as “the answer”

If $P(mid)$ is true, mid is an answer candidate, but it is not necessarily the first true index. The invariant only lets you conclude:

$$b\le mid$$

That is why the search continues to the left rather than returning immediately.

Mistake 4: omitting the bounds condition

The semantic claims about false and true regions are not enough by themselves for safe implementation. You also need:

$$0\le lo\le hi\le n$$

It proves that mid is in range whenever the loop runs and that the arithmetic has a well-defined interval interpretation.

---

A proof-oriented code annotation

Here is the template annotated with the invariant you should be able to state from memory:

template <class Pred>
int first_true(int n, Pred P) {
    int lo = 0;
    int hi = n;

    // Invariant:
    // 1. 0 <= lo <= hi <= n
    // 2. P(i) is false for every i in [0, lo)
    // 3. P(i) is true  for every i in [hi, n)
    // Therefore, the first true boundary b satisfies lo <= b <= hi.

    while (lo < hi) {
        int mid = lo + (hi - lo) / 2;

        if (P(mid)) {
            hi = mid;
        } else {
            lo = mid + 1;
        }
    }

    return lo;
}

At termination, the loop guard is false:

$$lo\nless hi$$

Together with the range part of the invariant, $lo\le hi$, this yields:

$$lo=hi$$

And since the boundary-containment invariant says:

$$lo\le b\le hi$$

we conclude:

$$b=lo=hi$$

That is the central correctness story in one chain of reasoning. A later lesson will separate it into the standard proof obligations: initialization, preservation, termination, and partial correctness.

---

Conclusion

A half-open first-true binary search maintains more than an interval of indices. It maintains a classification of the entire domain:

• $[0,lo)$ is proved false.
• $[hi,n)$ is proved true.
• The first-true boundary $b$ remains in $[lo,hi]$.
• The range condition $0\le lo\le hi\le n$ keeps all midpoint accesses safe.

The key conceptual distinction is that $[lo,hi)$ contains unresolved elements, whereas $[lo,hi]$ contains possible boundary positions. Once lo and hi meet, the invariant forces that shared position to be the answer.

Next, you will derive the midpoint updates formally and show that each one preserves this invariant rather than merely seeming intuitive.