达芙妮。带有布尔值的对不等于

【问题标题】：Dafny. Pairs with bools do not equal达芙妮。带有布尔值的对不等于
【发布时间】：2019-10-22 00:49:15
【问题描述】：

为什么这两个在 Dafny 中失败了？

lemma test(x : (int, bool)) {
  assert x == (x.0, true) || x == (x.0, false);
}

lemma test''(v : int, x : (int, bool))
  requires x.0 == v; 
{
  assert x == (v, true) || x == (v, false);
}

https://rise4fun.com/Dafny/DtDMdm

【问题讨论】：

标签： dafny

【解决方案1】：

我猜这与元组可以包含的泛型类型的布尔值的内部装箱有关。无论如何，这里有一个简单的解决方法：

lemma test(x : (int, bool)) {
  var (i, b) := x;
  assert x == (x.0, true) || x == (x.0, false);
}

鲁斯坦

【讨论】：