Next permutation

next_permutations.dfy

include "./next_permutations_rank.dfy"

method copy (src: array<nat>, dest: array<nat>)
  modifies dest
  requires src.Length == dest.Length
  ensures forall i :: 0 <= i < src.Length ==> dest[i] == src[i]
{
  var i := 0;
  while i < src.Length
    decreases src.Length - i
    invariant 0 <= i <= src.Length
    invariant forall j :: 0 <= j < i ==> dest[j] == src[j]
  {
    dest[i] := src[i];
    i := i + 1;
  }
}

lemma {:induction a, b} seq_permutation_lemma (a: seq<nat>, b: seq<nat>)
  decreases a, b
  requires |a| == |b|
  requires forall i :: 0 <= i < |a| ==> a[i] == b[i]
  ensures forall i :: 0 <= i < |a| ==> exists j :: 0 <= j < |b| && a[i] == b[j]
{
  if |a| <= 0 {
  }
  else {
    assert a[0] == b[0];
    seq_permutation_lemma(a[1..], b[1..]);
  }
}

predicate decreasing (s: seq<nat>)
  decreases |s|
{
  if |s| <= 1 then true else (s[0] > s[1]) && decreasing (s[1..])
}

lemma {:induction s} decreasing_lemma (s: seq<nat>)
  requires ! decreasing(s)
  requires forall i, j :: 0 <= i < j < |s| ==> s[i] != s[j]
  ensures exists i :: 0 <= i < |s|-1 && s[i] < s[i+1]
{
}

lemma decreasing_seq_aux_lemma (e: nat, s: seq<nat>)
  requires forall i :: 0 <= i < |s| - 1 ==> s[i] > s[i+1]
  requires |s| > 0 ==> e < s[|s|-1]
  ensures forall i :: 0 <= i < |s| ==> e < s[i]
{
  if |s| > 0 {
    var i := |s| - 1;
    while i >= 0
      invariant forall k :: i < k < |s| && k >= 0 ==> e < s[k]
    {
      if i == |s| - 1 {
        assert e < s[|s|-1];
      }
      else {
        assert e < s[i+1];
        assert s[i+1] < s[i];
      }
      i := i - 1;
    }
  }
}


method find_indices (perm: array<nat>) returns (first_index: nat, second_index: nat)
  requires forall i, j :: 0 <= i < j < perm.Length ==> perm[i] != perm[j]
  requires ! decreasing (perm[0..])
  ensures 0 <= first_index < second_index < perm.Length
  ensures perm[first_index] < perm[second_index]
  ensures forall i :: 0 <= i < perm.Length - 1 && perm[i] < perm[i+1] ==> i <= first_index
  ensures forall i :: first_index < i < perm.Length && perm[first_index] < perm[i] ==> i <= second_index
  ensures forall i :: first_index < i < perm.Length - 1 ==> perm[i] > perm[i+1]
  ensures forall i :: first_index < i <= second_index ==> perm[first_index] < perm[i]
  ensures forall i :: second_index < i < perm.Length ==> perm[i] < perm[first_index]
{
  first_index := perm.Length;
  second_index := perm.Length;

  decreasing_lemma(perm[0..]);
  var first_index_proof :| 0 <= first_index_proof < perm.Length - 1 &&
    perm[first_index_proof] < perm[first_index_proof+1];

  ghost var possible_first_indices : seq<nat> := [];

  var i := 0;
  while i < perm.Length
    decreases perm.Length - i
    invariant 0 <= i <= perm.Length
    invariant forall m :: 0 <= m < i && m < perm.Length - 1 && perm[m] < perm[m+1] <==> m in possible_first_indices
    invariant forall m :: m in possible_first_indices ==> m <= first_index && m < i
    invariant first_index != perm.Length ==> first_index in possible_first_indices
    invariant i > first_index_proof ==> first_index < perm.Length - 1
  {
    if i < perm.Length - 1 && perm[i] < perm[i+1]
    {
      first_index := i;
      possible_first_indices := possible_first_indices + [first_index];
    }
    i := i + 1;
  }

  var second_index_proof :| first_index < second_index_proof && second_index_proof < perm.Length &&
    perm[first_index] < perm[second_index_proof];

  ghost var possible_second_indices : seq<nat> := [];

  i := first_index + 1;
  while i < perm.Length
    decreases perm.Length - i
    invariant first_index < i <= perm.Length
    invariant forall m :: first_index < m < i && perm[first_index] < perm[m] <==> m in possible_second_indices
    invariant forall m :: m in possible_second_indices ==> first_index < m <= second_index && m < i
    invariant second_index != perm.Length ==> second_index in possible_second_indices
    invariant i > second_index_proof ==> second_index < perm.Length
  {
    if perm[first_index] < perm[i]
    {
      second_index := i;
      possible_second_indices := possible_second_indices + [second_index];
    }
    i := i + 1;
  }
  decreasing_seq_aux_lemma(perm[first_index], perm[(first_index+1)..(second_index+1)]);
  forall k | first_index < k <= second_index ensures perm[first_index] < perm[k] {
      assert perm[first_index] < perm[k];
  }
}

