quicksort - 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?

Question

This is my first time asking a question on here, so I hope I have adequately followed the guidelines for asking a proper question.

For some quick context: I am currently trying to implement and verify a recursive version of Quicksort in Dafny. At this point, it seems that all there is left to do is to prove one last lemma (i.e., the implementation completely verifies when I remove this lemma's body. If I am not mistaking, this should mean that the implementation completely verifies when assuming this lemma holds.).

Specifically, this lemma states that, if a sequence of values is currently properly partitioned around a pivot, then, if one permutes the (sub)sequences left and right of the pivot, the complete sequence is still a valid partition. Eventually, using this lemma, I essentially want to say that, if the subsequences left and right of the pivot get sorted, the complete sequence is still a valid partition; as a result, the complete sequence is sorted.

Now, I have tried to prove this lemma, but I get stuck on the part where I try to show that, if all values in a sequence are less than some value, then all values in a permutation of that sequence are also less than that value. Of course, I also need to show the equivalent property with "less than" replaced by "greater than or equal to", but I suppose that they are nearly identical, so knowing one would be sufficient.

The relevant part of the code is given below:

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)
{

}

I've tried several things, such as:

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]);

However, here the second assertion already fails to verify.

After this first attempt, I figured that Dafny might not be able to verify this property between the sequences because the "Permutation" predicate uses the corresponding multisets instead of the sequences themselves. So, I tried to make the relation between the sequences more explicit by doing the following:

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]);

This all verifies, which I thought was great, since there only seems one step left to connect this to the definition of "Partitioned", viz.:

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

Nevertheless, Dafny then fails to verify this assertion.

So, at this point, I am not sure how to convince Dafny that this lemma holds. I've tried looking at implementations of Quicksort in Dafny from other people, as well as any potentially relevant question I could find. However, this has, as of yet, been to no avail. I hope someone could help me out here.

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

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.