Как в Дафни утверждать, что если все элементы в последовательности меньше некоторого значения, то это же верно и для перестановки этой последовательности?

Это мой первый раз, когда я задаю вопрос здесь, поэтому я надеюсь, что я правильно следовал правилам, чтобы задать правильный вопрос.

Для краткого контекста: в настоящее время я пытаюсь реализовать и проверить рекурсивную версию Quicksort в Dafny. На данный момент кажется, что все, что осталось сделать, это доказать одну последнюю лемму (т. е. реализация полностью проверяет, когда я удаляю тело этой леммы. Если я не ошибаюсь, это должно означать, что реализация полностью проверяет при допущении этого лемма верна).

В частности, эта лемма утверждает, что если последовательность значений в настоящее время правильно разделена вокруг опорной точки, то, если кто-то переставляет (под)последовательности слева и справа от опорной точки, полная последовательность все еще является допустимым разделением. В конце концов, используя эту лемму, я, по сути, хочу сказать, что если подпоследовательности слева и справа от опорной точки отсортированы, полная последовательность все еще является допустимым разбиением; в результате сортируется вся последовательность.

Теперь я попытался доказать эту лемму, но я застрял на той части, где пытаюсь показать, что если все значения в последовательности меньше некоторого значения, то все значения в перестановке этой последовательности также меньше этого ценить. Конечно, мне также нужно показать эквивалентное свойство с заменой «меньше чем» на «больше или равно», но я полагаю, что они почти идентичны, поэтому одного знания будет достаточно.

Соответствующая часть кода приведена ниже:

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

Однако здесь второе утверждение уже не проверяется.

После этой первой попытки я решил, что Дафни не сможет проверить это свойство между последовательностями, потому что предикат «Перестановка» использует соответствующие мультимножества вместо самих последовательностей. Итак, я попытался сделать связь между последовательностями более явной, выполнив следующие действия:

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

Тем не менее, Дафни не может проверить это утверждение.

Итак, на данный момент я не знаю, как убедить Дафни в справедливости этой леммы. Я пытался посмотреть на реализации Quicksort в Dafny от других людей, а также на любой потенциально важный вопрос, который я мог найти. Однако пока это ни к чему не привело. Я надеюсь, что кто-то может помочь мне здесь.

Приношу свои извинения за возможное невежество в отношении Дафни, я только начинаю изучать язык.