method swap (a: array<nat>, m: nat, n: nat)
  modifies a
  requires 0 <= m < a.Length && 0 <= n < a.Length
  ensures a[m] == old(a[n]) && a[n] == old(a[m])
  ensures forall i :: 0 <= i < a.Length && i != m && i != n ==> a[i] == old(a[i])
{
    a[m], a[n] := a[n], a[m];
}

method reverse (a: array<nat>, m: nat, n:nat)
  modifies a
  requires 0 <= m <= n < a.Length
  ensures forall i :: 0 <= i < a.Length && ! (m <= i <= n) ==> a[i] == old(a[i])
  ensures forall i :: 0 <= i < a.Length && m <= i <= n ==> a[i] == old(a[m+n-i])
{

   var i := m;
   var j := n;

   while i <= j
    decreases j - i
    invariant m <= i <= n + 1 && m - 1 <= j <= n && i + j == m + n
    invariant forall k :: 0 <= k < a.Length && !(m <= k <= n) ==> a[k] == old(a[k])
    invariant forall k :: 0 <= k < a.Length && i <= k <= j ==> a[k] == old(a[k])
    invariant forall k :: 0 <= k < a.Length && m <= k < i ==> a[k] == old(a[m+n-k])
    invariant forall k :: 0 <= k < a.Length && j < k <= n ==> a[k] == old(a[m+n-k])
   {
      swap(a, i, j);
      i := i + 1;
      j := j - 1;
   }
}

method next_permutation (perm: array<nat>) returns (result: array<nat>)
  requires forall i, j :: 0 <= i < j < perm.Length ==> perm[i] != perm[j]
  requires ! decreasing(perm[0..])
  ensures result.Length == perm.Length
  ensures forall i :: 0 <= i < perm.Length ==> exists j :: 0 <= j < result.Length && perm[i] == result[j]
  ensures permutation_rank(result[0..]) - permutation_rank(perm[0..]) == 1
{
  var first_index, second_index := find_indices(perm);
  result := new nat[perm.Length];
  copy(perm, result);
  seq_permutation_lemma(perm[0..], result[0..]);

  swap(result, first_index, second_index);
  reverse(result, first_index+1, result.Length-1);

  assert perm.Length == result.Length;
  assert forall k :: 0 <= k && k < first_index ==> perm[k] == result[k];
  assert perm[first_index] == result[first_index + result.Length - second_index];
  assert perm[second_index] == result[first_index];
  assert forall k :: first_index < k < result.Length && k != second_index ==> perm[k] == result[first_index + result.Length - k];
  assert |perm[0..]| == perm.Length;
  assert |result[0..]| == result.Length;
  permutation_rank_difference_lemma(perm[0..], result[0..], first_index, second_index);
}

next_permutations_rank.dfy

function less_than_count (n: nat, s: seq<nat>) : nat
{
  if |s| == 0
  then 0
  else
    if s[0] < n
    then 1 + less_than_count(n, s[1..])
    else less_than_count(n, s[1..])
}

