在 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 可能无法在序列之间验证此属性，因为“排列”谓词使用相应的多重集而不是序列本身。因此，我试图通过执行以下操作使序列之间的关系更加明确：

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 相信这个引理成立。我已经尝试从其他人那里查看 Dafny 中 Quicksort 的实现，以及我能找到的任何可能相关的问题。然而，到目前为止，这仍然无济于事。我希望有人能帮助我。

对于对 Dafny 的任何潜在无知，我深表歉意，我才刚刚开始学习这门语言。

Answer 1

很难给出“排列”的可用定义。然而，要证明排序算法的正确性，只需要 元素的多重集 保持不变即可。对于序列 s，表达式 multiset(s) 给出了 s 的元素的多重集。如果你从一个数组 a 开始，那么 a[..] 给你一个由数组元素组成的序列，所以 multiset(a[..]) 给你数组中元素的多重集。

有关示例，请参阅 https://github.com/dafny-lang/dafny/blob/master/Test/dafny3/GenericSort.dfy#L59。

Dafny 的验证器无法自行计算出此类多重集的所有属性。然而，当你交换两个元素时，它通常会理解元素的多重集是不变的。

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

In Dafny, how to assert that, if all elements in a sequence are less than some value, this also holds for a permutation of this sequence?

partitioning

permutation

quicksort

dafny