在Dafny中证明有序唯一键序列的KeySet长度与序列长度相等

我在Dafny中实现了一个已验证的SortedMap，它由（键，值）对组成的序列构成，其中键是排序后的唯一整数。但无法证明KeySet的长度必须等于该序列的长度，错误信息如下：

this is the postcondition that could not be proved
  |
7 |   ensures |KeySet(sorted_seq)| == |sorted_seq|

简化后的代码：

predicate SortedSeq(sequence: seq<(int, int)>) {
  forall i, j | 0 <= i < j < |sequence| :: sequence[i].0 < sequence[j].0
}

function KeySet(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  set i | i in sorted_seq :: i.0
}


method Main()
{
  var s: seq<(int,int)> := [(1, 2), (30, 40), (50, 50)];
  print KeySet(s);
}

问题原因 #

SortedSeq谓词保证了序列中的键严格递增，因此所有键必然唯一。但Dafny的自动验证器无法直接从集合推导的语法中，关联出“严格递增的键对应集合中元素个数等于序列长度”这一结论。集合推导式set i | i in sorted_seq :: i.0的唯一性需要显式的推理支持。

解决方法 #

可以通过以下两种方式让Dafny完成证明：

方法1：添加辅助引理

先证明满足SortedSeq的序列中所有键都是唯一的，再用这个引理来支持KeySet的后置条件：

predicate SortedSeq(sequence: seq<(int, int)>) {
  forall i, j | 0 <= i < j < |sequence| :: sequence[i].0 < sequence[j].0
}

lemma KeysUnique(sequence: seq<(int, int)>)
  requires SortedSeq(sequence)
  ensures forall i, j | 0 <= i < j < |sequence| :: sequence[i].0 != sequence[j].0
{
  // 由SortedSeq的严格递增直接可得键唯一，Dafny能自动验证这个引理
}

function KeySet(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  set i | i in sorted_seq :: i.0
}
{
  KeysUnique(sorted_seq);
}

方法2：递归定义KeySet

改用递归方式构建键集合，同时维护“集合大小等于当前处理的序列长度”的不变量，这样Dafny更容易跟踪：

predicate SortedSeq(sequence: seq<(int, int)>) {
  forall i, j | 0 <= i < j < |sequence| :: sequence[i].0 < sequence[j].0
}

function KeySet(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  if sorted_seq == [] then
    {}
  else
    KeySet(sorted_seq[0..|sorted_seq|-1]) + {sorted_seq[|sorted_seq|-1].0}
}
{
  if sorted_seq == [] {
    assert |KeySet(sorted_seq)| == 0 == |sorted_seq|;
  } else {
    var prev := sorted_seq[0..|sorted_seq|-1];
    var lastKey := sorted_seq[|sorted_seq|-1].0;
    assert forall k in KeySet(prev) :: k < lastKey;
    assert lastKey !in KeySet(prev);
    assert |KeySet(sorted_seq)| == |KeySet(prev)| + 1 == |prev| + 1 == |sorted_seq|;
  }
}

内容的提问来源于stack exchange，提问作者Carl