►CMSC 433:   Programming Language Technologies and Paradigms
▼Notes
►7 Inductive Types
On this page:
7.1 Linked Lists
7.2 Generic Lists
7.3 Natural Numbers
7.4 BST
7.5 Higher-order Functions
7.6 Generic BST<T>
8.17
    contents    up   

7 Inductive Types🔗

    7.1 Linked Lists

    7.2 Generic Lists

    7.3 Natural Numbers

    7.4 BST

    7.5 Higher-order Functions

    7.6 Generic BST<T>

7.1 Linked Lists🔗

Here’s a simple container data structure: linked lists of natural numbers. 

datatype NatList = 
           NNil 
         | NCons(head: nat, tail: NatList)

The datatype command declares an inductive type by specifying its constructor functions—the functions used to build values of that type. The Cons constructor is recursive, since it refers to the same type in its definition. Its name comes from “construct,” a term rooted in the history of functional programming, where the Lisp language first introduced this convention.

Here is how to construct a list of the first n n positive integers, arranged in decreasing order.

Dafny

function FirstN(n: nat): NatList {
  if n == 0 then NNil else NCons(n, FirstN(n-1))
}
method TestFirstN(){
  assert FirstN(0) == NNil;
  assert FirstN(3) == NCons(3,NCons(2,NCons(1,NNil)));
}

We can also pull apart values of inductive types in recursive functions. Let’s add up all the numbers in a list.

We can also unpack values of inductive types within recursive functions. For example, let us write a function that sums all the numbers in a list.

Dafny

function Sum(ls: NatList): nat {
  if ls == NNil then 0 else ls.head + Sum(ls.tail)
}

These definitions lend themselves naturally to lemmas proved by induction. We will now make full use of Dafny’s capability to perform automatic induction.

Dafny

lemma Sum_FirstN(n: nat)
  ensures Sum(FirstN(n)) == n * (n + 1) / 2
{
}

Dafny is able to prove this automatically. However, if automatic induction is disabled, we must manually demonstrate that the postcondition holds.

Dafny

