§ Correctness of lower_bound search with half-open intervals

// precondition: `xs` is sorted.
// find rightmost i such that xs[i] <= y and dp[i+1] > y.
int tallest(vector<long> &xs, int y) {
    // [l, r)
    int l = 0, r = dp.size();
    // precondition: l < r
    while(1) {
        if (l + 1 == r) { return l; }
        // info gained from if: r > (l+1)
        int m = (l+r)/2;
        // should this be (xs[m] > y) or (xs[m] >= y)?
        if (xs[m] > y) {
            r = m; // will decrease interval floor division.
        } else {
            // r > (l+1)
            // so m := (l+r/2) > (2l+1)/2 > l.
            l = m;
        }
    }
}

• Firt see that if we can find such an i, then in the extreme case where the array does not have a greater element, we would like the find the rightmost i that fulfils the condition that xs[i] <= y. So in our imagination, we right pad the array with an infinitely large value.
• We wish to know whether the if condition should have xs[m] > y or xs[m] >= y before it decides to shrink the search range.
• Intuitively, we wish to move the search range rightwards. So if we have xs[m] == y, we must move l towards m to move the search range rightwards. For more clarity, let's write the above as:

// precondition: `xs` is sorted.
// find i such that xs[i] <= y and dp[i+1] > y.
int tallest(vector<long> &xs, int y) {
    // [l, r)
    int l = 0, r = dp.size();
    // precondition: l < r
    while(1) {
        if (l + 1 == r) { return l; }
        // info gained from if: r > (l+1)
        int m = (l+r)/2;
        // should this be (xs[m] > y) or (xs[m] >= y)?
        if (xs[m] > y) {
            // move interval towards `l` for smaller values.
            r = m; // will decrease interval floor division.
        } else if (xs[m] < y) {
            // move interval towards `r` for larger values.
            // r > (l+1)
            // so m := (l+r/2) > (2l+1)/2 > l.
            l = m;
        } else {
            //xs[m] == y
            // we want rightmost index `l` where `xs[l] <= y`.
            // - this `xs[m]` is a legal index.
            // - we want rightmost `m`. Since `m > l`, move `l` rightward by setting `l = m`.
            l = m;
        }
    }
}