断言、forall 和映射：通用量词不适用于映射

Question

在这个例子中，我只在一个映射中插入一个值，我试图断言这个映射中的任何两个键是相同的。但是断言失败。这是 link.

datatype HostState = HostState(counter:nat, vote: map<nat, set<nat>>)
predicate HostInit(s:HostState, counter: nat) {
  var default: nat := 0;
  && s.counter == 1
  && |s.vote| == 1 && default in s.vote
}

lemma lemma_UniqueKey(){
  var default: nat := 0;
  assert forall s, counter :: HostInit(s, counter) ==>
  (
    // |s.vote| == 1 && default in s.vote // Pass
    (forall t: nat, t': nat :: t in s.vote && t' in s.vote ==> t' == t) // Fail
    // (forall t: nat :: t in s.vote) // Not even this works
  );
}

仅当我使用 forall 遍历地图时断言才会失败。关于为什么断言失败的任何线索？

Answer 1

不幸的是，Dafny 没有 built-in 理解 cardinality-one 和您提到的量化属性之间的关系。这是让 Dafny 相信这一事实的一种方法。

我们可以将推理分解为关于地图的通用引理。

lemma CardinalityOneMap<A,B>(m: map<A,B>)
  requires |m| == 1
  ensures forall x, y | x in m && y in m :: x == y
{
  CardinalityOneSet(m.Keys);
}

这个引理只是说如果一个映射的基数为 1，那么它的所有键都是相等的。该证明在地图的键集上调用了关于集合的类似引理。

lemma CardinalityOneSet<A>(s: set<A>)
  requires |s| == 1
  ensures forall x, y | x in s && y in s :: x == y
{
  var z :| z in s;
  var s' := s - {z};
  assert |s'| == 0;  // this is enough for dafny to see s' is empty
}

这个引理是关于集合的相应事实。证明有点奇怪，并且依赖于（未记录，learned-by-fire）事实，即 Dafny 确实理解一组基数 0 是空的。所以我们抓取 s 的“任意”元素 z，然后构造集合 s - {z}。然后我们提到这个新集合的基数，Dafny 突然注意到这个集合必须是空的，这意味着 s 必须只包含 z，我们就完成了。

随着引理的证明，我们可以return你的代码。

lemma lemma_UniqueKey(){
  var default: nat := 0;
  forall s, counter | HostInit(s, counter) 
    ensures (forall t: nat, t': nat :: t in s.vote && t' in s.vote ==> t' == t)
  {
    CardinalityOneMap(s.vote);
  }

  assert forall s, counter :: HostInit(s, counter) ==>
    (forall t: nat, t': nat :: t in s.vote && t' in s.vote ==> t' == t)
  ;
}

您想证明关于所有状态的断言。为此，我们需要在 s 上调用我们的引理 CardinalityOneMap，但是 s 是通用量词下的一个变量，因此我们需要使用 forall 声明来做到这一点。在陈述之后，如果我们愿意，我们可以 re-assert 同样的事实，只是为了再次检查 Dafny 现在是否被说服了。

以下是一些可能相关的其他答案：

Proving facts about cardinality of range sets

PS：很高兴看到您正在学习分布式系统课程！

断言、forall 和映射：通用量词不适用于映射

Assertion, forall, and maps: Universal quantifiers does not work with maps

dafny