Take-Skip in Dafny

[EmilyOng]

We reason about the length properties of Take and Skip and that the result is a subsequence of the original list.

datatype List<T> = Nil | Cons(head: T, tail: List<T>)

function length<T>(xs: List<T>): nat
{
    match xs {
        case Nil => 0
        case Cons(_, ys) => 1 + length(ys)
    }
}

function subsequence<T(==)> (sub: List<T>, xs: List<T>): bool
ensures subsequence(sub, xs) ==> length(sub) <= length(xs)
{
    match sub {
        case Nil => true
        case Cons(y, ys1) => match xs {
            case Nil => false
            case Cons(x, xs1) => if x == y && subsequence(ys1, xs1) then true else subsequence(sub, xs1)
        }
    }
}

lemma TrivialSubsequenceLemma<T>(xs: List<T>)
ensures subsequence(Nil, xs)
ensures subsequence(xs, xs)
{
}

function Take<T>(n: nat, xs: List<T>): List<T>
ensures length(xs) >= n ==> length(Take(n, xs)) == n && subsequence(Take(n, xs), xs)
ensures length(xs) < n ==> length(Take(n, xs)) == length(xs) && Take(n, xs) == xs
{
    if n == 0 then Nil
    else match xs {
        case Nil => Nil
        case Cons(x, xs1) =>
            var v := Take(n - 1, xs1);
            Cons(x, v)
    }
}

function Skip<T>(n: nat, xs: List<T>): List<T>
ensures length(xs) >= n ==> length(Skip(n, xs)) == length(xs) - n && subsequence(Skip(n, xs), xs)
ensures length(xs) < n ==> length(Skip(n, xs)) == 0 && Skip(n, xs) == Nil
{
    TrivialSubsequenceLemma(xs);
    if n == 0 then xs
    else match xs {
        case Nil => Nil
        case Cons(x, xs1) =>
            Skip(n - 1, xs1)
    }
}

function TakeSkip<T>(n: nat, xs: List<T>): List<T>
ensures length(TakeSkip(n, xs)) == 0
{
    var ys := Take(n, xs);
    var ws := Skip(n, ys);
    ws
}