lemma {:induction a} less_than_count_append_lemma (e: nat, a: seq<nat>, b: seq<nat>)
  decreases a
  ensures less_than_count(e, a + b) == less_than_count(e, a) + less_than_count(e, b)
{
  if |a| == 0
  { assert a + b == b; }
  else
  {
    less_than_count_append_lemma(e, a[1..], b);
    calc == {
      less_than_count(e, a + b);
      if (a + b)[0] < e then 1 + less_than_count(e, (a + b)[1..]) else less_than_count(e, (a + b)[1..]);
      { assert (a + b)[0] == a[0]; assert (a + b)[1..] == a[1..] + b; }
      if a[0] < e then 1 + less_than_count(e, a[1..] + b) else less_than_count(e, a[1..] + b);
    }
  }
}

lemma {:induction false} less_than_count_aux_lemma (e: nat, a: seq<nat>, b: seq<nat>, idx: nat)
  requires |a| == |b| + 1
  requires 0 <= idx < |a|
  requires b == a[..idx] + a[(idx+1)..]
  ensures less_than_count(e, a) == if a[idx] < e then 1  + less_than_count(e, b) else less_than_count(e, b)
{
  calc == {
    less_than_count(e, a);
    { less_than_count_append_lemma(e, a[..idx], a[idx..]); assert a == a[..idx] + a[idx..]; }
    less_than_count(e, a[..idx]) + less_than_count(e, a[idx..]);
    { less_than_count_append_lemma(e, [a[idx]], a[(idx+1)..]); }
    less_than_count(e, a[..idx]) + less_than_count(e, [a[idx]]) + less_than_count(e, a[(idx+1)..]);
    less_than_count(e, [a[idx]]) + less_than_count(e, a[..idx]) + less_than_count(e, a[(idx+1)..]);
    { less_than_count_append_lemma(e, a[..idx], a[(idx+1)..]); assert b == a[..idx] + a[(idx+1)..]; }
    less_than_count(e, [a[idx]]) + less_than_count(e, b);
    if a[idx] < e then 1 + less_than_count(e, b) else less_than_count(e, b);
  }
}

lemma {:induction a, b} less_than_count_prefix_lemma (e: nat, n: nat, a: seq<nat>, b: seq<nat>)
  decreases a, b
  requires |a| == |b| && n <= |a|
  requires forall m :: 0 <= m < n ==> a[m] == b[m]
  requires forall j, k :: n <= j < k < |a| ==> a[j] != a[k]
  requires forall m :: n <= m < |a| ==> exists k :: n <= k < |b| && a[m] == b[k]
  ensures less_than_count(e, a) == less_than_count(e, b)
{
  if n == 0
  {
    if |a| <= 1 {}
    else
    {
      var j :| 0 <= j < |b| && b[j] == a[0];
      var nb := b[..j] + b[(j+1)..];
      forall m | 1 <= m < |a| ensures exists k :: 0 <= k < |nb| && a[m] == nb[k] {
        var l :| 0 <= l < |b| && l != j && b[l] == a[m];
        if l < j {
          assert b[l] == nb[l];
        }
        else {
          assert b[l] == nb[l-1];
        }
      }
      less_than_count_aux_lemma(e, b, nb, j);
      less_than_count_prefix_lemma(e, n, a[1..], nb);
    }
  }
  else {
    forall m | n-1 <= m < |a[1..]| ensures exists k :: n-1 <= k < |b[1..]| && a[1..][m] == b[1..][k]{
      assert a[1..][m] == a[m+1];
      var j :| n <= j < |b| && b[j] == a[m+1];
      assert b[j] == b[1..][j-1];
    }
    less_than_count_prefix_lemma(e, n-1, a[1..], b[1..]);
  }
}

lemma {:induction a} less_than_count_all_small (e: nat, a: seq<nat>)
  requires forall k :: 0 <= k < |a| ==> a[k] < e
  ensures less_than_count(e, a) == |a|
{}

