Precondition of merge sort too strong

[RustanLeino]

Dafny version

4.6.0

Problem

The MergeSortBy function in the standard library uses TotalOrdering(lessThanOrEq) as a precondition. Consequently, the ordering must depend on every part of the items being sorted. Unfortunately, this rules out the useful case of using a sort key that is only part of the items being sorted.

Remedy

The antisymmetry conjunct of the precondition should be removed.

Note, antisymmetry is still needed to prove lemma SortedUnique, unless its precondition multiset(xs) == multiset(ys) is strengthened to say a stable sort was applied (cf. Section 8.0.2 of Program Proofs).