Proving the 100 Prisoners and a lightbulb with Dafny

Question

Consider the standard strategy to solve the 100 prisoners and a lightbulb problem. Here's my attempt to model it in Dafny:

method strategy<T>(P: set<T>, Special: T) returns (count: int)
  requires |P| > 1 && Special in P
  ensures count == (|P| - 1)
  decreases *
{
  count := 0;
  var I := {};
  var S := {};
  var switch := false;

  while (count < (|P|-1)) 
    invariant count <= (|P|-1) 
    invariant count > 0 ==> Special in I
    invariant Special !in S && S < P && S <= I && I <= P 
    decreases *
  { 
    var c :| c in P;
    I := I + {c};

    if c == Special {
      if switch == true {
        switch := false;
        count := count + 1;
      }
    } else {
      if c !in S && switch == false {
        S := S + {c};
        switch := true;
      }
    }
  }  

  assert(I == P);  
}

It fails, however, to prove that in the end I == P. Why? I probably need to strengthen the loop invariant even further, but can't imagine where to start from...

Answer 1

Here is one way to do it.

I had to add one conceptually key loop invariant and one not-so-conceptually-key-but-helpful-to-Dafny lemma.

You need a loop invariant that connects count to the various sets somehow. Otherwise the fact that count == |P| - 1 after the loop isn't very useful. I chose to use

if switch then |S| == count + 1 else |S| == count

which connects count to the cardinality of S. (I think of S as the set of prisoners counted by The Counter.) When the light is off, count is up to date (ie, |S| == count). But when the light is on, we are waiting for The Counter to notice and update the count, so it is one behind (ie, |S| == count + 1).

With this loop invariant, we can now argue that I == P after the loop. By one of your other loop invariants, we already know I <= P. So it suffices to prove P <= I. Suppose instead that I < P. Then we have S < I < P. But by the loop exit condition, we also have |S| == |P| - 1. This is impossible.

The only wrinkle is that Dafny can't directly connect the subset relationships with the cardinality relationships, so we have to help it out. I proved a lemma, CardinalitySubset, which, given sets A and B such that A < B, it follows that |A| < |B|. The proof goes by induction on B, and is relatively straightforward. Calling it with the relevant sets finishes the main proof.

---

As an aside, I looked a little bit into why Dafny doesn't directly connect subset relationships to cardinality relationships. In Dafny's axioms about sets, I found a commented out axiom relating cardinality with subsets. (Admittedly, this axiom is about the non-strict subset relation, but by uncommenting this axiom, I was able to get a version of the proof to go through without additional lemmas, so it would be sufficient.) Tracing it back to why the axiom was commented out, it seems like the solver was using it too much even when it wasn't relevant, which slowed things down.

It ends up not being a huge deal because we can prove what we need by induction, but it's an interesting tidbit.