lemma {:induction a} less_than_count_all_large (e: nat, a: seq<nat>)
  requires forall k :: 0 <= k < |a| ==> a[k] > e
  ensures less_than_count(e, a) == 0
{}

function factorial (n: nat) : nat
  decreases n
{
  if n == 0 then 1 else n * factorial (n-1)
}

function permutation_rank (perm: seq<nat>) : nat
  decreases |perm|
{
  if |perm| <= 1
    then 0
  else less_than_count(perm[0], perm[1..]) * factorial(|perm|-1) + permutation_rank(perm[1..])
}

lemma {:induction a, b, n} permutation_rank_prefix_lemma (a: seq<nat>, b: seq<nat>, n: nat)
  decreases a, b, n
  requires |a| == |b| && n <= |a|
  requires forall k :: 0 <= k < n ==> a[k] == b[k]
  requires forall k, l :: n <= k < l < |a| ==> a[k] != a[l]
  requires forall k :: n <= k < |a| ==> exists l :: n <= l < |b| && a[k] == b[l]
  ensures permutation_rank(b) - permutation_rank(a) == permutation_rank(b[n..]) - permutation_rank(a[n..])
{
  if n == 0 {
  }
  else {
    forall m | n-1 <= m < |a[1..]| ensures exists k :: n-1 <= k < |b[1..]| && a[1..][m] == b[1..][k]{
      assert a[1..][m] == a[m+1];
      var j :| n <= j < |b| && b[j] == a[m+1];
      assert b[j] == b[1..][j-1];
    }
    calc == {
      permutation_rank(b) - permutation_rank(a);

      less_than_count(b[0], b[1..]) * factorial(|b|-1) + permutation_rank(b[1..]) -
      less_than_count(a[0], a[1..]) * factorial(|a|-1) - permutation_rank(a[1..]);

      less_than_count(a[0], b[1..]) * factorial(|a|-1) + permutation_rank(b[1..]) -
      less_than_count(a[0], a[1..]) * factorial(|a|-1) - permutation_rank(a[1..]);

      { less_than_count_prefix_lemma(a[0], n-1, a[1..], b[1..]); }
      permutation_rank(b[1..]) - permutation_rank(a[1..]);
      { permutation_rank_prefix_lemma(a[1..], b[1..], n-1); }
      permutation_rank(b[n..]) - permutation_rank(a[n..]);
    }
  }
}

lemma {:induction a} increasing_less_than_count_lemma (n: nat, a: seq<nat>)
  requires |a| > 0 ==> n < a[0]
  requires forall k :: 0 <= k && k < |a|-1 ==> a[k] < a[k+1]
  ensures less_than_count(n, a) == 0
{}

lemma {:induction a} increasing_rank_lemma (a: seq<nat>)
  decreases a
  requires forall k :: 0 <= k < |a|-1 ==> a[k] < a[k+1]
  ensures permutation_rank(a) == 0
{
  if |a| <= 1{
  }
  else {
    calc == {
      permutation_rank(a);
      less_than_count(a[0], a[1..]) * factorial(|a|-1) + permutation_rank(a[1..]);
      { increasing_less_than_count_lemma(a[0], a[1..]); }
      permutation_rank(a[1..]);
      { increasing_rank_lemma(a[1..]); }
      0;
    }
  }
}

lemma {:induction a} decreasing_less_than_count_lemma (n: nat, a: seq<nat>)
  requires |a| > 0 ==> n > a[0]
  requires forall k :: 0 <= k < |a|- 1 ==> a[k] > a[k+1]
  ensures less_than_count(n, a) == |a|
{}

