Defining Unique Sorted Permutations in Dafny

First, we can define sorted sequences as a predicate. This simply defines the pairwise less-than-or-equal comparison between two elements in the sequence.

predicate SortedSeq(s: seq<int>)
{
  forall i, j :: 0 <= i < j < |s| ==> s[i] <= s[j]
}

However, this allows duplicate elements in a sequence. Instead, we can define a strict order, which tightens the comparison in the predicate:

predicate StrictOrderSortedSeq(s: seq<int>)
{
  forall i, j :: 0 <= i < j < |s| ==> s[i] < s[j]
}

This is the definition of sortedness we'll use, as permutations do not contain duplicate elements.

A permutation of length n contains elements from 0 to n - 1 (yes, we're starting the count from 0). We won't define permutations in Dafny, because we're only concerned with sorted permutations. There really is only one permutation that is sorted, and that is by mapping each index to itself in the sequence:

predicate ValidSortedPerm(s: seq<nat>) {
  forall i :: 0 <= i < |s| ==> s[i] == i
}

With that, we can generate the sequence of sorted permutations of length n, by using Dafny's sequence comprehension. The second argument i ⇒ i is just the identity function, as we're mapping the index to itself. Note that Dafny uses zero-based indexing!

function SortedSeqPerm(n: nat): seq<nat>
  ensures var s := SortedSeqPerm(n);
          ValidSortedPerm(s) && StrictOrderSortedSeq(s)
{
  seq(n, i => i)
}

We'll make use of a proof by contradiction in the main proof below. A template for doing that in Dafny, as suggested here, structures the proof around precondition P and postcondition Q:

lemma L(...)
  requires P
  ensures Q
{
  if !Q {
    ...
    assert !P;
    assert false;
  }
}

Here, we suppose that Q doesn't hold, and from that we can show that !P, essentially contradicting the precondition. The assert false is not necessary but it makes it clear that this is a proof by contradiction¹.

Let's begin by outlining a proof sketch. As a reminder, our proof conditions are follows:

• PRE1: We have a sequence sorted in strict order: StrictOrderSortedSeq(s) holds.
• PRE2: Our sequence has elements from 0 to n - 1.
• PRE3: This also implies the length of the sequence is equal to n: |s| == n holds.
• POST1: From the above conditions, we want to deduce that s == [0, 1, .. n - 1]: that is, s == SortedSeqPerm(n) holds.

For PRE2, we'll define an auxiliary lemma in Dafny:

lemma MembershipOfSortedSeqPerm(n: nat)
  ensures var s := SortedSeqPerm(n);
          forall i :: 0 <= i < n ==> i in s
{
  var s := SortedSeqPerm(n);
  forall i | 0 <= i < n
    ensures i in s
  {
    assert s[i] == i;
  }
}

This makes use of Dafny's aggregate statement, with the forall quantifier. The given ensures clause states that all elements 0 ≤ i < n would be in the sequence. In the body, we simply assert that the index is mapped to itself in the sequence s[i] == i, thus proving the postcondition.

This may seem obvious, but recall that SortedSeqPerm was defined by sequence comprehension, so Dafny doesn't attempt to infer the elements of the sequence automatically without invoking this lemma.

Now, our proof proceeds as follows.

1. We case-analyze the length of the sequence. If n <= 1, the conclusion holds trivially.
2. Otherwise, we further perform case-analysis on the last element of the sequence, s[n - 1]. We know that if it is equal to n - 1, then we know that by induction on the remaining sequence, the conclusion holds.
3. What if it's not equal to n - 1? We should be able to derive a contradiction. We know from PRE2 that s[n - 1] must be an element from 0 to n - 2, that is, s[n - 1] ≤ n - 2. This follows the proof-by-contradiction template, since s[n - 1] != n - 1 implies the negation of POST1
4. • We can still invoke the induction hypothesis on the remaining sequence, since the choice of the element in s[n - 1] does not violate any conditions on s[..n - 1].
   • From the induction hypothesis, we know n - 2 must be in s[..n - 1]
5. We derive a contradiction from (4), thus completing our proof.

The description above is translated into the Dafny code below, where a relevant line of code is annotated with the corresponding number in the description above:

lemma StrictOrderingPerm(n: nat, s: seq<nat>)
  requires StrictOrderSortedSeq(s) // PRE1
  requires forall i :: 0 <= i < n ==> 0 <= s[i] < n // PRE2
  requires n == |s| // PRE3
  ensures s == SortedSeqPerm(n) // POST1
{
  if n <= 1 {} // (1)
  else {
    if s[n - 1] == n - 1 { // (2)
      StrictOrderingPerm(n - 1, s[..n - 1]);
      assert s == SortedSeqPerm(n);
    } else { // (3)
      StrictOrderingPerm(n - 1, s[..n - 1]); // (4)
      // This ensures that s[i] == i in the remaining sequence
      MembershipOfSortedSeqPerm(n - 1);
      assert s[n - 1] <= n - 2; // (3)
      assert n - 2 in s[..n - 1]; // (4)
      assert !StrictOrderSortedSeq(s); // (5)
      assert false;
    }
  }
}

As with non-trivial proofs in Dafny (and most other proof languages out there), we need to make explicit some facts we think should hold trivially, especially for sequences (and other container types in general). Here, I would say that precondition PRE2, that is ∀ i ∙ 0 ≤ i < n ⇒ 0 ≤ s[i] < n, and the auxiliary lemma MembershipOfSortedPerm were facts that we could take for granted by the definition of a sorted permutation.

Being able to prove lemmas by contradiction is nice to know :)