datatype List<T> = Nil | Cons(head: T, tail: List<T>)
function Length<T>(xs: List<T>): int
case Cons(_, tl) => 1 + Length(tl)
function At<T>(xs: List, i: nat): T
if i == 0 then xs.head else At(xs.tail, i - 1)
ghost predicate Ordered(xs: List<int>) {
case Cons(_, Nil) => true
case Cons(hd0, Cons(hd1, _)) => (hd0 <= hd1) && Ordered(xs.tail)
lemma AllOrdered(xs: List<int>, i: nat, j: nat)
requires Ordered(xs) && i <= j < Length(xs)
ensures At(xs, i) <= At(xs, j)
AllOrdered(xs.tail, i - 1, j - 1);
assert xs.head <= xs.tail.head;
AllOrdered(xs.tail, 0, j - 1);
ghost function Count<T(==)>(xs: List<T>, p: T): int
ensures Count(xs, p) >= 0
case Cons(hd, tl) => (if hd == p then 1 else 0) + Count(tl, p)
ghost function Project<T(==)>(xs: List<T>, p: T): List<T> {
case Cons(hd, tl) => if hd == p then Cons(hd, Project(tl, p)) else Project(tl, p)
lemma {:induction false} CountProject<T(==)>(xs: List<T>, ys: List<T>, p: T)
requires Project(xs, p) == Project(ys, p)
ensures Count(xs, p) == Count(ys, p)
assert Count(xs, p) == 0;
assert Project(xs, p) == Nil;
assert Project(ys, p) == Nil;
CountProject(xs, ytl, p);
assert Count(ys, p) == 0;
CountProject(xtl, ys, p);
if xhd == p && yhd == p {
assert Count(xs, p) == 1 + Count(xtl, p);
assert Count(ys, p) == 1 + Count(ytl, p);
assert Project(xtl, p) == Project(ytl, p);
CountProject(xtl, ytl, p);
} else if xhd != p && yhd == p {
assert Count(xs, p) == Count(xtl, p);
assert Count(ys, p) == 1 + Count(ytl, p);
CountProject(xtl, ys, p);
} else if xhd == p && yhd != p {
assert Count(ys, p) == Count(ytl, p);
assert Count(xs, p) == 1 + Count(xtl, p);
CountProject(xs, ytl, p);
CountProject(xtl, ytl, p);
function InsertionSort(xs: List<int>): List<int>
case Cons(x, rest) => Insert(x, InsertionSort(rest))
function Insert(x: int, xs: List<int>): List<int>
case Cons(hd, tl) => if x < hd then Cons(x, xs) else Cons(hd, Insert(x, tl))
lemma InsertionSortOrdered(xs: List<int>)
ensures Ordered(InsertionSort(xs))
InsertionSortOrdered(tl);
InsertOrdered(hd, InsertionSort(tl));
lemma InsertOrdered(y: int, xs: List<int>)
ensures Ordered(Insert(y, xs))
assert Ordered(Cons(y, xs));
assert Ordered(Cons(hd, Insert(y, tl)));
lemma InsertionSortSameElements(xs: List<int>, p: int)
ensures Project(xs, p) == Project(InsertionSort(xs), p)
InsertSameElements(hd, InsertionSort(tl), p);
lemma InsertSameElements(y: int, xs: List<int>, p: int)
ensures Project(Cons(y, xs), p) == Project(Insert(y, xs), p)