lemma {:induction a} decreasing_rank_lemma (a: seq<nat>)
  decreases a
  requires forall k :: 0 <= k < |a|-1 ==> a[k] > a[k+1]
  ensures permutation_rank(a) == factorial(|a|) - 1
{
  if |a| <= 1 {

  }
  else {
    calc == {
      permutation_rank(a);
      less_than_count(a[0], a[1..]) * factorial(|a|-1) + permutation_rank(a[1..]);
      { decreasing_less_than_count_lemma(a[0], a[1..]); }
      (|a|-1) * factorial(|a|-1) + permutation_rank(a[1..]);
      { decreasing_rank_lemma(a[1..]); }
      (|a|-1) * factorial(|a|-1) + factorial(|a|-1) - 1;
      |a| * factorial(|a|-1) - factorial(|a|-1) + factorial(|a|-1) - 1;
      |a| * factorial(|a|-1) - 1;
      factorial(|a|) - 1;
    }
  }
}

lemma decreasing_seq_lemma (idx: nat, s: seq<nat>)
  requires forall i :: 0 <= i < |s| - 1 ==> s[i] > s[i+1]
  requires 0 <= idx < |s|
  ensures forall i :: 0 <= i < idx ==> s[i] > s[idx]
  ensures forall i :: idx < i < |s| ==> s[idx] > s[i]
{
  var i := idx - 1;
  while i >= 0
    invariant -1 <= i < idx
    invariant forall k :: i < k < idx ==> s[k] > s[idx]
  {
    if i == idx - 1 {
      assert s[i] > s[idx];
    }
    else {
      assert s[i] > s[i+1];
      assert s[i+1] > s[idx];
    }
    i := i - 1;
  }
  i := idx + 1;
  while i < |s|
    invariant idx < i <= |s|
    invariant forall k :: idx < k < i ==> s[idx] > s[k]
  {
    if i == idx + 1 {
      assert s[idx] > s[i];
    }
    else {
      assert s[idx] > s[i-1];
      assert s[i-1] > s[i];
    }
    i := i + 1;
  }
}


