permutation - 在 Dafny 中，如何断言，如果序列中的所有元素都小于某个值，那么这也适用于该序列的排列？

Question

这是我第一次在这里提问，所以我希望我已经充分遵循了提出正确问题的指导方针。

对于一些快速的上下文：我目前正在尝试在 Dafny 中实现和验证 Quicksort 的递归版本。在这一点上，似乎剩下要做的就是证明最后一个引理（即，当我删除这个引理的主体时，实现完全验证。如果我没记错的话，这应该意味着实现在假设这一点时完全验证引理成立。）。

具体来说，这个引理指出，如果一个值序列当前围绕一个枢轴正确分区，那么，如果对枢轴的左右（子）序列进行置换，则完整序列仍然是有效分区。最后，使用这个引理，我基本上想说，如果枢轴的左右子序列被排序，完整的序列仍然是一个有效的分区；结果，完整的序列被排序。

现在，我试图证明这个引理，但我卡在我试图证明的部分，如果一个序列中的所有值都小于某个值，那么该序列的排列中的所有值也都小于那个价值。当然，我还需要用“大于或等于”代替“小于”来显示等效属性，但我认为它们几乎相同，所以知道一个就足够了。

代码的相关部分如下：

predicate Permutation(a: seq<int>, b: seq<int>)
    requires 0 <= |a| == |b|
{
    multiset(a) == multiset(b)
}

predicate Partitioned(a: seq<int>, lo: int, hi: int, pivotIndex: int)
    requires 0 <= lo <= pivotIndex < hi <= |a|
{
    (forall k :: lo <= k < pivotIndex ==> a[k] < a[pivotIndex])
    &&
    (forall k :: pivotIndex <= k < hi ==> a[k] >= a[pivotIndex])
}

lemma PermutationPreservesPartition(apre: seq<int>, apost: seq<int>, lo: int, hi: int, pivotIndex: int)
    requires 0 <= lo <= pivotIndex < hi <= |apre| == |apost|
    requires Partitioned(apre, lo, hi, pivotIndex)
    requires Permutation(apre[lo..pivotIndex], apost[lo..pivotIndex])
    requires Permutation(apre[pivotIndex + 1..hi], apost[pivotIndex + 1..hi])
    requires apre[pivotIndex] == apost[pivotIndex]

    ensures Partitioned(apost, lo, hi, pivotIndex)
{

}

我尝试了几件事，例如：

assert
Partitioned(apre, lo, hi, pivotIndex) && apre[pivotIndex] == apost[pivotIndex]
==>
(
    (forall k :: lo <= k < pivotIndex ==> apre[k] < apost[pivotIndex])
    &&
    (forall k :: pivotIndex <= k < hi ==> apre[k] >= apost[pivotIndex])
);

assert
(forall k :: lo <= k < pivotIndex ==> apre[k] < apost[pivotIndex])
&&
(Permutation(apre[lo..pivotIndex], apost[lo..pivotIndex]))
==>
(forall k :: lo <= k < pivotIndex ==> apost[k] < apost[pivotIndex]);

但是，这里的第二个断言已经无法验证。

在第一次尝试之后，我认为 Dafny 可能无法验证序列之间的这个属性，因为“Permutation”谓词使用相应的多重集而不是序列本身。因此，我尝试通过执行以下操作使序列之间的关系更加明确：

assert 
Permutation(apre[lo..pivotIndex], apost[lo..pivotIndex])
==>
forall v :: v in multiset(apre[lo..pivotIndex]) <==> v in multiset(apost[lo..pivotIndex]);

assert
forall v :: v in multiset(apre[lo..pivotIndex]) <==> v in apre[lo..pivotIndex];

assert
forall v :: v in multiset(apost[lo..pivotIndex]) <==> v in apost[lo..pivotIndex];

assert
forall v :: v in apre[lo..pivotIndex] <==> v in apost[lo..pivotIndex];

assert
(
    (forall v :: v in apre[lo..pivotIndex] <==> v in apost[lo..pivotIndex]) 
    &&
    (forall v :: v in apre[lo..pivotIndex] ==> v < apre[pivotIndex])
)
==>
(forall v :: v in apost[lo..pivotIndex] ==> v < apre[pivotIndex]);

assert
(
    (forall v :: v in apost[lo..pivotIndex] ==> v < apre[pivotIndex])
    &&
    apre[pivotIndex] == apost[pivotIndex]
)
==>
(forall v :: v in apost[lo..pivotIndex] ==> v < apost[pivotIndex]);

这一切都验证了，我认为这很好，因为似乎只剩下一步可以将其与“分区”的定义联系起来，即：

assert
(forall v :: v in apost[lo..pivotIndex] ==> v < apost[pivotIndex])
==>
(forall k :: lo <= k < pivotIndex ==> apost[k] < apost[pivotIndex]);

然而，达夫尼随后未能验证这一说法。

所以，在这一点上，我不确定如何让 Dafny 相信这个引理成立。我尝试从其他人那里查看 Dafny 中 Quicksort 的实现，以及我能找到的任何潜在相关问题。然而，到目前为止，这一切都无济于事。我希望有人可以在这里帮助我。

My apologies for any potential ignorance regarding Dafny, I am just starting out with the language.

标签： permutationquicksortpartitioningdafny

Answer 1

It is difficult to give a usable definition of "permutation". However, to prove the correctness of a sorting algorithm, you only need that the multiset of elements stays the same. For a sequence s, the expression multiset(s) gives you the multiset of elements of s. If you start with an array a, then a[..] gives you a sequence consisting of the elements of the array, so multiset(a[..]) gives you the multiset of elements in the array.

See https://github.com/dafny-lang/dafny/blob/master/Test/dafny3/GenericSort.dfy#L59 for an example.

Dafny's verifier cannot work out all properties of such multisets by itself. However, it generally does understand that the multiset of elements is unchanged when you swap two elements.