A Universe of Sorts

§ Binary search to find rightmost index which does not possess some property

// p for predicate/property
// precondition: p(0) = false
// precondition: p(1 << NBITS) = last ix we process.
// precondition: p is monotonic;
//   once it switches to true, does not switch back to false.

if (p(1 << NBITS) == 0) { return 1 << NBITS; }
else {
  assert(p(1<<NBITS) == 1);
  int ans = 0;
  for (int i = NBITS-1; i >= 0; i--) {
    int k = 1 << i;
    assert(p(ans + 2*k) == 1);
    if (p(ans + k) == 0) {
      ans = ans + k;
    }
  }
}
// postcondition:
// ans is largest index such that
// has_some_poperty(ans) = 0

Claim 1: (Correctness) p(ans[i]) = 0. By precondition, this is true before the loop. See that it's a loop invariant, as we only update ans[i] to ans[i]+k if p(ans[i]+k) = 0. Thus, is is true after the loop.

Claim 2: (Maximality) : At loop iteration i: p(ans[i] + 2k[i]) = 1. We cannot improve our solution by using previous jump lengths.

This implies optimality once the loop ends. At the end of the loop we have i = -1. So:

2k[-1] = 2(1/2) = 1
finalans = ans[-1]
---
p(ans[-1] + 2k[-1]) = 1
=> p(finalans+1) = 1

Proof of Claim 2: induction on i
Suppose claim 2 is true till index i: p(ans[i] + 2k[i]) = 1.
To prove: induction hypothesis holds at index (i-1).
Case analysis based on loop body at i: p(ans[i] + k[i]) = 0 or 1
(a) p(ans[i] + k[i]) = 0. We update ans[i-1] = ans[i] + k[i].
We wish to show that the loop invariant holds at i-1: p(ans[i-1]+2k[i-1]) == 1.

\begin{aligned} &\text{k value: } k[i] = 2^i \\ &\text{(k-1) value: } k[i-1] = 2^{i-1} = 2k[i] \\ &\text{Ind: } p(ans[i] + 2k[i]) = 0 \\ &\text{Case (a): } p(ans[i] + k[i]) = 0 \\ &\text{Update: } ans[i-1] \equiv ans[i] + k[i] \\ &p(ans[i-1] + 2k[i-1]) \\ &= p((ans[i] + k[i]) + 2k[i-1]) \\ &= p(ans[i] + k[i] + k[i])\\ &= p(ans[i] + 2k[i]) \\ &= 1 ~\text{(By Induction Hyp.)} \end{aligned}

We've shown that the induction hypothesis hold at index $(i-1)$ in case (a) where we update the value of $ans[i]$ .

(b) If p(ans[i] + k[i]) = 1, then we update ans[i-1] = ans[i].
We wish to show that the loop invariant holds at i-1: p(ans[i-1]+2k[i-1]) ==1.

\begin{aligned} &\text{k value: } k[i] = 2^i \\ &\text{(k-1) value: } k[i-1] = 2^{i-1} = 2k[i] \\ &\text{Ind: } p(ans[i] + 2k[i]) = 0 \\ &\text{Case (b): } p(ans[i] + k[i]) = 1 \\ &\text{Update: } ans[i-1] \equiv ans[i] \\ &p(ans[i-1] + 2k[i-1]) \\ &= p(ans[i] + 2k[i-1]) \\ &= p(ans[i] + k[i] + k[i])\\ &= p(ans[i] + 2k[i]) \\ &= 1 ~\text{(By Induction Hyp.)} \end{aligned}

We've shown that the induction hypothesis hold at index $(i-1)$ in case (b) where we don't change the value of $ans[i]$ .

In summary, the loop invariant is held at index $(i-1)$ assuming the loop invariant is satisfied at index $(i)$ , for both updates of $ans[i]$ . Thus, by induction, the loop invariant holds for all iterations.