lemma {:induction a, b} permutation_rank_difference_lemma (a: seq<nat>, b: seq<nat>, first_index: nat, second_index: nat)
requires |a| == |b|
requires 0 <= first_index < second_index < |a|
requires forall k, l :: 0 <= k < l < |a| ==> a[k] != a[l]
requires forall k :: 0 <= k < |a| ==> exists l :: 0 <= l < |b| && a[k] == b[l]
requires forall k :: 0 <= k < first_index ==> a[k] == b[k]
requires a[first_index] == b[first_index + |a| - second_index]
requires forall k :: first_index < k < |a| && k != second_index ==> a[k] == b[first_index + |a| - k]
requires a[second_index] == b[first_index]
requires forall k :: first_index < k < |a| - 1 ==> a[k] > a[k+1]
requires forall k :: first_index < k <= second_index ==> a[first_index] < a[k]
requires forall k :: second_index < k < |a| ==> a[k] < a[first_index]
ensures permutation_rank(b) - permutation_rank(a) == 1
{
  decreasing_seq_lemma (second_index - (first_index+1), a[(first_index+1)..]);
  assert forall k :: first_index < k < second_index ==> a[k] > a[second_index];
  assert forall k :: second_index < k < |a| ==> a[second_index] > a[k];

  forall k | first_index < k < |b| - 1 ensures b[k] < b[k+1]
   {
    if k != first_index + |a| - second_index {
      assert b[k] == a[first_index + |a| - k];
      if k + 1 == first_index + |a| - second_index {
        assert b[k+1] == a[first_index];
        assert a[first_index + |a| - k] < a[first_index];
      }
      else {
        assert b[k+1] == a[first_index + |a| - k - 1];
        assert a[first_index + |a| - k] < a[first_index + |a| - k - 1];
      }
    }
    else {
      assert b[k] == a[first_index];
      assert b[k+1] == a[first_index + |a| - (k+1)];
      assert a[first_index] < a[first_index + |a| - (k+1)];
    }
   }

  forall k | first_index < k <= first_index + |a| - second_index ensures b[first_index] > b[k]
   {
      assert b[first_index] == a[second_index];
      if (k == first_index + |a| - second_index)
      {
        assert b[k] == a[first_index];
        assert a[first_index] < a[second_index];
      }
      else {
        assert b[k] == a[first_index + |a| - k];
        assert a[second_index] > a[first_index + |a| - k];
      }
   }

  forall k | first_index + |a| - second_index < k < |b| ensures b[first_index] < b[k]
   {
      assert b[first_index] == a[second_index];
      assert b[k] == a[first_index + |a| - k];
      assert a[first_index + |a| - k] > a[second_index];
   }

  calc == {
    less_than_count(b[first_index], b[(first_index+1)..]) -
    less_than_count(a[first_index], a[(first_index+1)..]);

    {
      assert a[(first_index+1)..] == a[(first_index+1)..(second_index+1)] + a[(second_index+1)..];
      less_than_count_append_lemma(a[first_index], a[(first_index+1)..(second_index+1)], a[second_index+1..]);
    }

    less_than_count(b[first_index], b[(first_index+1)..]) -
    less_than_count(a[first_index], a[(first_index+1)..(second_index+1)])-
    less_than_count(a[first_index], a[(second_index+1)..]);

    {
      less_than_count_all_large(a[first_index], a[(first_index+1)..(second_index+1)]);
      less_than_count_all_small(a[first_index], a[(second_index+1)..]);
      assert |a[(second_index+1)..]| == |a| - second_index - 1;
    }

    less_than_count(b[first_index], b[(first_index+1)..]) - (0 + |a| - second_index - 1);

    {
      assert b[(first_index+1)..] == b[(first_index+1)..(first_index+|a|-second_index+1)] + b[(first_index+|a|-second_index+1)..];
      less_than_count_append_lemma(b[first_index], b[(first_index+1)..(first_index+|a|-second_index+1)], b[(first_index+|a|-second_index+1)..]);
    }

    less_than_count(b[first_index], b[(first_index+1)..(first_index+|a|-second_index+1)]) +
    less_than_count(b[first_index], b[(first_index+|a|-second_index+1)..]) -
    (0 + |a| - second_index - 1);

    {
      less_than_count_all_small(b[first_index], b[(first_index+1)..(first_index+|a|-second_index+1)]);
      less_than_count_all_large(b[first_index], b[(first_index+|a|-second_index+1)..]);
      assert |a| == |b|;
    }

    (|a| - second_index) - (0 + |a| - second_index - 1);
    1;
  }

  assert less_than_count(b[first_index], b[(first_index+1)..]) - less_than_count(a[first_index], a[(first_index+1)..]) == 1;

  calc == {

    permutation_rank(b) - permutation_rank(a);

    { permutation_rank_prefix_lemma(a, b, first_index); }

    permutation_rank(b[first_index..]) - permutation_rank(a[first_index..]);

    less_than_count(b[first_index], b[(first_index+1)..]) * factorial(|b[first_index..]|-1) +
    permutation_rank(b[(first_index+1)..]) -
    less_than_count(a[first_index], a[(first_index+1)..]) * factorial(|a[first_index..]|-1) -
    permutation_rank(a[(first_index+1)..]);

    { decreasing_rank_lemma(a[(first_index+1)..]); increasing_rank_lemma(b[(first_index+1)..]); }

    less_than_count(b[first_index], b[(first_index+1)..]) * factorial(|b[first_index..]|-1) -
    less_than_count(a[first_index], a[(first_index+1)..]) * factorial(|a[first_index..]|-1) -
    factorial(|a[(first_index+1)..]|) + 1;

    { assert factorial(|b[first_index..]|) == factorial(|a[first_index..]|); }

    less_than_count(b[first_index], b[(first_index+1)..]) * factorial(|a[first_index..]|-1) -
    less_than_count(a[first_index], a[(first_index+1)..]) * factorial(|a[first_index..]|-1) -
    factorial(|a[(first_index+1)..]|) + 1;

    (less_than_count(b[first_index], b[(first_index+1)..]) - less_than_count(a[first_index], a[(first_index+1)..])) *
    factorial(|a[first_index..]|-1) - factorial(|a[(first_index+1)..]|) + 1;

    factorial(|a[first_index..]|-1) - factorial(|a[(first_index+1)..]|) + 1;

    1;
  }
}