§ 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
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.
k value: k[i]=2i(k-1) value: k[i1]=2i1=2k[i]Ind: p(ans[i]+2k[i])=0Case (a): p(ans[i]+k[i])=0Update: ans[i1]ans[i]+k[i]p(ans[i1]+2k[i1])=p((ans[i]+k[i])+2k[i1])=p(ans[i]+k[i]+k[i])=p(ans[i]+2k[i])=1 (By Induction Hyp.) \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 (i1)(i-1) in case (a) where we update the value of ans[i]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.
k value: k[i]=2i(k-1) value: k[i1]=2i1=2k[i]Ind: p(ans[i]+2k[i])=0Case (b): p(ans[i]+k[i])=1Update: ans[i1]ans[i]p(ans[i1]+2k[i1])=p(ans[i]+2k[i1])=p(ans[i]+k[i]+k[i])=p(ans[i]+2k[i])=1 (By Induction Hyp.) \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 (i1)(i-1) in case (b) where we don't change the value of ans[i]ans[i].
  • In summary, the loop invariant is held at index (i1)(i-1) assuming the loop invariant is satisfied at index (i)(i), for both updates of ans[i]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];
}