Reverse Involution in Dafny

[EmilyOng]

Prove that reverse(reverse(lst)) == lst

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 append<T>(xs: List<T>, ys: List<T>): List<T>
ensures length(xs) + length(ys) == length(append(xs, ys))
{
    match xs {
        case Nil => ys
        case Cons(x, xs') => Cons(x, append(xs', ys))
    }
}

lemma AppendNilLemma<T>(xs: List<T>)
ensures append(Nil, xs) == xs
ensures append(xs, Nil) == xs
{}

lemma AppendAssociativeLemma<T>(xs: List<T>, ys: List<T>, zs: List<T>)
ensures append(xs, append(ys, zs)) == append(append(xs, ys), zs)
{}

function reverse<T>(lst: List<T>): List<T>
ensures length(lst) == length(reverse(lst))
{
    match lst {
        case Nil => Nil
        case Cons(x, xs) => append(reverse(xs), Cons(x, Nil))
    }
}

// Write induction:false to make the use explicit in the proof
lemma {:induction false} ReverseDistributesOverAppendLemma<T>(xs: List<T>, ys: List<T>)
ensures reverse(append(xs, ys)) == append(reverse(ys), reverse(xs))
{
    var LHS := reverse(append(xs, ys));
    var RHS := append(reverse(ys), reverse(xs));

    match xs
    case Nil =>
        // LHS
        // == reverse(append(Nil, ys)) (by substitution)
        // == reverse(ys) (by AppendNilLemma)
        // == append(reverse(ys), Nil) (by AppendNilLemma)
        // == RHS

        AppendNilLemma(ys);
        AppendNilLemma(reverse(ys));
        assert LHS == RHS;
    case Cons(x, xs') =>
        // LHS
        // == reverse(append(xs, ys))
        // == reverse(append(Cons(x, xs'), ys)) (by substitution)
        // == reverse(Cons(x, append(xs', ys))) (by rewriting)
        // == append(reverse(append(xs', ys)), Cons(x, Nil)) (by rewriting)
        // == append(append(reverse(ys), reverse(xs')), Cons(x, Nil)) (by induction hypothesis)
        // == append(reverse(ys), append(reverse(xs'), Cons(x, Nil))) (by AppendAssociativeLemma)
        // == append(reverse(ys), reverse(xs)) (by rewriting)
        // == RHS

        ReverseDistributesOverAppendLemma(xs', ys);
        AppendAssociativeLemma(reverse(ys), reverse(xs'), Cons(x, Nil));

        assert LHS == RHS;
}

function reverseReverse<T>(lst: List<T>): List<T>
ensures length(lst) == length(reverseReverse(lst))
{
    reverse(reverse(lst))
}

lemma {:induction false} reverseInvolutionLemma<T>(lst: List<T>)
ensures reverseReverse(lst) == lst
{
    var LHS := reverseReverse(lst);
    var RHS := lst;
    match lst {
        case Nil => assert LHS == RHS;
        case Cons(x, xs) =>
            // LHS
            // == reverse(reverse(Cons(x, xs))) (by substitution)
            // == reverse(reverse(append(Cons(x, Nil), xs))) (by rewriting)
            // == reverse(append(reverse(xs), Cons(x, Nil))) (by rewriting)
            // == append(reverse(Cons(x, Nil)), reverse(reverse(xs))) (by ReverseDistributesOverAppendLemma)
            // == append(Cons(x, Nil), reverse(reverse(xs))) (by rewriting)
            // == append(Cons(x, Nil), xs) (by induction hypothesis)
            // == Cons(x, xs)
            // == lst
            // == RHS

            ReverseDistributesOverAppendLemma(reverse(xs), Cons(x, Nil));
            reverseInvolutionLemma(xs);
            assert LHS == RHS;
    }
}