
Dafny beginner here, and I'm struggling with what I assume is a simple proof.
If I define a sequence filtering function as follows:
function method filter<T>(xs: seq<T>, pred: T > bool): seq<T>
reads pred.reads
requires forall t :: pred.requires(t)
ensures forall x :: x in xs && pred(x) ==> x in filter(xs, pred)
ensures forall x :: x in filter(xs, pred) ==> x in xs && pred(x)
{
if xs == 0 then []
else if pred(xs[0]) then [xs[0]] + filter(xs[1..], pred)
else filter(xs[1..], pred)
}
How might I prove that this function distributes over an append?
lemma filter_distributes_over_append<T>(xs1: seq<T>, xs2: seq<T>, pred: T > bool)
requires forall t :: pred.requires(t)
ensures filter(xs1 + xs2, pred) == filter(xs1, pred) + filter(xs2, pred)
Any tips and techniques would be much appreciated! Thanks!



Had a flash of insight and came up with the following, but to be honest, it feels a bit like writeonly code. Any suggestions for making this proof clearer?
lemma append_associative<T>(xs: seq<T>, ys: seq<T>, zs: seq<T>)
ensures (xs + ys) + zs == xs + (ys + zs)
{}
lemma filter_distributes_over_append<T>(xs1: seq<T>, xs2: seq<T>, pred: T > bool)
requires forall t :: pred.requires(t)
ensures filter(xs1 + xs2, pred) == filter(xs1, pred) + filter(xs2, pred)
{
if (xs1 == []) {
} else if pred(xs1[0]) {
calc == {
filter(xs1 + xs2, pred); { assert xs1 == [xs1[0]] + xs1[1..]; }
filter(([xs1[0]] + xs1[1..]) + xs2, pred); { append_associative([xs1[0]], xs1[1..], xs2); }
filter([xs1[0]] + (xs1[1..] + xs2), pred);
[xs1[0]] + filter(xs1[1..] + xs2, pred);
[xs1[0]] + filter(xs1[1..], pred) + filter(xs2, pred);
filter([xs1[0]], pred) + filter(xs1[1..], pred) + filter(xs2, pred);
filter([xs1[0]] + xs1[1..], pred) + filter(xs2, pred);
filter(xs1, pred) + filter(xs2, pred);
}
} else {
calc == {
filter(xs1 + xs2, pred); { assert xs1 == [xs1[0]] + xs1[1..]; }
filter(([xs1[0]] + xs1[1..]) + xs2, pred); { append_associative([xs1[0]], xs1[1..], xs2); }
filter([xs1[0]] + (xs1[1..] + xs2), pred);
[] + filter(xs1[1..] + xs2, pred);
filter(xs1[1..] + xs2, pred);
filter(xs1, pred) + filter(xs2, pred);
}
}
}

