< on unary numbers in Dafny

Question

我无法使用 Dafny 证明以下内容： S(x) < S(y) ==> x < y for the datatype of unary numbers with constructors Z and S (here I am only using S).

我尝试了各种归纳法，我怀疑原因在于 一般来说 < relation, but still I am wondering whether there could be a way out.

Answer 1

数据类型的内置

<

运算符可能无法实现您想要的功能。我建议根据您的类型定义您自己的“小于”概念。那么你应该可以正常使用感应了。

---

请参阅参考手册，了解如何为数据类型定义内置

<

运算符：

操作员< is defined for two operands of the same datataype. It means is properly contained in. For example, in the code

datatype X = T(t: X) | I(i: int)
method comp() {
  var x := T(I(0));
  var y := I(0);
  var z := I(1);
  assert x.t < x;
  assert y < x;
  assert !(x < x);
  assert z < x; // FAILS
}

x 是一个包含 T 变量的数据类型值，T 变量包含 I 变量，I 变量包含整数 0。值 x.t 是由 x 表示的数据类型结构的一部分，因此 x.t < x is true. Datatype values are immutable mathematical values, so the value of y is identical to the value of x.t, so y < x is true also, even though y is constructed from the ground up, rather than as a portion of x. However, z is different than either y or x.t and consequently z < x is not provable. Furthermore, < does not include ==, so x < x is false.

请注意，只有 < is defined; not <= or > 或 >=。

还有，< is underspecified. With the above code, one can prove neither z < x nor !(z < x) and neither z < y nor !(z < y). In each pair, though, one or the other is true, so (z < x) || !(z < x) is provable.