lemma{:induction false}  Sum_FirstN'(n: nat)
  ensures Sum(FirstN(n)) == n * (n + 1) / 2
{
  if n == 0{} //base case. Trivially holds.
  else{
    calc{
      Sum(FirstN(n));
      n + Sum(FirstN(n-1));
      {Sum_FirstN'(n-1);}
      n + (n -1 )* n  / 2;
      n * (n + 1) / 2;
    }
  }
}

We can also use assert .. by instead of calc

Dafny

lemma{:induction false}  Sum_FirstN''(n: nat)
  ensures Sum(FirstN(n)) == n * (n + 1) / 2
{
  if n == 0{}
  else{
    assert Sum(FirstN(n)) == n + Sum(FirstN(n-1));
    assert Sum(FirstN(n-1)) == (n -1 )* n  / 2
      by {Sum_FirstN'(n-1);}
    assert Sum(FirstN(n))  == n * (n + 1) / 2;
  }
}

The concepts underlying inductive datatypes originate from the long-standing tradition of functional programming, as exemplified by languages such as Haskell. Dafny likewise provides a pattern-matching notation, which aligns with this tradition and is often the preferred style.

Dafny

function Sum'(ls: NatList): nat {
  match ls
  case NNil => 0
  case NCons(n, ls') => n + Sum'(ls')
}
lemma Sum_Sum'(ls: NatList)
  ensures Sum(ls) == Sum'(ls)
{
}

// turn off the automatic induction
lemma {:induction false} Sum_Sum''(ls: NatList)
  ensures Sum(ls) == Sum'(ls)
{
  if ls == NNil{}
  else{
    calc{
      Sum(ls);
      ls.head + Sum(ls.tail);
      {Sum_Sum''(ls.tail);}
      ls.head + Sum'(ls.tail);
    }
  }
}


lemma Sum_Sum'_FirstN(n: nat)
  ensures Sum'(FirstN(n)) == n * (n + 1) / 2
{
}

7.2 Generic Lists🔗

Notice that the definition of lists is not inherently specialized to numerical data. It is common to define generic container types that can store values of arbitrary type. Below is a generic version, parameterized by a type variable T.

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

We now turn our attention to several classic operations on lists.

First, how many elements does a list have?

Dafny

function Length<T>(xs: List<T>): nat {
  match xs
  case Nil => 0
  case Cons(_, tail) => 1 + Length(tail)
}
method TestLength(){
  var l:List<int> := Cons(10,Cons(20,Nil));
  assert Length(l) == 2;
}

Next, we can use a version of Cons that adds a new element at the end of a list, instead of the start.

Dafny

function Snoc<T>(xs: List<T>, y: T): List<T> {
  match xs
    case Nil => Cons(y, Nil)
    case Cons(x, tail) => Cons(x, Snoc(tail, y))
}
method TestSnoc(){
  var l:List<int> := Cons(10,Cons(20,Nil));
  assert Snoc(l,30) == Cons(10,Cons(20,Cons(30,Nil)));
}

How do the last two functions interact?

Dafny

lemma LengthSnoc<T>(xs: List<T>, y: T)
  ensures Length(Snoc(xs, y)) == Length(xs) + 1
{
}

Again, here is a proof without the automatic induction:

Dafny

lemma{:induction false}  LengthSnoc'<T>(xs: List<T>, y: T)
  ensures Length(Snoc(xs, y)) == Length(xs) + 1
{
  if xs == Nil{}
  else{
    calc{
      Length(Snoc(xs, y));
      Length(Cons(xs.head, Snoc(xs.tail, y)));
      Length(Snoc(xs.tail, y)) + 1;
      {LengthSnoc'(xs.tail,y);}
      Length(xs) + 1;
    }
  }
}

The next classic is appending two lists together.

Dafny

function Append'<T>(xs: List<T>, ys: List<T>): List<T> {
  match xs
    case Nil => ys
    case Cons(x, tail) => Cons(x, Append'(tail, ys))
}

It is easy to capture the interaction with Length’.

Dafny

lemma LengthAppend<T>(xs: List<T>, ys: List<T>)
  ensures Length(Append'(xs, ys)) == Length(xs) + Length(ys)
{
}

However, we could also build this property into the original definition as a postcondition!

Dafny

function Append<T>(xs: List<T>, ys: List<T>): List<T>
  ensures Length(Append(xs, ys)) == Length(xs) + Length(ys)
{
  match xs
    case Nil => ys
    case Cons(x, tail) => Cons(x, Append(tail, ys))
}
method TestAppend(){
  var l1:= Cons(1,Cons(2,Nil));
  var l2:= Cons(3,Cons(4,Nil));
  assert Append(l1,l2) == Cons(1,Cons(2,Cons(3,Cons(4,Nil))));
}

In Dafny, methods become opaque once they are completed, meaning that only the properties specified in their contracts are available for reasoning. In contrast, function definitions remain transparent, allowing their full definitions to be visible. The advantage of embedding properties directly in function definitions is that Dafny automatically “remembers” them at each call site, eliminating the need to invoke lemmas manually. The drawback is that the definition can become cluttered if numerous properties must be included.

Let’s prove some more algebraic properties of Append.

Dafny

lemma AppendNil<T>(xs: List<T>)
  ensures Append(xs, Nil) == xs
{
}

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

lemma SnocAppend<T>(xs: List<T>, y: T)
  ensures Snoc(xs, y) == Append(xs, Cons(y, Nil))
{
}

If you are curious, here are two different proofs for AppendAssociative without automatic induction.

Dafny

lemma{:induction false}
  AppendAssociative'<T>(xs: List<T>, ys: List<T>, zs:List<T>)
  ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs))
{
  match xs
  case Nil =>
  // Base case:
  // Append(Append(Nil, ys), zs) == Append(Nil, Append(ys, zs))
  // Left:  Append(Nil, ys) = ys, so Append(ys, zs)
  // Right: Append(Nil, Append(ys, zs)) = Append(ys, zs)
  // So both sides equal.
  case Cons(h, t) =>
    calc{
      Append(Append(Cons(h, t), ys), zs);
      Append(Cons(h, Append(t, ys)), zs);
      {AppendAssociative'(t, ys, zs);}
      Cons(h, Append(t, Append(ys, zs)));
      Append(Cons(h,t), Append(ys, zs));
      Append(xs, Append(ys, zs));
    }
}

Actually, the proof can be shoter:

Dafny

lemma{:induction false}
 AppendAssociative''<T>(xs: List<T>, ys: List<T>, zs:List<T>)
  ensures Append(Append(xs, ys), zs) == Append(xs, Append(ys, zs))
{
  if xs == Nil{}
  else{
    calc{
      Append(Append(xs, ys), zs);
      {AppendAssociative''(xs.tail, ys, zs);}
      Append(xs, Append(ys, zs));
    }
  }}

Dafny

lemma SnocAppend<T>(xs: List<T>, y: T)
  ensures Snoc(xs, y) == Append(xs, Cons(y, Nil))
{
}

And some other classic list functions:

Dafny

function Take<T>(xs: List<T>, n: nat): List<T>
  requires n <= Length(xs)
{
  if n == 0 then Nil else Cons(xs.head, Take(xs.tail, n - 1))
}
method testTake(){
  var t := Take(Cons(1,Cons(2,Cons(3,Cons(4,Nil)))),2);
  assert t == Cons(1,Cons(2,Nil));
}

function Drop<T>(xs: List<T>, n: nat): List<T>
  requires n <= Length(xs)
{
  if n == 0 then xs else Drop(xs.tail, n - 1)
}
method testDrop(){
  var t := Drop(Cons(1,Cons(2,Cons(3,Cons(4,Nil)))),2);
  assert t == Cons(3,Cons(4,Nil));
}

lemma AppendTakeDrop<T>(xs: List<T>, n: nat)
  requires n <= Length(xs)
  ensures Append(Take(xs, n), Drop(xs, n)) == xs
{
}

lemma TakeDropAppend<T>(xs: List<T>, ys: List<T>)
  ensures Take(Append(xs, ys), Length(xs)) == xs
  ensures Drop(Append(xs, ys), Length(xs)) == ys
{
}

Note that Dafny rejects the postconditions here if we use the version of Append without a postcondition asserting the length of the resulting list!

Dafny

function At<T>(xs: List<T>, i: nat): T
  requires i < Length(xs)
{
  if i == 0 then xs.head else At(xs.tail, i - 1)
}
method testAt(){
  var t := At(Cons(1,Cons(2,Cons(3,Cons(4,Nil)))),2);
  assert t == 3;
}

lemma AtDropHead<T>(xs: List<T>, i: nat)
  requires i < Length(xs)
  ensures Drop(xs, i).Cons? && At(xs, i) == Drop(xs, i).head
{
}

Note that we used a question-mark operation to check which list constructor created a particular value. Without this, Dafny would reject the postcondition as ill-formed (it “may crash”)

Dafny

lemma AtAppend<T>(xs: List<T>, ys: List<T>, i: nat)
  requires i < Length(Append(xs, ys))
  ensures At(Append(xs, ys), i)
       == if i < Length(xs) then
            At(xs, i)
          else
            At(ys, i - Length(xs))
{
}

How can we determine the position of an element in a list? What should we do if the element is not present?

Dafny

function Find<T(==)>(xs: List<T>, y: T): nat
  ensures Find(xs, y) <= Length(xs)
{
  match xs
  case Nil => 0
  case Cons(x, tail) =>
    if x == y then 0 else 1 + Find(tail, y)
}
method testFind(){
  assert Find(Nil,0) == 0;
  assert Find(Nil,5) == 0;
  var t := Find(Cons(1,Cons(2,Cons(3,Cons(4,Nil)))),2);
  assert t == 1;
  //if not found, return list length
  assert Find(Cons(1,Cons(2,Cons(3,Cons(4,Nil)))),5) == 4;
}

Note the (==) annotation on the type parameter, to require it to support a particular operator.

The answer to the question above is that, if the element is not found, we return the length of the list.

Dafny

lemma AtFind<T>(xs: List<T>, y: T)
  ensures Find(xs, y) == Length(xs) || At(xs, Find(xs, y)) == y
{
}

lemma BeforeFind<T>(xs: List<T>, y: T, i: nat)
  ensures i < Find(xs, y) ==> At(xs, i) != y
{
}

lemma FindAppend<T>(xs: List<T>, ys: List<T>, y: T)
  ensures Find(xs, y) == Length(xs) ||
          Find(Append(xs, ys), y) == Find(xs, y)
{
}

lemma FindDrop<T>(xs: List<T>, y: T, i: nat)
  ensures i <= Find(xs, y) ==>
          Find(xs, y) == Find(Drop(xs, i), y) + i
{
}

function SlowReverse<T>(xs: List<T>): List<T> {
  match xs
  case Nil => Nil
  case Cons(x, tail) => Snoc(SlowReverse(tail), x)
}

Surprisingly, the following isn’t proved automatically!

Dafny

lemma LengthSlowReverse<T>(xs: List<T>)
  ensures Length(SlowReverse(xs)) == Length(xs)
{
  match xs
  case Nil =>
  case Cons(x, tail) => LengthSnoc(SlowReverse(tail), x);
}

An asymptotically efficient version of reverse is included in most standard libraries of functional programming languages.

Dafny

function ReverseAux<T>(xs: List<T>, acc: List<T>): List<T>
{
  match xs
  case Nil => acc
  case Cons(x, tail) => ReverseAux(tail, Cons(x, acc))
}

function Reverse<T>(xs: List<T>): List<T> {
  ReverseAux(xs, Nil)
}

lemma ReverseAuxSlowCorrect<T>(xs: List<T>, acc: List<T>)
  ensures ReverseAux(xs, acc) == Append(SlowReverse(xs), acc)
{
  match xs
  case Nil =>
  case Cons(x, tail) =>
    calc {
      Append(SlowReverse(xs), acc);
      Append(Snoc(SlowReverse(tail), x), acc);
      { SnocAppend(SlowReverse(tail), x); }
      Append(Append(SlowReverse(tail), Cons(x, Nil)), acc);
      { AppendAssociative(SlowReverse(tail), Cons(x, Nil), acc); }
      Append(SlowReverse(tail), Append(Cons(x, Nil), acc));
      { assert Append(Cons(x, Nil), acc) == Cons(x, acc); }
      Append(SlowReverse(tail), Cons(x, acc));
      { ReverseAuxSlowCorrect(tail, Cons(x, acc)); }
      ReverseAux(tail, Cons(x, acc));
      ReverseAux(xs, acc);
    }
}

lemma ReverseCorrect<T>(xs: List<T>)
  ensures Reverse(xs) == SlowReverse(xs)
{
  calc {
    Reverse(xs);
    ReverseAux(xs, Nil);
    { ReverseAuxSlowCorrect(xs, Nil); }
    Append(SlowReverse(xs), Nil);
    { AppendNil(SlowReverse(xs)); }
    SlowReverse(xs);
  }
}

lemma ReverseAuxCorrect<T>(xs: List<T>, acc: List<T>)
  ensures ReverseAux(xs, acc) == Append(Reverse(xs), acc)
{
  ReverseCorrect(xs);
  ReverseAuxSlowCorrect(xs, acc);
}

lemma LengthReverse<T>(xs: List<T>)
  ensures Length(Reverse(xs)) == Length(xs)
{
  ReverseCorrect(xs); //Reverse(xs) == SlowReverse(xs)
  LengthSlowReverse(xs); // Length(SlowReverse(xs)) == Length(xs)
}

lemma ReverseAuxAppend<T>(xs: List<T>, ys: List<T>, acc: List<T>)
  ensures ReverseAux(Append(xs, ys), acc) ==
                       Append(Reverse(ys), ReverseAux(xs, acc))
{
  match xs
  case Nil => ReverseAuxCorrect(ys, acc);
  case Cons(_, _) =>
}

Dafny

// Length of a list (Tail recursive)
function LengthTailCall<T>(xs:List<T>, acc:nat):(l:nat)
  ensures LengthTailCall(xs,acc) == Length(xs) + acc
{
  match xs {
    case Nil => acc
    case Cons(_, tail) => LengthTailCall(tail, acc+1)
  }
}

Prove the tail recursive length equals the non-tail recursive length

Dafny

lemma LengthCorrect<T>(xs:List<T>)
  ensures LengthTailCall(xs,0) == Length(xs)
{}

Dafny

// Length of a list (imperative)
method LengthImp<T>(xs:List<T>) returns (l:nat)
  ensures Length(xs) == l  //postcondition
{
  var lst := xs;
  var len := 0;
  while lst != Nil
    decreases Length(lst)
    invariant len + Length(lst) == Length(xs)
  {
    len := len + 1;
    lst := lst.tail;
  }
  return len;
}

Dafny

// Insert an item at index
function insert<T>(xs:List<T>,v:T, index:nat):(l:List<T>)
  requires  index <= Length(xs)
  ensures Length(xs) + 1 == Length(l)
  ensures At(l,index) == v
 // Equality-supporting type parameter T(==) is not needed
 // for ghost context
{
  if index == 0 then Cons(v,xs)
  else Cons(xs.head, insert(xs.tail, v, index - 1))
}

Dafny

// Check membership
function contains<T(==)>(xs:List<T>, v:T):bool{
  match xs {
    case Nil => false
    case Cons(h,t) => v == h || contains(t,v)
  }
}

Dafny

// Convert a list to q sequence
function List2Seq<T>(xs:List<T>):(s:seq<T>)
  ensures Length(xs) == |s|
  ensures forall i:nat:: i < Length(xs) ==> At(xs,i) == s[i]
{
  match xs{
    case Nil => []
    case Cons(h,t)=>[h] + List2Seq(t)
  }
}

7.3 Natural Numbers🔗

OK, now for something completely different! Let’s do some number theory, explaining the natural numbers and their key operations from first principles. 

datatype Unary = 
             Zero 
           | Suc(pred: Unary)

That’s Suc for successor and pred for predecessor. These are the Peano numbers: every natural is either zero or the successor of another natural.

We can convert back to the built-in type.

Dafny

function UnaryToNat(x: Unary): nat {
  match x
  case Zero => 0
  case Suc(x') => 1 + UnaryToNat(x')
}

And we can convert in the opposite direction.

Dafny

function NatToUnary(n: nat): Unary {
  if n == 0 then Zero else Suc(NatToUnary(n-1))
}

lemma NatUnaryCorrespondence(n: nat, x: Unary)
  ensures UnaryToNat(NatToUnary(n)) == n
  ensures NatToUnary(UnaryToNat(x)) == x
{
}

predicate Less(x: Unary, y: Unary) {
  y != Zero && (x.Suc? ==> Less(x.pred, y.pred))
}

lemma LessCorrect(x: Unary, y: Unary)
  ensures Less(x, y) <==> UnaryToNat(x) < UnaryToNat(y)
{
}

lemma LessTransitive(x: Unary, y: Unary, z: Unary)
  requires Less(x, y) && Less(y, z)
  ensures Less(x, z)
{
}

Now, let us prove the lemma without automatic induction.

Dafny

lemma{:induction false} LessTransitive2(x: Unary, y: Unary, z: Unary)
  requires Less(x, y) && Less(y, z)
  ensures Less(x, z)
{
  match x
   case Zero =>
   case Succ(x') =>
    match y
    case Succ(y') =>
      // y == Succ(y') and Less(x', y')
      // Also, Less(y, z) => y == Succ(y') and
      // z == Succ(z') and Less(y', z')
      match z
      case Succ(z') =>
        // x == Succ(x'), y == Succ(y'), z == Succ(z')
        // Less(x', y') and Less(y', z')
        // Apply induction on x', y', z'
        LessTransitive(x', y', z');
        //assert Less(x', z');
        //assert Less(Succ(x'), Succ(z'));
        //assert Less(x, z);
}

If we change the explicit requires to an implication, it requires a bit of extra work because Less(x, y) && Less(y, z) is no longer available as an assumption.

Dafny


lemma LessTransitive3(x: Unary, y: Unary, z: Unary)
  ensures  (Less(x, y) && Less(y, z)) ==> Less(x, z)
{
  if Less(x, y) && Less(y, z) {
    match x
    case Zero =>
    // Zero is less than any non-zero y,
    // and y < z implies z != Zero
    // assert y != Zero;
    // assert z != Zero;
    // assert Less(Zero, z);
    case Succ(x') =>
      // Since Less(x, y), y must be Succ(y') and Less(x', y')
      match y
      case Succ(y') =>
        //assert x == Succ(x') && y == Succ(y');
        //assert Less(x', y');
        // Also, Less(y, z) implies z is Succ(z') and Less(y', z')
        match z
        case Succ(z') =>
          //assert y == Succ(y') && z == Succ(z');
          //assert Less(y', z');
          // Apply induction
          calc {
            Less(x', y');
            Less(y', z');
            {LessTransitive3(x',y',z');}
            Less(x', z');  // by induction
            Less(x, z);
          }
          //assert Less(x, z);
  }
}

Dafny


function Add(x: Unary, y: Unary): Unary {
  match y
  case Zero => x
  case Suc(y') => Suc(Add(x, y'))
}

lemma AddCorrect(x: Unary, y: Unary)
  ensures UnaryToNat(Add(x, y)) == UnaryToNat(x) + UnaryToNat(y)
{
}

lemma SucAdd(x: Unary, y: Unary)
  ensures Suc(Add(x, y)) == Add(Suc(x), y)
{
}

lemma AddZero(x: Unary)
  ensures Add(Zero, x) == x
{
}

lemma LessAdd(x:Unary)
   ensures Less(x,Add(Suc(Zero),x))
 {}

function Sub(x: Unary, y: Unary): Unary
  requires !Less(x, y)
{
  match y
  case Zero => x
  case Suc(y') => Sub(x.pred, y')
}

lemma SubCorrect(x: Unary, y: Unary)
  requires !Less(x, y)
  ensures UnaryToNat(Sub(x, y)) == UnaryToNat(x) - UnaryToNat(y)
{
}

function Mul(x: Unary, y: Unary): Unary {
  match x
  case Zero => Zero
  case Suc(x') => Add(Mul(x', y), y)
}

lemma MulCorrect(x: Unary, y: Unary)
  ensures UnaryToNat(Mul(x, y)) == UnaryToNat(x) * UnaryToNat(y)
{
  match x
  case Zero =>
  case Suc(x') =>
    calc {
      UnaryToNat(Mul(x, y));
      == UnaryToNat(Add(Mul(x', y), y));
      == { AddCorrect(Mul(x', y), y); }
      UnaryToNat(Mul(x', y)) + UnaryToNat(y);
    }
}

7.4 BST🔗

Let’s finish up with another classic container structure, 

datatype BST<V> = 
        Leaf
      | Node(key: int, value: V, left: BST<V>, right: BST<V>)

First, we will look at binary search trees (BSTs) with integers as keys. We will extend this to generic BSTs later. We use the Option type for return values. You have seen the Option type before in OCaml. 
datatype Option<T> = 
     None 
  | Some(value: T)

Dafny

function Lookup<V>(t: BST<V>, k: int): Option<V>
{
  match t
  case Leaf => None
  case Node(k', v, l, r) =>
    if k == k' then
      Some(v)
    else if k < k' then
      Lookup(l, k)
    else
      Lookup(r, k)
}

function Insert<V>(t: BST<V>, k: int, v: V): BST<V>
{
  match t
  case Leaf => Node(k, v, Leaf, Leaf)
  case Node(k', v', l, r) =>
    if k == k' then
      Node(k, v, l, r)
    else if k < k' then
      Node(k', v', Insert(l, k, v), r)
    else
      Node(k', v', l, Insert(r, k, v))
}

This property gets a nice automated proof.

Dafny

lemma Lookup_Insert<V>(t: BST<V>, k: int, v: V, k': int)
  ensures Lookup(Insert(t, k, v), k') ==
    if k' == k then Some(v) else Lookup(t, k')
{
}

Let’s also reason about the ranges of values that appear in BSTs. A range has optional lower and upper bounds, pushed into pairs like so. 

type range = (Option<int>, Option<int>)

Dafny

predicate InRange(n: int, r: range) {
  (r.0.None? || r.0.value < n)
    && (r.1.None? || n < r.1.value)
}

A BST is well-formed w.r.t. a range if all its keys fall in the range.

Dafny

predicate WellFormedBST<V>(t: BST<V>, rng: range) {
  match t
  case Leaf => true
  case Node(k, _, l, r) =>
    InRange(k, rng)
    && WellFormedBST(l, (rng.0, Some(k)))
    && WellFormedBST(r, (Some(k), rng.1))
}

lemma LookupRange<V>(t: BST<V>, k: int, rng: range)
  requires WellFormedBST(t, rng)
  requires InRange(k, rng)
  ensures Lookup(t, k).Some? ==> InRange(k, rng)
  // Note the above '?' syntax for checking if a value was
  // formed with a certain constructor.
{
}

This proof is interesting for forcing us to invoke IH(induction hypothesis)es explicitly.

Dafny

lemma InsertWellFormed<V>(t: BST<V>, rng: range, k : int, v: V)
  requires WellFormedBST(t, rng)
  requires InRange(k, rng)
  ensures WellFormedBST(Insert(t, k, v), rng)
{
  match t
  case Leaf =>
  case Node(k', v', l, r) =>
    if k == k' {
    } else if k < k' {
      InsertWellFormed(l, (rng.0, Some(k')), k, v);
    } else {
      InsertWellFormed(r, (Some(k'), rng.1), k, v);
    }
}

7.5 Higher-order Functions🔗

Dafny

function Map<A, B>(f: A -> B, ls: List<A>): List<B> {
  match ls
  case Nil => Nil
  case Cons(x, ls') => Cons(f(x), Map(f, ls'))
}

lemma LengthMap<A, B>(f: A -> B, ls: List<A>)
  ensures Length(Map(f, ls)) == Length(ls)
{
}

lemma MapAppend<A, B>(f: A -> B, ls1: List<A>, ls2: List<A>)
  ensures Map(f, Append(ls1, ls2)) ==
             Append(Map(f, ls1), Map(f, ls2))
{
}

We can work with functions in an event more first-class way.

Dafny

function Identity<A>(): A -> A {
  x => x
}

lemma MapIdentity<A>(ls: List<A>)
  ensures Map(Identity(), ls) == ls
{
}

function Compose<A, B, C>(f: A -> B, g: B -> C): A -> C {
  x => g(f(x))
}

lemma MapCompose<A, B, C>(f: A -> B, g: B -> C, ls: List<A>)
  ensures Map(Compose(f, g), ls) == Map(g, Map(f, ls))
{
}

This function is a classic for stepping through all elements of a list.

Dafny

function Foldl<A, B>(f : (A, B) -> B, acc: B, ls: List<A>): B {
  match ls
  case Nil => acc
  case Cons(x, ls') => Foldl(f, f(x, acc), ls')
}

For instance, we can use Foldl to add up the elements of a list.

Dafny

lemma Foldl_example()
  ensures Foldl((n, m) => n + m, 0,
                Cons(1, Cons(2, Cons(3, Nil)))) ==
                3 + 2 + 1 + 0
{
}

The order in which we wrote that sum at the end is suggestive. Foldl somewhat naturally applies list elements in reverse order. Let’s formalize that connection to list reversal.

Dafny

lemma FoldlReverseAux<A>(ls: List<A>, acc: List<A>)
  ensures Foldl((h, t) => Cons(h, t), acc, ls) ==
          ReverseAux(ls, acc)
{
}

lemma FoldlReverse<A>(ls: List<A>)
  ensures Foldl((h, t) => Cons(h, t), Nil, ls) == Reverse(ls)
{
  FoldlReverseAux(ls, Nil);
}

Yup, it worked!

Here is a classic algebraic law relating Map and Fold.

Dafny

lemma FoldlMap<A, B, C>(f: A -> B, g : (B, C) -> C,
                        acc: C, ls: List<A>)
  ensures Foldl(g, acc, Map(f, ls)) == Foldl((x, a) =>
                g(f(x), a), acc, ls)
{
  match ls
  case Nil =>
  case Cons(x, ls') =>
    calc {
      Foldl(g, acc, Map(f, ls));
      Foldl(g, acc, Map(f, Cons(x, ls')));
      Foldl(g, acc, Cons(f(x), Map(f, ls')));
      Foldl(g, g(f(x), acc), Map(f, ls'));
      { FoldlMap(f, g, g(f(x), acc), ls'); }
      Foldl((x, a) => g(f(x), a), g(f(x), acc), ls');
      Foldl((x, a) => g(f(x), a), acc, ls);
    }

    // Or just the following line suffices:
    // FoldlMap(f, g, g(f(x), acc), ls');
}

7.6 Generic BST<T>🔗

Now back to binary search trees. This time, using higher-order functions, we venture into making trees generic in their key types! 

datatype Option<T> = 
             None 
           | Some(value: T)

datatype BST<K, V> = 
        Leaf
      | Node(key: K, value: V, left: BST<K, V>, right: BST<K, V>)

Note how Lookup (and many more operations to come) takes in a "less-than" comparison function as an argument.

Dafny

function Lookup<K(==), V>(lt: (K, K) -> bool,
                         t: BST<K, V>, k: K): Option<V>
{
  match t
  case Leaf => None
  case Node(k', v, l, r) =>
    if k == k' then
      Some(v)
    else if lt(k, k') then
      Lookup(lt, l, k)
    else
      Lookup(lt, r, k)
}

function Insert<K(==), V>(lt: (K, K) -> bool,
                          t: BST<K, V>, k: K, v: V): BST<K, V>
{
  match t
  case Leaf => Node(k, v, Leaf, Leaf)
  case Node(k', v', l, r) =>
    if k == k' then
      Node(k, v, l, r)
    else if lt(k, k') then
      Node(k', v', Insert(lt, l, k, v), r)
    else
      Node(k', v', l, Insert(lt, r, k, v))
}

Nifty: we can prove this old law, without needing to know anything about the implementation of ’lt’.

Dafny

lemma Lookup_Insert<K, V>(lt: (K, K) -> bool,
                          t: BST<K, V>, k: K, v: V, k': K)
  ensures Lookup(lt, Insert(lt, t, k, v), k') ==
          if k' == k then Some(v) else Lookup(lt, t, k')
{
}

OK, let’s try a more stringent example. This function flips the tree on its side. What should the effect be on the tree, interpreted as a proper binary search tree?

Dafny

function Mirror<K, V>(t: BST<K, V>): BST<K, V> {
  match t
  case Leaf => Leaf
  case Node(k, v, l, r) => Node(k, v, Mirror(r), Mirror(l))
}

This function transformer will be helpful. It flips the senses of the two arguments, which is just what we need to explain what Mirror accomplishes.

Dafny

function Flip<A, B, C>(f: (A, B) -> C): (B, A) -> C {
  (b, a) => f(a, b)
}

function Less(x: int, y: int): bool { x < y }

method testFlip(){
  assert Less(10, 20) == Flip(Less)(20,10);
}

So Mirror preserves Lookup, when we flip the less-than test. Note that, working through the proof, we realize that this property depends on ’lt’ acting like a real total order.

Dafny

lemma LookupMirror<K, V>(lt: (K, K) -> bool, t: BST<K, V>, k: K)
  requires forall a, b : K :: lt(a, b) == (!lt(b, a) && a != b)
  ensures Lookup(lt, t, k) == Lookup(Flip(lt), Mirror(t), k)
{
  // This proof actually goes through automatically,
}

Here we show a calc that helped us realize what precondition to add.

Dafny

lemma LookupMirror'<K, V>(lt: (K, K) -> bool, t: BST<K, V>, k: K)
  requires forall a, b : K :: lt(a, b) == (!lt(b, a) && a != b)
  ensures Lookup(lt, t, k) == Lookup(Flip(lt), Mirror(t), k)
{
  match t
  case Leaf =>
  case Node(k', v', l, r) =>
    if k == k' {
    } else if lt(k, k') {
      calc {
        Lookup(lt, t, k);
        Lookup(lt, Node(k', v', l, r), k);
        Lookup(lt, l, k);
        { LookupMirror'(lt, l, k); } Lookup(Flip(lt), Mirror(l), k);
        { assert Flip(lt)(k', k); } Lookup(Flip(lt), Node(k', v', Mirror(r), Mirror(l)), k);
        Lookup(Flip(lt), Mirror(Node(k', v', l, r)), k);
        Lookup(Flip(lt), Mirror(t), k);
      }
    } else {
      calc {
        Lookup(lt, t, k);
        Lookup(lt, Node(k', v', l, r), k);
        Lookup(lt, r, k);
        { LookupMirror(lt, r, k); } Lookup(Flip(lt), Mirror(r), k);
        { assert Flip(lt)(k, k'); } Lookup(Flip(lt), Node(k', v', Mirror(r), Mirror(l)), k);
        Lookup(Flip(lt), Mirror(Node(k', v', l, r)), k);
        Lookup(Flip(lt), Mirror(t), k);
      }
    }
}

This property may initially seem unnecessary to state explicitly: Lookup behaves identically when given two functions that themselves behave identically. However, this property does not hold automatically for arbitrary Dafny functions. In practice, we must examine each function individually. Intuitively, while different sorting algorithms may always produce equivalent outputs, we may not want to consider the algorithms themselves as equivalent.

Dafny

lemma LookupExtensional<K, V>(lt: (K, K) -> bool, lt': (K, K) ->
                                       bool, t: BST<K, V>, k: K)
  requires forall a, b : K :: lt(a, b) == lt'(a, b)
  ensures Lookup(lt, t, k) == Lookup(lt', t, k)
{
}

The precondition two lemmas back was a little delicate, so let’s check it works with a concrete key type.

Dafny

lemma LookupMirrorInt<V>(t: BST<int, V>, k: int)
  ensures Lookup((a, b) => a < b, t, k) ==
          Lookup((b, a) => a < b, Mirror(t), k)
{
  var lt := (a: int, b: int) => a < b;
  var lt' := (b: int, a: int) => a < b;

  LookupMirror(lt, t, k);
  LookupExtensional(Flip(lt), lt', Mirror(t), k);
}

How many nodes are there in the tree?

Dafny

function Size<K, V>(t: BST<K, V>): nat {
  match t
  case Leaf => 0
  case Node(_, _, l, r) => 1 + Size(l) + Size(r)
}

Sorted list of keys from a tree (Well, it’s sorted if the tree is well-formed.)

Dafny

function Keys<K, V>(t: BST<K, V>): List<K> {
  match t
  case Leaf => Nil
  case Node(k, _, l, r) => Cons(k, Append(Keys(l), Keys(r)))
}

lemma SizeKeys<K, V>(t: BST<K, V>)
  ensures Length(Keys(t)) == Size(t)
{
}

Checking if an element appears in a list

Dafny

predicate Member<A(==)>(x: A, xs: List<A>) {
  match xs
  case Nil => false
  case Cons(y, xs') => x == y || Member(x, xs')
}

lemma MemberAppend<A>(x: A, xs1: List<A>, xs2: List<A>)
  ensures Member(x, Append(xs1, xs2)) == (Member(x, xs1) ||
          Member(x, xs2))
{
}

Checking if a list is duplicate-free.

Dafny

predicate NoDup<A(==)>(xs: List<A>) {
  match xs
  case Nil => true
  case Cons(x, xs') => !Member(x, xs') && NoDup(xs')
}

OK, now we’re ready to characterize well-formedness of BSTs. This type captures a range of keys, optionally omitting a bound on either end.

Dafny

type range<K> = (Option<K>, Option<K>)

predicate InRange<K>(lt: (K, K) -> bool, n: K, r: range<K>) {
  (r.0.None? || lt(r.0.value, n))
    && (r.1.None? || lt(n, r.1.value))
}

Now we can redefine our well-formedness predicate from last time, but now it’s type-generic.

Dafny

predicate WellFormedBST<K, V>(lt: (K, K) -> bool, t: BST<K, V>, rng: range) {
  match t
  case Leaf => true
  case Node(k, _, l, r) =>
    InRange(lt, k, rng)
    && WellFormedBST(lt, l, (rng.0, Some(k)))
    && WellFormedBST(lt, r, (Some(k), rng.1))
}

Let’s check that well-formedness captures the intuitive property. Note that this property depends on a different algebraic property of ’lt’: transitivity.

Dafny

lemma RangeKeys<K, V>(lt: (K, K) -> bool, t : BST<K, V>, rng: range<K>, k: K)
  requires WellFormedBST(lt, t, rng)
  requires Member(k, Keys(t))
  requires forall a, b, c :: lt(a, b) && lt(b, c) ==> lt(a, c)
  ensures InRange(lt, k, rng)
{
  match t
  case Leaf =>
  case Node(k', v', l, r) => MemberAppend(k, Keys(l), Keys(r));
}

Working up to further BST properties, let’s define what it means for two lists to share no elements.

Dafny

predicate Disjoint<A(==)>(ls1: List<A>, ls2: List<A>) {
  match ls1
  case Nil => true
  case Cons(x, ls1') => !Member(x, ls2) && Disjoint(ls1', ls2)
}

That predicate is helpful to characterize the interaction of NoDup and Append.

Dafny

lemma NoDupAppend<A>(ls1: List<A>, ls2: List<A>)
  ensures NoDup(Append(ls1, ls2)) ==
           (Disjoint(ls1, ls2) && NoDup(ls1) && NoDup(ls2))
{
  match ls1
  case Nil =>
  case Cons(v, ls1') =>
    calc {
      NoDup(Append(ls1, ls2));
      == NoDup(Append(Cons(v, ls1'), ls2));
      == NoDup(Cons(v, Append(ls1', ls2)));
      == !Member(v, Append(ls1', ls2)) && NoDup(Append(ls1', ls2));
      == { NoDupAppend(ls1', ls2); }
       !Member(v, Append(ls1', ls2))
       && Disjoint(ls1', ls2) && NoDup(ls1') && NoDup(ls2);
      == { MemberAppend(v, ls1', ls2); }
      !Member(v, ls1') && !Member(v, ls2)
      && Disjoint(ls1', ls2) && NoDup(ls1') && NoDup(ls2);
    }
}

Here’s an even-more-direct but useful property.

Dafny

lemma DisjointAppend<A>(ls1: List<A>, ls2: List<A>, ls: List<A>)
  ensures Disjoint(Append(ls1, ls2), ls) ==
       (Disjoint(ls1, ls) && Disjoint(ls2, ls))
{
}

Now let’s prove an involved kind of strengthened induction hypothesis allowing us to conclude that two trees have disjoint keys.

Dafny

lemma BSTDisjoint<K, V>(lt: (K, K) -> bool, t1: BST<K, V>,
                        t2: BST<K, V>,
                        lower1: Option<K>, upper1: K, lower2: K, upper2: Option<K>)
  requires WellFormedBST(lt, t1, (lower1, Some(upper1)))
  requires WellFormedBST(lt, t2, (Some(lower2), upper2))
  requires lt(upper1, lower2) || upper1 == lower2
  // That last one is critical: the two trees' ranges are ordered
  // in a particular way, overlapping in *at most one* element,
  // and given how we interpret range ends strictly, that implies
  // *no overlap of elements*.

  requires forall a, b, c :: lt(a, b) && lt(b, c) ==> lt(a, c)
  requires forall a :: !lt(a, a) // New property: 'lt' is *irreflexive*.

  ensures Disjoint(Keys(t1), Keys(t2))
{
  match t1
  case Leaf =>
  case Node(k, v, l, r) =>
    // Note a little *proof by contradiction* here,
    // to show how we know a given fact doesn't hold.
    if Member(k, Keys(t2)) {
      assert InRange(lt, k, (lower1, Some(upper1)));
      assert lt(k, upper1);
      assert InRange(lt, k, (Some(lower2), upper2)) by
      { RangeKeys(lt, t2, (Some(lower2), upper2), k); }
      assert lt(lower2, k);
      assert lt(k, k); // by transitivity
      assert false;    // by antireflexivity
    }
    assert !Member(k, Keys(t2));

    calc {
      Disjoint(Cons(k, Append(Keys(l), Keys(r))), Keys(t2));
      !Member(k, Keys(t2)) && Disjoint(Append(Keys(l), Keys(r)), Keys(t2));
      { DisjointAppend(Keys(l), Keys(r), Keys(t2)); }
      !Member(k, Keys(t2)) && Disjoint(Keys(l), Keys(t2)) && Disjoint(Keys(r), Keys(t2));
      { BSTDisjoint(lt, l, t2, lower1, k, lower2, upper2); }
      !Member(k, Keys(t2)) && true && Disjoint(Keys(r), Keys(t2));
      { BSTDisjoint(lt, r, t2, Some(k), upper1, lower2, upper2); }
      !Member(k, Keys(t2)) && true && true;
      true && true && true;
      true;
    }
}

Finally, we pull it together into one pleasingly simple property: well-formed BSTs have no duplicate keys.

Dafny

lemma NoDupKeys<K, V>(lt: (K, K) -> bool,
                      t: BST<K, V>, rng: range<K>)
  requires WellFormedBST(lt, t, rng)
  requires forall a :: !lt(a, a)
  requires forall a, b, c :: lt(a, b) && lt(b, c) ==> lt(a, c)
  ensures NoDup(Keys(t))
{
  match t
  case Leaf =>
  case Node(k, v, l, r) =>
    assert !Member(k, Keys(l)) by {
      if Member(k, Keys(l)) {
        RangeKeys(lt, l, (rng.0, Some(k)), k);
      }
    }

    assert !Member(k, Keys(r)) by {
      if Member(k, Keys(r)) {
        RangeKeys(lt, r, (Some(k), rng.1), k);
      }
    }

    assert !Member(k, Append(Keys(l), Keys(r))) by {
      MemberAppend(k, Keys(l), Keys(r));
    }

    NoDupAppend(Keys(l), Keys(r));
    assert Disjoint(Keys(l), Keys(r)) by
     { BSTDisjoint(lt, l, r, rng.0, k, k, rng.1); }
}

    contents    up