permutations.dfy

least predicate perm<T(!new)>(p: seq<T>, q: seq<T>)
{
  || (p == [] && q == [])
  || (exists x: T, m: seq<T>, n: seq<T> :: p == [x] + m && q == [x] + n && perm(m, n))
  || (exists x: T, y: T, m: seq<T> :: p == [x, y] + m && q == [y, x] + m)
  || (exists m: seq<T> :: perm(p, m) && perm(m, q))
}

lemma refl<T(!new)>(p: seq<T>)
  ensures perm(p, p)
{
  if p == [] {}
  else {
    assert p == [p[0]] + p[1..];
    refl(p[1..]);
  }
}

least lemma symm<T(!new)>(p: seq<T>, q: seq<T>)
  requires perm(p, q)
  ensures perm(q, p)
{}

lemma comm<T(!new)>(p: seq<T>, q: seq<T>, r: seq<T>)
  requires perm(p, q)
  requires perm(q, r)
  ensures perm(p, r)
{}

function permToMultiSet<T(!new)>(p: seq<T>) : multiset<T>
{
  if p == [] then multiset({})
  else multiset({p[0]}) + permToMultiSet(p[1..])
}

least lemma subset<T(!new)>(p: seq<T>, q: seq<T>)
  requires perm(p, q)
  ensures forall x :: x in permToMultiSet(p) ==> x in permToMultiSet(q)
{
   if p == [] && q == [] {}
   else {
     if (exists x, m, n :: p == [x] + m && q == [x] + n && perm(m, n)) {
        var x, m, n :| p == [x] + m && q == [x] + n && perm(m, n);
        subset(m, n);
     }
  }
}

lemma perm_cons<T(!new)>(p: seq<T>, q: seq<T>, t: T)
  requires perm(p, q)
  ensures perm([t] + p, [t] + q)
{}

lemma perm_prepend_left<T(!new)>(p: seq<T>, q: seq<T>, t: seq<T>)
  decreases |t|
  requires perm(p, q)
  ensures perm(t + p, t + q)
{
  if t == [] {
     assert t + p == p;
     assert t + q == q;
  }
  else {
    var ln, hd := |t|, t[0..|t|-1];
    assert t == hd + [t[ln-1]];
    assert t + p == hd + ([t[ln-1]] + p);
    assert t + q == hd + ([t[ln-1]] + q);
    perm_cons(p, q, t[ln-1]);
    perm_prepend_left([t[ln-1]] + p, [t[ln-1]] + q, hd);
  }
}

lemma perm_swap<T>(x: T, y: T, t: seq<T>)
  ensures perm([x, y] + t, [y, x] + t)
{}

least lemma perm_snoc<T(!new)>(p: seq<T>, q: seq<T>, t: T)
  requires perm(p, q)
  ensures perm(p + [t], q + [t])
{
  if p == [] && q == [] {
    assert p + [t] == [t];
    assert q + [t] == [t];
    refl([t]);
  }
  else {
    if (exists x, m, n :: p == [x] + m && q == [x] + n && perm(m, n))
    {
      var x, m, n :| p == [x] + m && q == [x] + n && perm(m, n);
      perm_snoc(m, n, t);
      perm_cons(m + [t], n + [t], x);
    }
    else {
      if (exists x, y, m :: p == [x, y] + m && q == [y, x] + m) {
       var x, y, m :| p == [x, y] + m && q == [y, x] + m;
       var lt := m + [t];
       perm_swap(x, y, lt);
     }
    }
  }
}

lemma aux_append_lemma<T>(p: seq<T>, q: seq<T>)
  requires |q| >= 1
  ensures p + q == p + [q[0]] + q[1..]
{
  if p == [] {}
  else {
     aux_append_lemma(p[1..], q);
     assert p + q == [p[0]] + p[1..] + q;
  }
}

lemma perm_append_right<T(!new)>(p: seq<T>, q: seq<T>, t: seq<T>)
  decreases |t|
  requires perm(p, q)
  ensures perm(p + t, q + t)
{
  if t == [] {
     assert p + t == p;
     assert q + t == q;
  }
  else {
    perm_snoc(p, q, t[0]);
    perm_append_right(p + [t[0]], q + [t[0]], t[1..]);
    aux_append_lemma(p, t);
    aux_append_lemma(q, t);
  }
}