为什么 Dafny 不能验证某些简单的集合基数和关系命题? [英] Why can't Dafny verify certain easy set cardinality and relational propositions?
问题描述
这是一个简单的 Dafny 程序:两行代码和三个断言.
方法 Main(){var S := set s: int |0 <= s <50 :: 2 * 秒；var T := 设置 t |在 S & &＜25;断言 |S|== 50;//不验证断言 T <= S;//验证断言 T <;//不验证}S 的基数是 50，但 Dafny 无法验证此声明，如书面所述.同样，T显然是S的子集，Dafny可以验证这个说法；但 T 也是 S 的真子集，Dafny 无法验证这一说法.
导致这些困难的幕后"是什么，正在学习和使用 Dafny 的人可能会预见和避免或处理这些困难吗?
Dafny 无法验证第一个断言，因为 Dafny 没有用于推理集合推导式基数的内置模型.所以它永远无法证明像 |S| 这样的方程== 50 本身.然而，它可以推理一些其他集合操作的基数，例如联合和单例集合.你可以用它来说服 Dafny |S|== 50 以一种相当迂回的方式，我将在下面展示.
Dafny 无法证明最后一个断言，因为它不够聪明，无法提出 S 中不在 T 中的元素.我们可以通过提及这样一个元素来帮助它.更多内容见下文.
设置合适的触发器
但首先，有一个关于集合理解的警告，说达夫尼找不到任何可以触发的术语".这与 Dafny 如何使用量词将集合推导式转换为一阶逻辑有关.Dafny 指示 Z3 使用某些句法模式(称为触发器)来推理量词，但此警告表示找不到此类模式.这个问题不仅仅是抽象的，Dafny 在推理这个理解上遇到了严重的麻烦:它甚至无法证明 0 in S.
解决此类问题的一种相当通用的方法是引入一个新函数来缩写公式中可用作触发器的某些部分.具体来说，定义
function method Double(n: int): int {2 * n}然后将理解重写为
var S := set s: int |0 <= s <50 :: 双打；这样 Dafny 就可以使用触发器Double(s).现在，每当你想说服 Dafny 某些东西在 S 中时，你可以用 Double(x) 来表示某些 x，而 Dafny将能够证明这一点.
例如，在新定义下显示0 in S，我们可以说
assert Double(0) in S;//删除它以查看下面的失败在 S 中断言 0；证明 T
到目前为止，我们所做的只是稍微调整程序，以便 Dafny 可以更好地推理 S.这已经足以修复你最终断言的证明 T <;S，接下来让我们看一下.
Dafny 理解 T <S 为(本质上)T <= S &&T != S.您已经看到它能够显示 T <= S，所以还需要证明 T != S.最简单的方法是展示一个集合中不在另一个集合中的元素，在这种情况下，一个 S 不在 T 中的元素.26就是这样一个元素，我们可以通过添加行来修复断言
assert Double(13) in S;//提及触发器；这证明了 S 中的 26断言 T <;//现在验证证明<代码>|S|== 50
最后，让我们回到第一个失败的断言，即 |S|== 50.这个更难修复.可能有更简短的证明，但我会向您展示一种方法，它也应该可以帮助您了解如何自行解决类似问题.
我们的方法是首先证明 S 可以用集合上两个更简单的函数表示，然后证明这两个函数如何影响基数的引理.
达夫尼能够展示
assert S == MapSet(Double, RangeSet(0, 50));其中 RangeSet(a,b) 是构造 a 和 b 和 MapSet 之间的整数集的函数 是一个将函数映射到集合上"的函数.这些函数定义如下:
函数方法 RangeSet(a: int, b: int): set{设置 x: int |a <= x <乙}函数方法 MapSet(f: A -> B, S: set): set{设置 x |S 中的 x :: f(x)} 因此，为了证明 |S| 的某些内容，只需对 RangeSet 的基数进行推理并证明(在合适的条件下)MapSet 保留基数.这里有两个引理来达到这个效果
引理 CardRangeSet(a: int, b: int)要求 a <= b减少 b - a确保 |RangeSet(a, b)|== b - a引理 CardMapSetInj(f: A -> B, S: set)需要 Injective(f)减小 S确保 |MapSet(f, S)|== |S| CardRangeSet 表示 a 和 b 之间的数字集的基数是 b - a，这应该是相当直观的，记住 RangeSet 包含 a 但exclusive b.
引理 CardMapSetInj 表示单射函数在映射到集合上时保留基数.请注意，Double 是单射的(Dafny 认为这是显而易见的——它不需要证明).还要注意，注入性假设对于引理成立是必要的，否则如果函数将输入集的两个元素发送到同一个输出元素，映射可能会降低基数.我们可以如下定义Injective:
谓词 单射(f: A -> B){对于所有 x, y :: x != y ==>f(x) != f(y)} 我将证明下面的两个引理，但首先让我们看看如何使用它们来完成显示|S|== 50.
assert S == MapSet(Double, RangeSet(0, 50));CardMapSetInj(Double, RangeSet(0, 50));断言 |S|== |范围集(0, 50)|;CardRangeSet(0, 50);断言 |S|== 50;//现在验证还不错！我们首先用 Double 调用 CardMapSet 来显示 |S|== |RangeSet(0, 50)|.然后我们调用CardRangeSet来显示|RangeSet(0, 50)|== 50，证明完成.
这两个引理都是通过归纳证明的.
引理 CardRangeSet(a: int, b: int)要求 a <= b减少 b - a确保 |RangeSet(a, b)|== b - a{如果 a != b {计算{|范围集(a, b)|;{ assert RangeSet(a, b) == {a} + RangeSet(a + 1, b);}|{a} + RangeSet(a + 1, b)|;1 + |范围集(a + 1, b)|;{ CardRangeSet(a + 1, b);}1 + (b - (a + 1));b - 一个;}}}CardRangeSet 通过对b - a 的归纳证明.Dafny 发现基本情况是微不足道的，所以我们只考虑 a != b 时的归纳步骤.证明的工作原理是展开RangeSet 拉出a，然后调用(a + 1, b) 上的归纳假设并清理.
(证明以计算方式编写.如果您不熟悉 calc，它允许您非常简洁易读地编写一系列方程.花括号中的行是证明显示下一行为何与前一行相等的注释.如果不需要注释，则可以省略.有关 calc 的更多详细信息，请参阅 Dafny 手册.)
lemma CardMapSetInj(f: A -> B, S: set)需要 Injective(f)减小 S确保 |MapSet(f, S)|== |S|{如果 S != {} {变量 x :|S中的x；计算{|地图集(f, S)|;{ assert MapSet(f, S) == MapSet(f, {x} + (S - {x})) == {f(x)} + MapSet(f, S - {x});}|{f(x)} + MapSet(f, S - {x})|;1 + |地图集(f, S - {x})|;{ CardMapSetInj(f, S - {x});}|S|;}}} CardMapSetInj 通过对参数集S 的归纳证明.同样，基本情况是微不足道的，被省略了.在 S 为非空的归纳步骤中，我们选择一个任意元素 x in S(这样一个 x 存在于 S代码> 为非空).然后我们可以在S上展开MapSet的定义，并在S - {x}上调用归纳假设.
(如果您不熟悉语法 var x :| x in S，这是 Dafny 的let such-that"语句.它有点类似于赋值语句，除了它不是为 x 分配一个特定的值，而是选择一个满足 :| 右侧谓词的任意值.在验证过程中，Dafny 验证存在这样一个元素.程序的其余部分除了满足谓词之外，对 x 的值一无所知.有关详细信息，请参阅 Dafny 参考.)
总结
这里基本上有两个想法:
- 引入新函数作为触发器
- 理解有时很难推理；改用函数.
可能还有一种方法可以证明|S|== 50 更直接，通过引入一个函数 f(n)，该函数通过返回 set s | 来概括定义 S 的理解.0 <= s n 进行归纳来证明 |f(n)|== n，然后注意S == f(50).
这将是一个非常好的替代证明，我鼓励您尝试自己开发它.我在这里给出的证明的一个优点是它更通用(如果您经常操作集合，MapSet 和 RangeSet 通常很有用).>
Here's a simple Dafny program: two line of code and three assertions.
method Main()
{
var S := set s: int | 0 <= s < 50 :: 2 * s;
var T := set t | t in S && t < 25;
assert |S| == 50; // does not verify
assert T <= S; // does verify
assert T < S; // does not verify
}
The cardinality of S is 50, but Dafny can't verify this claim, as written. Similarly, T is obviously a subset of S, and Dafny can verify this claim; but T is also a proper subset of S, and Dafny cannot verify this claim.
What is going on "under the hood" that accounts for these difficulties, and might people who are learning and using Dafny anticipate and avoid, or deal with, such difficulties?
Dafny cannot verify the first assertion because Dafny has no built-in model for reasoning about the cardinality of set comprehensions. So it will never be able to prove equations like |S| == 50 on its own. It can, however, reason about cardinalities of some other set operations, such as union and singleton sets. You can use this to convince Dafny that |S| == 50 in a rather roundabout way, which I'll show below.
Dafny cannot prove the last assertion because it isn't smart enough to come up with an element of S that is not in T. We can help it out by mentioning such an element. More on that below.
Setting up appropriate triggers
But first, there is a warning about the set comprehension, saying that Dafny "cannot find any terms to trigger on". This has to do with how Dafny translates set comprehensions into first-order logic, using quantifiers. Dafny instructs Z3 to use certain syntactic patterns (called triggers) to reason about quantifiers, but this warning says that no such pattern could be found. This problem is not just abstract, Dafny has serious trouble reasoning about this comprehension: it cannot even prove 0 in S.
A fairly generic way of fixing such problems is to introduce a new function to abbreviate some portion of the formula that is useful as a trigger. Concretely, define
function method Double(n: int): int {
2 * n
}
and then rewrite the comprehension as
var S := set s: int | 0 <= s < 50 :: Double(s);
so that Dafny can use the trigger Double(s). Now, whenever you want to convince Dafny that something is in S, you can mention it as Double(x) for some x, and Dafny will be able to prove it.
For example, to show 0 in S under the new definition, we can say
assert Double(0) in S; // remove this to see the one below fail
assert 0 in S;
Proving T < S
So far all we've done is massage the program a little bit so that Dafny can better reason about S. This is already enough to fix the proof of your final assertion T < S, so let's look at that next.
Dafny understands T < S as (essentially) T <= S && T != S. You have already seen that it is able to show T <= S, so it remains to prove T != S. The easiest way to do that is to exhibit an element of one set that is not in the other, in this case, an element of S that is not in T. 26 is such an element, and we can fix the assertion by adding the line
assert Double(13) in S; // mention the trigger; this proves 26 in S
assert T < S; // now verifies
Proving |S| == 50
Finally, let's go back to your first failing assertion, that |S| == 50. This one is harder to fix. There might be a shorter proof, but I'll show you one way to do it that should also help you see how to fix similar problems on your own.
Our approach will be to first show that S can be expressed in terms of two simpler functions on sets, and then prove lemmas about how these two functions affect cardinalities.
Dafny is able to show
assert S == MapSet(Double, RangeSet(0, 50));
where RangeSet(a,b) is a function that constructs the set of integers between a and b, and MapSet is a function that "maps a function over a set". These functions are defined as follows:
function method RangeSet(a: int, b: int): set<int> {
set x: int | a <= x < b
}
function method MapSet<A,B>(f: A -> B, S: set<A>): set<B>
{
set x | x in S :: f(x)
}
So in order to prove something about |S|, it suffices to reason about the cardinality of RangeSet and to show that (under suitable conditions) MapSet preserves cardinality. Here are two lemmas to this effect
lemma CardRangeSet(a: int, b: int)
requires a <= b
decreases b - a
ensures |RangeSet(a, b)| == b - a
lemma CardMapSetInj<A, B>(f: A -> B, S: set<A>)
requires Injective(f)
decreases S
ensures |MapSet(f, S)| == |S|
CardRangeSet says that the cardinality of the set of numbers between a and b is b - a, which should be fairly intuitive, remembering that RangeSet is inclusive of a but exclusive of b.
The lemma CardMapSetInj says that injective functions preserve cardinality when mapped over a set. Note that Double is injective (Dafny thinks this is obvious -- it requires no proof). Also note that the injectivity assumption is necessary for the lemma to hold, otherwise mapping could decrease the cardinality if the function sends two elements of the input set to the same output element. We can define Injective as follows:
predicate Injective<A, B>(f: A -> B)
{
forall x, y :: x != y ==> f(x) != f(y)
}
I will prove the two lemmas below, but first let's see how to use them to finish showing |S| == 50.
assert S == MapSet(Double, RangeSet(0, 50));
CardMapSetInj(Double, RangeSet(0, 50));
assert |S| == |RangeSet(0, 50)|;
CardRangeSet(0, 50);
assert |S| == 50; // now verifies
Not too bad! We first call CardMapSet with Double to show that |S| == |RangeSet(0, 50)|. Then we call CardRangeSet to show |RangeSet(0, 50)| == 50, which finishes the proof.
The two lemmas are both proved by induction.
lemma CardRangeSet(a: int, b: int)
requires a <= b
decreases b - a
ensures |RangeSet(a, b)| == b - a
{
if a != b {
calc {
|RangeSet(a, b)|;
{ assert RangeSet(a, b) == {a} + RangeSet(a + 1, b); }
|{a} + RangeSet(a + 1, b)|;
1 + |RangeSet(a + 1, b)|;
{ CardRangeSet(a + 1, b); }
1 + (b - (a + 1));
b - a;
}
}
}
CardRangeSet is proved by induction on b - a. Dafny finds the base case trivial, so we consider only the induction step when a != b. The proof works by unrolling RangeSet to pull out the a, and then calling the induction hypothesis on (a + 1, b) and cleaning up.
(The proof is written in a calculational style. If you're not familiar with calc, it allows you to write a sequence of equations very succinctly and readbly. The lines surrounded in braces are proof annotations showing why the next line is equal to the previous. If no annotation is required, it can be omitted. Consult the Dafny manual for more details on calc.)
lemma CardMapSetInj<A, B>(f: A -> B, S: set<A>)
requires Injective(f)
decreases S
ensures |MapSet(f, S)| == |S|
{
if S != {} {
var x :| x in S;
calc {
|MapSet(f, S)|;
{ assert MapSet(f, S) == MapSet(f, {x} + (S - {x})) == {f(x)} + MapSet(f, S - {x}); }
|{f(x)} + MapSet(f, S - {x})|;
1 + |MapSet(f, S - {x})|;
{ CardMapSetInj(f, S - {x}); }
|S|;
}
}
}
CardMapSetInj is proved by induction on the argument set S. Again the base case is trivial and omitted. In the inductive step where S is nonempty, we select an arbitrary element x in S (such an x exists since S is nonempty). Then we can unroll the definition of MapSet on S and call the induction hypothesis on S - {x}.
(If you're not familiar with the syntax var x :| x in S, this is Dafny's "let such-that" statement. It is sort of similar to an assignment statement, except instead of assigning a particular value to x, it instead selects an arbitrary value that satisfies the predicate on the right-hand side of the :|. During verification, Dafny verifies that there exists such an element. The rest of the program knows nothing about the value of x except that it satisfies the predicate. See the Dafny reference for more details.)
Wrapping up
There are basically two ideas here:
- Introduce new functions to serve as triggers
- Comprehensions are sometimes hard to reason about; use functions instead.
There is also probably a way to prove |S| == 50 more directly, by introducing a function f(n) that generalizes the comprehension defining S by returning set s | 0 <= s < n :: Double(s). One could then proceed directly by induction on n to prove that |f(n)| == n, and then note that S == f(50).
That would be a perfectly fine alternative proof, and I encourage you to try to develop it yourself. One advantage of the proof I've given here is that it is more generic (MapSet and RangeSet are likely to be generally useful if you are frequently manipulating sets).
这篇关于为什么 Dafny 不能验证某些简单的集合基数和关系命题?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
