用Dafny证明100名囚犯和灯泡

Question

考虑解决100名囚犯的标准策略和灯泡问题.这是我在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);  
}

然而,它最终无法证明这一点I == P.为什么？我可能需要进一步强化循环不变量,但无法想象从哪里开始......

Answer 1

这是一种方法。

我必须添加一个概念上关键的循环不变量和一个概念上不那么关键但对 Dafny 引理有帮助的引理。

count您需要一个以某种方式连接到各个集合的循环不变量。count == |P| - 1否则，循环之后的事实并不是很有用。我选择使用

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

这count与 的基数有关S。（我认为S是由计数器计数的囚犯集合。）当灯关闭时，count是最新的（即|S| == count）。但是当灯亮起时，我们正在等待计数器注意到并更新计数，因此它落后了一位（即，|S| == count + 1）。

I == P有了这个循环不变式，我们现在可以在循环之后争论。通过你的其他循环不变量之一，我们已经知道了I <= P。所以只要证明就可以了P <= I。假设I < P. 然后我们就有了S < I < P。但根据循环退出条件，我们也有|S| == |P| - 1. 这是不可能的。

唯一的问题是 Dafny 无法直接将子集关系与基数关系联系起来，因此我们必须帮助它解决。我证明了一个引理 ，CardinalitySubset给定集合A等B，A < B则得出|A| < |B|。证明是通过归纳法进行的B，并且相对简单。用相关集合调用它就完成了主要证明。

顺便说一句，我研究了为什么 Dafny 不直接将子集关系与基数关系连接起来。在达夫尼关于集合的公理中，我发现了一个注释掉的公理，将基数与子集相关联。（诚​​然，这个公理是关于非严格子集关系的，但是通过取消注释这个公理，我能够得到一个不需要额外引理的证明版本，所以这就足够了。）追溯到为什么axiom 被注释掉了，似乎解算器使用它太多，即使它不相关，这减慢了速度。

这最终并不是什么大不了的事，因为我们可以通过归纳法证明我们需要什么，但这是一个有趣的花絮。