Elaborated proof of why p(ans[0]+1) = 1 at the end of the loop

See that we can insert a new invaraiant at the end of the loop which asserts p(ans[i]+k[i]) == 1:

if (p(1 << nbits) == 0) { return 1 << nbits; }
else {
  assert(p(1<<nbits) == 1);
  int ans = 0;
  for (int i = nbits-1; i >= 0; i--) {
    int k = 1 << i;
    assert(p(ans + 2*k) == 1);
    int ans2;
    if (p(ans + k) == 0) {
      ans2 = ans + k;
      // ans2 + k
      // = (ans + k) + k
      // = ans + 2k
      // = 1 (from assertion)
    } else {
       ans2 = ans;
      // ans2 + k
      // = ans + k
      // = 1 [from else branch]
    }
    // ## new loop end invariant ##
    // true from then, else branch.
    assert(p(ans2+k) == 1)
    ans = ans2;
  }
}

We've proven the correctness of the loop invariant at the end of the loop, given the prior loop invariant at the beginning of the loop.
So, At the end of the (i=0) iteration, we have k=1, and so p(ans+1) == 1, which is the "rightmost index" condition. that we originally wanted.

§ Fully elaborated proof

if (p(1 << nbits) == 0) { return 1 << nbits; }
else {
  assert(p(1<<nbits) == 1);
  int ans = 0;
  // p(ans[nbits-1] + 2*(1<<nbits-1))
  // = p(0 + 1 << nbits)
  // = p(1 << nbits)
  // = 1 [from assert]
  for (int i = nbits-1; i >= 0; i--) {
    int k = 1 << i;
    // From previous loop iteratio (i+1):
    // ---------------------------------
    // p(ans[(i+1)-1] + k[i+1]) == true
    // => p(ans[i] + k[i+1]) == true
    // => p(ans[i] + 2k[i]) == true
    assert(p(ans + 2*k) == true);

    if (p(ans + k) == 0) {
      ans += ans + k;
      // ASSIGNMENT: ans[i-1] = ans[i] + k[i]
      // p(ans[i-1] + k[i])
      // = p(ans[i] + k[i] + k[i])
      // = p(ans[i] + 2k[i])
      // = p(ans[i] + k[i+1])
      // = 1 (from induction hyp)
    } else {
       ans = ans; // no-op
       // ASSIGNMENT: ans[i-1] = ans[i].
       // p(ans[i-1] + k[i])
       // = p(ans[i] + k[i])
       // = 1 (from else branch)
    }
    // ## new loop end invariant ##
    // p(ans[i-1] + k[i])== 1
    assert(p(ans+k) == 1)
  }
}

§ Simplified implementation

If we are willing to suffer some performance impact, we can change the loop to become significantly easier to prove:

if (p(1 << nbits) == 0) { return 1 << nbits; }
else {
  assert(p(1<<nbits) == 1);
  int ans = 0;
  int i = nbits-1;
  while(i >= 0) {
    assert (p(ans+2*k) == 1);
    int k = 1 << i;
    if (p(ans + k) == 0) {
      ans += ans + k;
    } else {
        i--;
    }
    assert(p(ans) == 0)
  }
}

In this version of the loop, we only decrement i when we are sure that p(ans+k) == 0. We don't need to prove that decrementing i monotonically per loop trip maintains the invariant; Rather, we can try "as many is as necessary" and then decrement i once it turns out to not be useful.

§ Relationship to LCA / binary lifting

This is very similar to LCA, where we find the lowest node that is not an ancestor. The ancestor of such a node must be the ancestor.

int lca(int u, int v) {
    if (is_ancestor(u, v)) return u;
    if (is_ancestor(v, u)) return v;

    // u is not an ancestor of v.
    // find lowest parent of u that is not an ancestor of v.
    for (int i = l; i >= 0; --i) {
        if (!is_ancestor(up[u][i], v))
            u = up[u][i];
    }
    return up[u][0];
}