Sunday, August 11, 2024

Binary Search Trees, Correctly!

This is the seventh blog post in a series about developing correct implementations of basic data structures and algorithms using the Deduce language and proof checker.

This post continues on the theme of binary trees, that is, trees in which each node has at most two children. The focus of this post is to implement the Search interface, described next, using binary trees.

The Search Interface

The Search interface includes operations to (1) create an empty data structure, (2) search for a value based on its associated key, and (3) insert a new key-value association.

The Search interface can also be implemented in a simple but less efficient way, using a function to map keys to values. With this approach, the operation to search for a value is just function call. The Maps.pf file defines the empty_map operation, which returns a function that maps every input to none.

assert @empty_map<Nat,Nat>(5) = none

The Maps.pf file also defined the update(f, k, v) operation, which returns a function that associates the key k with v but otherwise behaves like the given function f. Here is an example use of update.

define m2 = update(@empty_map<Nat,Nat>, 4, just(99))
assert m2(4) = just(99)
assert m2(5) = none

We will use this function implementation of the Search interface to specify the correctness of the binary tree implementation of Search.

We will store the keys and their values in a binary tree and implement BST_search and BST_insert operations. These operations are efficient (logarithmic time) when the binary tree is balanced, but we will save how to balance trees for a later blog post.

The main idea of a binary search tree comes from the notion of binary search on a sequence, that is, keep the sequennce in sorted-order and when searching for a key, start in the middle and go left by half of the subsequence if the key you’re looking for is less than the one at the current position; go right by half of the subsequence if the key is greater than the one at the current position. Of course, if they are equal, then you’ve found what you’re looking for. Thus, binary search is just like looking up the definition of a word in a dictionary. The word is your key and the dictionary is sorted alphabetically. You can start in the middle and compare your word to those on the current page, then flip to the left or right depending on whether your word is lower or higher in the alphabet.

The binary search tree adapts the idea of binary search from a sequence to a tree. Each node in the tree stores a key and its value. The left subtree of the node contain keys that are less than the node and the right subtree contain keys that are greater than the node. Thus, when searching for a key, one can compare it to the current node and then either go left or right depending on whether the key is less-than or greater-than the current node.

Consider the following diagram of a binary search tree. For simplicity, we will use numbers for both the keys and the values. In this diagram the key is listed before the colon and the value is after the colon. For example, this tree contains

  • key 10 associated with value 32,
  • key 13 associated with value 63,
  • etc.
Diagram of a Binary Search Tree

The following code builds this binary search tree using the Tree union type defined in the Binary Tree blog post and the Pair type from the Pair.pf file.

define mt = @EmptyTree<Pair<Nat,Nat>>
define BST_1 = TreeNode(mt, pair(1, 53), mt)
define BST_9 = TreeNode(mt, pair(9, 42), mt)
define BST_6 = TreeNode(BST_1, pair(6, 85), BST_9)
define BST_11 = TreeNode(mt, pair(11, 99), mt)
define BST_13 = TreeNode(BST_11, pair(13, 69), mt)
define BST_19 = TreeNode(mt, pair(19, 74), mt)
define BST_14 = TreeNode(BST_13, pair(14, 27), BST_19)
define BST_10 = TreeNode(BST_6, pair(10, 32), BST_14)

There are three operations in the binary search tree interface and here are their specifications.

  • The EmptyTree constructor from the Tree union type, which builds a binary search tree that does not contain any key-value associations.

  • BST_search : fn Tree<Pair<Nat,Nat>> -> (fn Nat -> Option<Nat>)

    The operation BST_search(T) returns a function that maps each key to its associated value.

  • BST_insert : fn Tree<Pair<Nat,Nat>>, Nat, Nat -> Tree<Pair<Nat,Nat>>

    The operation BST_insert(T, k, v) produces a new tree that associates value v with key k and for all other keys, associates keys with the values according to tree T. In other words, BST_insert(T, k, v) = update(BST_search(T), k, v).

Write the BST_search and BST_insert functions

The BST_search function is recursive over the Tree parameter. If the tree is empty, the result is none. Otherwise, we compare the key k with the key in the current node x. If they are equal, return the value in the current node; if k is less-than, recursively search the left subtree; if k is greater-than, recursively search the right subtree.

The BST_insert function follows a similar control structure: recursive over the Tree parameter followed by an if-then-else based on the key k and the key of the current node. However, BST_insert returns a new tree that contains the specified key and value. When the key k is already in the tree, BST_insert overrides the current value with the new value, as implied by the specification above.

function BST_insert(Tree<Pair<Nat,Nat>>, Nat, Nat) -> Tree<Pair<Nat,Nat>> {
  BST_insert(EmptyTree, k, v) = TreeNode(EmptyTree, pair(k, v), EmptyTree)
  BST_insert(TreeNode(L, x, R), k, v) =
    if k = first(x) then
      TreeNode(L, pair(k, v), R)
    else if k < first(x) then
      TreeNode(BST_insert(L, k, v), x, R)
    else
      TreeNode(L, x, BST_insert(R, k, v))
}

Test

We test the correctness of the EmptyTree, BST_search, and BST_insert operations by making sure they behave according to their specification. Starting with EmptyTree, the result of BST_search with any key should be none.

assert BST_search(EmptyTree)(5) = none

After inserting key 10 with value 32, the result of BST_search on 10 should be 32. For other keys, such as 5, the result should be the same as for EmptyTree.

define BST_a = BST_insert(EmptyTree, 10, 32)
assert BST_search(BST_a)(10) = just(32)
assert BST_search(BST_a)(5) = none

The story is similar for inserting key 6 with value 85.

define BST_b = BST_insert(BST_a, 6, 85)
assert BST_search(BST_b)(6) = just(85)
assert BST_search(BST_b)(10) = just(32)
assert BST_search(BST_b)(5) = none

If we insert with the same key 6 but a different value 59, the result of BST_search for 6 should be the new value 59. For other keys, the result of BST_search remains the same.

define BST_c = BST_insert(BST_b, 6, 59)
assert BST_search(BST_c)(6) = just(59)
assert BST_search(BST_c)(10) = just(32)
assert BST_search(BST_c)(5) = none

Prove

Starting with EmptyTree, we prove that applying BST_search produces an empty map.

theorem BST_search_EmptyTree: 
  BST_search(EmptyTree) = λk{none}
proof
  extensionality
  arbitrary k:Nat
  conclude BST_search(EmptyTree)(k) = none
      by definition BST_search
end

The main correctness theorem is to show that BST_insert behaves the same as update. That is to say, applying BST_insert to a tree followed by BST_search is the same as first applying BST_search and then applying update.

theorem BST_search_insert_udpate: all T:Tree<Pair<Nat,Nat>>. all k:Nat, v:Nat.
  BST_search(BST_insert(T, k, v)) = update(BST_search(T), k, just(v))

The proof is by induction on the tree. For the case T = EmptyTree, we start by using extensionality to apply both sides of the equation to an arbitrary number i. We then expand BST_insert(EmptyTree, k, v).

    // <<BST_search_insert_empty_ext>> =
    arbitrary k:Nat, v:Nat
    extensionality
    arbitrary i:Nat
    suffices BST_search(TreeNode(EmptyTree, pair(k, v), EmptyTree))(i)
           = update(BST_search(EmptyTree), k, just(v))(i)   with definition BST_insert

Looking at the definition of BST_search, the left-hand side will either be none or just(v) depending on whether i is less-than, equal to, or greater than k. So we proceed with case analysis using the trichotomy theorem from Nat.pf.

    // <<BST_search_insert_empty_tri>> =
    cases trichotomy[i][k]
    case i_less_k: i < k {
      <<BST_search_insert_empty_less>>
    }
    case i_eq_k: i = k {
      <<BST_search_insert_empty_equal>>
    }
    case i_greater_k: k < i {
      <<BST_search_insert_empty_greater>>
    }

Indeed, when i is less than k, both the left-hand side and the right-hand side are equal to none.

    // <<BST_search_insert_empty_less>> =
    have not_i_eq_k: not (i = k)   by apply less_not_equal to i_less_k
    equations
        BST_search(TreeNode(EmptyTree, pair(k, v), EmptyTree))(i)
         = @none<Nat>
            by definition {BST_search, BST_search, first, second}
               and rewrite not_i_eq_k | i_less_k
     ... = update(BST_search(EmptyTree), k, just(v))(i)
            by definition {BST_search, update} and rewrite not_i_eq_k 

When i is equal to k, both sides are equal to just(v).

    // <<BST_search_insert_empty_equal>> =
    equations
        BST_search(TreeNode(EmptyTree, pair(k, v), EmptyTree))(i)
         = just(v)
            by definition {BST_search, first, second} and rewrite i_eq_k
     ... = update(BST_search(EmptyTree), k, just(v))(i)
            by definition {BST_search, update} and rewrite i_eq_k

When i is greater than k, both side are equal to none.

    // <<BST_search_insert_empty_greater>> =
    have not_k_eq_i: not (k = i)  by apply less_not_equal to i_greater_k
    have not_i_eq_k: not (i = k)  by suppose ik apply not_k_eq_i to symmetric ik
    have not_i_less_k: not (i < k) 
        by apply less_implies_not_greater to i_greater_k
    equations
        BST_search(TreeNode(EmptyTree, pair(k, v), EmptyTree))(i)
         = @none<Nat>
            by definition {BST_search, BST_search, first, second}
               and rewrite not_i_eq_k | not_i_less_k
     ... = update(BST_search(EmptyTree), k, just(v))(i)
            by definition {BST_search, update}
               and rewrite not_i_eq_k 

Next we consider the case where T = TreeNode(L, x, R). Again we begin with extensionality.

    // <<BST_search_insert_node_ext>> =
    arbitrary k:Nat, v:Nat
    extensionality
    arbitrary i:Nat
    suffices BST_search(BST_insert(TreeNode(L, x, R), k, v))(i) 
           = update(BST_search(TreeNode(L, x, R)), k, just(v))(i)   by .

Looking at BST_insert(TreeNode(L, x, R), k, v), its result will depend on whether k is less than, equal to, or greater than first(x). So we proceed by cases, using the trichotomy theorem from Nat.py.

    // <<BST_search_insert_node_tri>> =
    cases trichotomy[k][first(x)]
    case k_less_fx: k < first(x) {
      <<BST_search_insert_node_k_less_fx>>
    }
    case k_eq_fx: k = first(x) {
      <<BST_search_insert_node_k_equal_fx>>
    }
    case k_greater_fx: first(x) < k {
      <<BST_search_insert_node_k_greater_fx>>
    }

For the case k < first(x), we have

  BST_insert(TreeNode(L, x, R), k, v) 
= BST_search(TreeNode(BST_insert(L, k, v), x, R))(i)

so it suffices to prove the following.

    // <<BST_search_insert_node_k_less_fx_suffices>> =
    have not_k_eq_fx: not (k = first(x))   by apply less_not_equal to k_less_fx
    suffices BST_search(TreeNode(BST_insert(L, k, v), x, R))(i)
           = update(BST_search(TreeNode(L, x, R)), k, just(v))(i)
                with definition {BST_insert} and rewrite not_k_eq_fx | k_less_fx

The result of BST_search(TreeNode(BST_insert(L, k, v), x, R))(i) depends on the relationship between i and first(x), so we again proceed by cases using the trichotomy theorem. There sure are a lot of cases in this proof!

    // <<BST_search_insert_node_k_less_fx_tri>> =
    cases trichotomy[i][first(x)]
    case i_less_fx: i < first(x) {
      <<BST_search_insert_node_k_less_fx_i_less_fx>>
    }
    case i_eq_fx: i = first(x) {
      <<BST_search_insert_node_k_less_fx_i_eq_fx>>
    }
    case fx_less_i: first(x) < i {
      <<BST_search_insert_node_k_less_fx_i_greater_fx>>
    }

For the case i < first(x), we proceed by the following several steps of equational reasoning, shown below. The key step is applying the induction hypothesis for the left subtree L.

    // <<BST_search_insert_node_k_less_fx_i_less_fx>> =
    have not_i_eq_fx: not (i = first(x)) by apply less_not_equal to i_less_fx
    equations
          BST_search(TreeNode(BST_insert(L, k, v), x, R))(i) 
        = BST_search(BST_insert(L, k, v))(i)
            by definition{BST_search} and rewrite not_i_eq_fx | i_less_fx
    ... = update(BST_search(L), k, just(v))(i)
            by rewrite IH_L[k,v]
    ... = update(BST_search(TreeNode(L, x, R)), k, just(v))(i) by
            switch i = k {
              case true suppose ik_true {
                definition {BST_search,update} and rewrite ik_true
              }
              case false suppose ik_false {
                definition {BST_search,update}
                and rewrite ik_false | not_i_eq_fx | i_less_fx
              }
            }

For the case i = first(x), both sides simplify to just(second(x)).

    // <<BST_search_insert_node_k_less_fx_i_eq_fx>> =
    have not_fx_eq_k: not (first(x) = k)
      by suppose fx_eq_k
         conclude false by rewrite not_k_eq_fx in symmetric fx_eq_k 
    equations
          BST_search(TreeNode(BST_insert(L, k, v), x, R))(i) 
        = just(second(x))
            by definition {BST_search} and rewrite i_eq_fx
    ... = update(BST_search(TreeNode(L, x, R)), k, just(v))(i)
            by definition {BST_search,update} and rewrite i_eq_fx | not_fx_eq_k

For the case first(x) < i, both side are equal to BST_search(R)(i). because we know that i ≠ k.

    // <<BST_search_insert_node_k_less_fx_i_greater_fx>> =
    have not_i_eq_fx: not (i = first(x))
      by suppose i_eq_fx
         apply (apply less_not_equal to fx_less_i) to symmetric i_eq_fx
    have not_i_less_fx: not (i < first(x))
      by apply less_implies_not_greater to fx_less_i
    have not_i_eq_k: not (i = k)
      by suppose i_eq_k
         have fx_less_k: first(x) < k   by rewrite i_eq_k in fx_less_i
         have not_k_less_fx: not (k < first(x)) 
             by apply less_implies_not_greater to fx_less_k
         conclude false by apply not_k_less_fx to rewrite k_less_fx
    equations
          BST_search(TreeNode(BST_insert(L, k, v), x, R))(i) 
        = BST_search(R)(i)
            by definition BST_search and rewrite not_i_eq_fx | not_i_less_fx
    ... = update(BST_search(TreeNode(L, x, R)), k, just(v))(i)
            by definition {BST_search, update}
               and rewrite not_i_eq_k | not_i_eq_fx | not_i_less_fx

This completes the proof of the case for k < first(x).

    <<BST_search_insert_node_k_less_fx_suffices>>
    <<BST_search_insert_node_k_less_fx_tri>>

Next consider the case for k = first(x). We have

  BST_insert(TreeNode(L, x, R), k, v) 
= TreeNode(L, pair(k, v), R)

so it suffices to prove the following

    // <<BST_search_insert_node_k_equal_fx_suffices>> =
    suffices BST_search(TreeNode(L, pair(k, v), R))(i) 
           = update(BST_search(TreeNode(L, x, R)), k, just(v))(i)
                by definition BST_insert and rewrite k_eq_fx

Looking at the definition of BST_search, the result of BST_search(TreeNode(L, pair(k, v), R))(i) will depend on the relationship between i and k. So we proceed by cases, using the trichotomy theorem.

    // <<BST_search_insert_node_k_equal_fx_tri>> =
    cases trichotomy[i][k]
    case i_less_k: i < k {
      <<BST_search_insert_node_k_equal_fx_i_less_k>>
    }
    case i_eq_k: i = k {
      <<BST_search_insert_node_k_equal_fx_i_eq_k>>
    }
    case k_less_i: k < i {
      <<BST_search_insert_node_k_equal_fx_i_greater_k>>
    }

When i < k, both sides of the equation are equal to BST_search(L)(i).

    // <<BST_search_insert_node_k_equal_fx_i_less_k>> =
    have not_i_eq_k: not (i = k)   by apply less_not_equal to i_less_k
    equations
          BST_search(TreeNode(L, pair(k, v), R))(i) 
        = BST_search(L)(i)
              by definition {BST_search, first}
                 and rewrite not_i_eq_k | i_less_k
    ... = update(BST_search(TreeNode(L, x, R)), k, just(v))(i)
              by definition {update,BST_search}
                 and rewrite symmetric k_eq_fx | not_i_eq_k | i_less_k

When i = k, both sides are equal to just(v).

    // <<BST_search_insert_node_k_equal_fx_i_eq_k>> =
    suffices BST_search(TreeNode(L, pair(k, v), R))(k)
            = update(BST_search(TreeNode(L, x, R)), k, just(v))(k)
            with rewrite i_eq_k
    equations
      BST_search(TreeNode(L, pair(k, v), R))(k)
        = just(v)          by definition {BST_search, first, second}
    ... = update(BST_search(TreeNode(L, x, R)), k, just(v))(k)
                           by definition {BST_search, update}

When i > k, both sides are equal to BST_search(R)(i).

    have not_i_eq_k: not (i = k) 
      by have nki: not (k = i) by apply less_not_equal to k_less_i
         suppose i_eq_k apply nki to symmetric i_eq_k
    have not_i_less_k: not (i < k) 
        by apply less_implies_not_greater to k_less_i
    equations
          BST_search(TreeNode(L, pair(k, v), R))(i) 
        = BST_search(R)(i)
            by definition {BST_search, first, second}
               and rewrite not_i_eq_k | not_i_less_k
    ... = update(BST_search(TreeNode(L, x, R)), k, just(v))(i)
            by definition {update, BST_search}
               and rewrite symmetric k_eq_fx | not_i_eq_k | not_i_less_k

This concludes the proof of the case for k = first(x).

    <<BST_search_insert_node_k_equal_fx_suffices>>
    <<BST_search_insert_node_k_equal_fx_tri>>

The last case to prove is for k > first(x). We leave this as an exercise.

The following puts together the pieces of the proof for BST_search_insert_udpate.

theorem BST_search_insert_udpate: all T:Tree<Pair<Nat,Nat>>. all k:Nat, v:Nat.
  BST_search(BST_insert(T, k, v)) = update(BST_search(T), k, just(v))
proof
  induction Tree<Pair<Nat,Nat>>
  case EmptyTree {
    <<BST_search_insert_empty_ext>>
    <<BST_search_insert_empty_tri>>
  }
  case TreeNode(L, x, R) suppose IH_L, IH_R {
    <<BST_search_insert_node_ext>>
    <<BST_search_insert_node_tri>>
  }
end

Saturday, July 20, 2024

Binary Trees with In-order Iterators (Part 2)

This is the sixth blog post in a series about developing correct implementations of basic data structures and algorithms using the Deduce language and proof checker.

This post continues were we left off from the previous post in which we implemented binary trees and in-order tree iterators.

Our goal in this post is to prove that we correctly implemented the iterator operations:

ti2tree : < E > fn TreeIter<E> -> Tree<E>
ti_first : < E > fn Tree<E>,E,Tree<E> -> TreeIter<E>
ti_get : < E > fn TreeIter<E> -> E
ti_next : < E > fn TreeIter<E> -> TreeIter<E>
ti_index : < E > fn(TreeIter<E>) -> Nat

The first operation, ti2tree, requires us to first obtain a tree iterator, for example, with ti_first, so ti2tree does not have a correctness criteria all of its own, but instead the proof of its correctness will be part of the correctness of the other operations.

So we skip to the proof of correctness for ti_first.

Correctness of ti_first

Let us make explicit the specification of ti_first:

Specification: The ti_first(A, x, B) function returns an iterator pointing to the first node, with respect to in-order traversal, of the tree TreeNode(A, x, B).

Also, recall that we said the following about ti2tree and ti_first: creating an iterator from a tree using ti_first and then applying ti2tree produces the original tree.

So we have two properties to prove about ti_first. For the first property, we need a way to formalize "the first node with respect to in-order traversal". This is where the ti_index operation comes in. If ti_first returns the first node, then its index should be 0. (One might worry that if ti_index is incorrect, then this property would not force ti_first to be correct. Not to worry, we will prove that ti_index is correct!) So we have the following theorem:

theorem ti_first_index: all E:type, A:Tree<E>, x:E, B:Tree<E>.
  ti_index(ti_first(A, x, B)) = 0
proof
  arbitrary E:type, A:Tree<E>, x:E, B:Tree<E>
  definition ti_first
  ?
end

After expanding the definition of ti_first, we are left with the following goal. So we need to prove a lemma about the first_path auxiliary function.

    ti_index(first_path(A,x,B,empty)) = 0

Here is a first attempt to formulate the lemma.

lemma first_path_index: all E:type. all A:Tree<E>. all y:E, B:Tree<E>.
  ti_index(first_path(A,y,B, empty)) = 0

However, because first_path is recursive, we will need to prove this by recursion on A. But looking at the second clause of in the definition of first_path, the path argument grows, so our induction hypothesis, which requires the path argument to be empty, will not be applicable. As is often the case, we need to generalize the lemma. Let’s replace empty with an arbitrary path as follows.

lemma first_path_index: all E:type. all A:Tree<E>. all y:E, B:Tree<E>, path:List<Direction<E>>.
  ti_index(first_path(A,y,B, path)) = 0

But now this lemma is false. Consider the following situation in which the current node y is 5 and the path is L,R (going from node 5 up to node 3).

Diagram for lemma first path index

The index of node 5 is not 0, it is 5! Instead the index of node 5 is equal to the number of nodes that come before 5 according to in-order travesal. We can obtain that portion of the tree using functions that we have already defined, in particular take_path followed by plug_tree. So we can formulate the lemma as follows.

lemma first_path_index: all E:type. all A:Tree<E>. all y:E, B:Tree<E>, path:List<Direction<E>>.
  ti_index(first_path(A,y,B, path)) = num_nodes(plug_tree(take_path(path), EmptyTree))
proof
  arbitrary E:type
  induction Tree<E>
  case EmptyTree {
    arbitrary y:E, B:Tree<E>, path:List<Direction<E>>
    ?
  }
  case TreeNode(L, x, R) suppose IH {
    arbitrary y:E, B:Tree<E>, path:List<Direction<E>>
    ?
  }
end

For the case A = EmptyTree, the goal simply follows from the definitions of first_path, ti_index, and ti_take.

    conclude ti_index(first_path(EmptyTree,y,B,path))
           = num_nodes(plug_tree(take_path(path),EmptyTree))
                by definition {first_path, ti_index, ti_take}.

For the case A = TreeNode(L, x, R), after expanding the definition of first_path, we need to prove:

  ti_index(first_path(L,x,R,node(LeftD(y,B),path)))
= num_nodes(plug_tree(take_path(path),EmptyTree))

But that follows from the induction hypothesis and the definition of take_path.

    definition {first_path}
    equations
          ti_index(first_path(L,x,R,node(LeftD(y,B),path)))
        = num_nodes(plug_tree(take_path(node(LeftD(y,B),path)),EmptyTree))
                by IH[x, R, node(LeftD(y,B), path)]
    ... = num_nodes(plug_tree(take_path(path),EmptyTree))
                by definition take_path.

Here is the completed proof of the first_path_index lemma.

lemma first_path_index: all E:type. all A:Tree<E>. all y:E, B:Tree<E>, path:List<Direction<E>>.
  ti_index(first_path(A,y,B, path)) = num_nodes(plug_tree(take_path(path), EmptyTree))
proof
  arbitrary E:type
  induction Tree<E>
  case EmptyTree {
    arbitrary y:E, B:Tree<E>, path:List<Direction<E>>
    conclude ti_index(first_path(EmptyTree,y,B,path))
           = num_nodes(plug_tree(take_path(path),EmptyTree))
                by definition {first_path, ti_index, ti_take}.
  }
  case TreeNode(L, x, R) suppose IH {
    arbitrary y:E, B:Tree<E>, path:List<Direction<E>>
    definition {first_path}
    equations
          ti_index(first_path(L,x,R,node(LeftD(y,B),path)))
        = num_nodes(plug_tree(take_path(node(LeftD(y,B),path)),EmptyTree))
                by IH[x, R, node(LeftD(y,B), path)]
    ... = num_nodes(plug_tree(take_path(path),EmptyTree))
                by definition take_path.
  }
end

Returning to the proof of ti_first_index, we need to prove that ti_index(first_path(A,x,B,empty)) = 0. So we apply the first_path_index lemma and then the definitions of take_path, plug_tree, and num_nodes. Here is the completed proof of ti_first_index.

theorem ti_first_index: all E:type, A:Tree<E>, x:E, B:Tree<E>.
  ti_index(ti_first(A, x, B)) = 0
proof
  arbitrary E:type, A:Tree<E>, x:E, B:Tree<E>
  definition ti_first
  equations  ti_index(first_path(A,x,B,empty))
           = num_nodes(plug_tree(take_path(empty),EmptyTree))
                       by first_path_index[E][A][x,B,empty]
       ... = 0      by definition {take_path, plug_tree, num_nodes}.
end

Our next task is to prove that creating an iterator from a tree using ti_first and then applying ti2tree produces the original tree.

theorem ti_first_stable: all E:type, A:Tree<E>, x:E, B:Tree<E>.
  ti2tree(ti_first(A, x, B)) = TreeNode(A, x, B)
proof
  arbitrary E:type, A:Tree<E>, x:E, B:Tree<E>
  definition ti_first
  ?
end

After expanding the definition of ti_first, we are left to prove that

ti2tree(first_path(A,x,B,empty)) = TreeNode(A,x,B)

So we need to prove another lemma about first_path and again we need to generalize the empty path to an arbitrary path. Let us consider again the situation where the current node x is 5.

Diagram for lemma first path index

The result of first_path(A,x,B,path) will be the path to node 4, and the result of ti2tree will be the whole tree, not just TreeNode(A,x,B) as in the above equation. However, we can construct the whole tree from the path and TreeNode(A,x,B) using the plug_tree function. So we have the following lemma to prove.

lemma first_path_stable:
  all E:type. all A:Tree<E>. all y:E, B:Tree<E>, path:List<Direction<E>>.
  ti2tree(first_path(A, y, B, path)) = plug_tree(path, TreeNode(A, y, B))
proof
  arbitrary E:type
  induction Tree<E>
  case EmptyTree {
    arbitrary y:E, B:Tree<E>, path:List<Direction<E>>
    ?
  }
  case TreeNode(L, x, R) suppose IH_L, IH_R {
    arbitrary y:E, B:Tree<E>, path:List<Direction<E>>
    ?
  }
end

In the case A = EmptyTree, we prove the equation using the definitions of first_path and ti2tree.

    equations  ti2tree(first_path(EmptyTree,y,B,path))
             = ti2tree(TrItr(path,EmptyTree,y,B))       by definition first_path.
         ... = plug_tree(path,TreeNode(EmptyTree,y,B))  by definition ti2tree.

In the case A = TreeNode(L, x, R), we need to prove that

  ti2tree(first_path(TreeNode(L,x,R),y,B,path))
= plug_tree(path,TreeNode(TreeNode(L,x,R),y,B))

We probably need to expand the definition of first_path, but doing so in your head is hard. So we can instead ask Deduce to do it. We start by constructing an equation with a bogus right-hand side and apply the definition of first_path.

    equations
          ti2tree(first_path(TreeNode(L,x,R),y,B,path))
        = EmptyTree
             by definition first_path ?
    ... = plug_tree(path,TreeNode(TreeNode(L,x,R),y,B))
             by ?

Deduce responds with

incomplete proof
Goal:
    ti2tree(first_path(L,x,R,node(LeftD(y,B),path))) = EmptyTree

in which the left-hand side has expanded the definition of first_path. So we cut and paste that into our proof and move on to the next step.

    equations
          ti2tree(first_path(TreeNode(L,x,R),y,B,path))
        = ti2tree(first_path(L,x,R,node(LeftD(y,B),path)))
             by definition first_path.
    ... = plug_tree(path,TreeNode(TreeNode(L,x,R),y,B))
             by ?

We now have something that matches the induction hypothesis, so we instantiate it and ask Deduce to tell us the new right-hand side.

    equations
          ti2tree(first_path(TreeNode(L,x,R),y,B,path))
        = ti2tree(first_path(L,x,R,node(LeftD(y,B),path)))
             by definition first_path.
    ... = EmptyTree
             by IH_L[x,R,node(LeftD(y,B),path)]
    ... = plug_tree(path,TreeNode(TreeNode(L,x,R),y,B))
             by ?

Deduce responds with

expected
ti2tree(first_path(L,x,R,node(LeftD(y,B),path))) = EmptyTree
but only have
ti2tree(first_path(L,x,R,node(LeftD(y,B),path))) = plug_tree(node(LeftD(y,B),path),TreeNode(L,x,R))

So we cut and paste the right-hand side of the induction hypothesis to replace EmptyTree.

    equations
          ti2tree(first_path(TreeNode(L,x,R),y,B,path))
        = ti2tree(first_path(L,x,R,node(LeftD(y,B),path)))
             by definition first_path.
    ... = plug_tree(node(LeftD(y,B),path),TreeNode(L,x,R))
             by IH_L[x,R,node(LeftD(y,B),path)]
    ... = plug_tree(path,TreeNode(TreeNode(L,x,R),y,B))
             by ?

The final step of the proof is easy; we just apply the definition of plug_tree. Here is the completed proof of first_path_stable.

lemma first_path_stable:
  all E:type. all A:Tree<E>. all y:E, B:Tree<E>, path:List<Direction<E>>.
  ti2tree(first_path(A, y, B, path)) = plug_tree(path, TreeNode(A, y, B))
proof
  arbitrary E:type
  induction Tree<E>
  case EmptyTree {
    arbitrary y:E, B:Tree<E>, path:List<Direction<E>>
    equations  ti2tree(first_path(EmptyTree,y,B,path))
             = ti2tree(TrItr(path,EmptyTree,y,B))       by definition first_path.
         ... = plug_tree(path,TreeNode(EmptyTree,y,B))  by definition ti2tree.
  }
  case TreeNode(L, x, R) suppose IH_L, IH_R {
    arbitrary y:E, B:Tree<E>, path:List<Direction<E>>
    equations
          ti2tree(first_path(TreeNode(L,x,R),y,B,path))
        = ti2tree(first_path(L,x,R,node(LeftD(y,B),path)))
             by definition first_path.
    ... = plug_tree(node(LeftD(y,B),path),TreeNode(L,x,R))
             by IH_L[x,R,node(LeftD(y,B),path)]
    ... = plug_tree(path,TreeNode(TreeNode(L,x,R),y,B))
             by definition plug_tree.
  }
end

Returning to the ti_first_stable theorem, the equation follows from our first_path_stable lemma and the definition of plug_tree.

theorem ti_first_stable: all E:type, A:Tree<E>, x:E, B:Tree<E>.
  ti2tree(ti_first(A, x, B)) = TreeNode(A, x, B)
proof
  arbitrary E:type, A:Tree<E>, x:E, B:Tree<E>
  definition ti_first
  equations  ti2tree(first_path(A,x,B,empty))
           = plug_tree(empty,TreeNode(A,x,B))  by first_path_stable[E][A][x,B,empty]
       ... = TreeNode(A,x,B)                   by definition plug_tree.
end

Correctness of ti_next

We start by writing down a more careful specification of ti_next.

Specification: The ti_next(iter) operation returns an iterator whose position is one more than the position of iter with respect to in-order traversal, assuming the iter is not at the end of the in-order traversal.

To make this specification formal, we can again use ti_index to talk about the position of the iterator. So we begin to prove the following theorem ti_next_index, taking the usual initial steps in the proof as guided by the formula to be proved and the definition of ti_next, which performs a switch on the right child R of the current node.

theorem ti_next_index: all E:type, iter : TreeIter<E>.
  if suc(ti_index(iter)) < num_nodes(ti2tree(iter))
  then ti_index(ti_next(iter)) = suc(ti_index(iter))
proof
  arbitrary E:type, iter : TreeIter<E>
  suppose prem: suc(ti_index(iter)) < num_nodes(ti2tree(iter))
  switch iter {
    case TrItr(path, L, x, R) suppose iter_eq {
      definition ti_next
      switch R {
        case EmptyTree suppose R_eq {
          ?
        }
        case TreeNode(RL, y, RR) suppose R_eq {
          ?
        }
      }
    }
  }
end

In the case R = EmptyTree, ti_next calls the auxiliary function next_up and we need to prove.

ti_index(next_up(path,L,x,EmptyTree)) = suc(ti_index(TrItr(path,L,x,EmptyTree)))

As usual, we must create a lemma that generalizes this equation.

Proving the next_up_index lemma

Looking at the definition of next_up, we see that the recursive call grows the fourth argument, so we must replace the EmptyTree in the needed equation with an arbitrary tree R:

ti_index(next_up(path,L,x,R)) = suc(ti_index(TrItr(path,L,x,R)))

But this equation is not true in general. Consider the situation below where the current node x is node 1 in our example tree. The index of the next_up from node 1 is 3, but the index of node 1 is 1 and of course, adding one to that is 2, not 3!

Diagram for path to node 1

So we need to change this equation to account for the situation where R is not empty, but instead an arbitrary subtree. The solution is to add the number of nodes in R to the right-hand side:

ti_index(next_up(path,L,x,R)) = suc(ti_index(TrItr(path,L,x,R))) + num_nodes(R)

One more addition is necessary to formulate the lemma. The above equation is only meaningful when the index on the right-hand side is in bounds. That is, it must be smaller than the number of nodes in the tree. So we formula the lemma next_up_index as follows and take a few obvious steps into the proof.

lemma next_up_index: all E:type. all path:List<Direction<E>>. all A:Tree<E>, x:E, B:Tree<E>.
  if suc(ti_index(TrItr(path, A, x, B)) + num_nodes(B)) < num_nodes(ti2tree(TrItr(path, A, x, B)))
  then ti_index(next_up(path, A, x, B)) = suc(ti_index(TrItr(path, A,x,B)) + num_nodes(B))
proof
  arbitrary E:type
  induction List<Direction<E>>
  case empty {
    arbitrary A:Tree<E>, x:E, B:Tree<E>
    suppose prem: suc(ti_index(TrItr(empty,A,x,B)) + num_nodes(B)) 
                  < num_nodes(ti2tree(TrItr(empty,A,x,B)))
    ?
  }
  case node(f, path') suppose IH {
    arbitrary A:Tree<E>, x:E, B:Tree<E>
    suppose prem
    switch f {
      case LeftD(y, R) {
        ?
      }
      case RightD(L, y) suppose f_eq {
        ?
      }
    }
  }
end

In the case path = empty, the premise is false because there are no nodes that come afterwards in the in-order traversal. In particular, the premise implies the following contradictory inequality.

    have AB_l_AB: suc(num_nodes(A) + num_nodes(B)) < suc(num_nodes(A) + num_nodes(B))
      by definition {ti_index, ti_take, take_path, plug_tree, ti2tree, num_nodes} 
         in prem
    conclude false  by apply less_irreflexive to AB_l_AB

Next consider the case path = node(LeftD(y, R), path'). After expanding all the relevant definitions, we need to prove that

  num_nodes(plug_tree(take_path(path'), TreeNode(A,x,B))) 
= suc(num_nodes(plug_tree(take_path(path'), A)) + num_nodes(B))

We need a lemma that relates num_nodes and plug_tree. So we pause the current proof for the following exercise.

Exercise: prove the num_nodes_plug lemma

lemma num_nodes_plug: all E:type. all path:List<Direction<E>>. all t:Tree<E>.
  num_nodes(plug_tree(path, t)) = num_nodes(plug_tree(path, EmptyTree)) + num_nodes(t)

Back to the next_up_index lemma

We use num_nodes_plug on both the left and right-hand sides of the equation, and apply the definition of num_nodes.

    rewrite num_nodes_plug[E][take_path(path')][TreeNode(A,x,B)]
    rewrite num_nodes_plug[E][take_path(path')][A]
    definition num_nodes

After that it suffices to prove the following.

  num_nodes(plug_tree(take_path(path'),EmptyTree)) + suc(num_nodes(A) + num_nodes(B)) 
= suc((num_nodes(plug_tree(take_path(path'),EmptyTree)) + num_nodes(A)) + num_nodes(B))

This equation is rather big, so let’s squint at it by giving names to its parts. (This is a new version of define that I’m experimenting with.)

    define_ X = num_nodes(plug_tree(take_path(path'),EmptyTree))
    define_ Y = num_nodes(A)
    define_ Z = num_nodes(B)

Now it’s easy to see that our goal is true using some simple arithmetic.

    conclude X + suc(Y + Z) = suc((X + Y) + Z)
        by rewrite add_suc[X][Y+Z] | add_assoc[X][Y,Z].

Finally, consider the case path = node(RightD(L, y), path'). After expanding the definition of next_up, we need to prove

  ti_index(next_up(path',L,y,TreeNode(A,x,B))) 
= suc(ti_index(TrItr(node(RightD(L,y),path'),A,x,B)) + num_nodes(B))

The left-hand side matches the induction hypothesis, so we have

    equations
      ti_index(next_up(path',L,y,TreeNode(A,x,B))) 
        = suc(ti_index(TrItr(path',L,y,TreeNode(A,x,B))) + num_nodes(TreeNode(A,x,B)))
            by apply IH[L,y,TreeNode(A,x,B)] 
               to definition {ti_index, ti_take, num_nodes, ti2tree} ?
    ... = suc(ti_index(TrItr(node(RightD(L,y),path'),A,x,B)) + num_nodes(B))
            by ?

But we need to prove the premise of the induction hypothesis. We can do that as follows, with many uses of num_nodes_plug and some arithmetic that we package up into lemma XYZW_equal.

    have IH_prem: suc(num_nodes(plug_tree(take_path(path'),L)) 
                      + suc(num_nodes(A) + num_nodes(B))) 
                  < num_nodes(plug_tree(path',TreeNode(L,y,TreeNode(A,x,B))))
      by rewrite num_nodes_plug[E][take_path(path')][L]
          | num_nodes_plug[E][path'][TreeNode(L,y,TreeNode(A,x,B))]
         definition {num_nodes, num_nodes}
         define_ X = num_nodes(plug_tree(take_path(path'),EmptyTree))
         define_ Y = num_nodes(L) define_ Z = num_nodes(A) define_ W = num_nodes(B)
         define_ P = num_nodes(plug_tree(path',EmptyTree))
         suffices suc((X + Y) + suc(Z + W)) < P + suc(Y + suc(Z + W))
         have prem2: suc((X + suc(Y + Z)) + W) < P + suc(Y + suc(Z + W))
           by enable {X,Y,Z,W,P}
              definition {num_nodes, num_nodes} in
              rewrite num_nodes_plug[E][take_path(path')][TreeNode(L,y,A)]
                    | num_nodes_plug[E][path'][TreeNode(L,y,TreeNode(A,x,B))] in
              definition {ti_index, ti_take, take_path, ti2tree, plug_tree} in
              rewrite f_eq in prem
         rewrite XYZW_equal[X,Y,Z,W]
         prem2

Here is the proof of XYZW_equal.

lemma XYZW_equal: all X:Nat, Y:Nat, Z:Nat, W:Nat.
  suc((X + Y) + suc(Z + W)) = suc((X + suc(Y + Z)) + W)
proof
  arbitrary X:Nat, Y:Nat, Z:Nat, W:Nat
  enable {operator+}
  equations
        suc((X + Y) + suc(Z + W))
      = suc(suc(X + Y) + (Z + W))      by rewrite add_suc[X+Y][Z+W].
  ... = suc(suc(((X + Y) + Z) + W))    by rewrite add_assoc[X+Y][Z,W].
  ... = suc(suc((X + (Y + Z)) + W))    by rewrite add_assoc[X][Y,Z].
  ... = suc((X + suc(Y + Z)) + W)      by rewrite add_suc[X][Y+Z].
end

Getting back to the equational proof, it remains to prove that

  suc(ti_index(TrItr(path',L,y,TreeNode(A,x,B))) + num_nodes(TreeNode(A,x,B)))
= suc(ti_index(TrItr(node(RightD(L,y),path'),A,x,B)) + num_nodes(B))

which we can do with yet more uses of num_nodes_plug and XYZW_equal.

    ... = suc(num_nodes(plug_tree(take_path(path'),L)) + suc(num_nodes(A) + num_nodes(B)))
          by definition {ti_index, ti_take, num_nodes}.
    ... = suc((num_nodes(plug_tree(take_path(path'),EmptyTree)) + num_nodes(L))
              + suc(num_nodes(A) + num_nodes(B)))
          by rewrite num_nodes_plug[E][take_path(path')][L].
    ... = suc((num_nodes(plug_tree(take_path(path'),EmptyTree)) 
              + suc(num_nodes(L) + num_nodes(A))) + num_nodes(B))
          by define_ X = num_nodes(plug_tree(take_path(path'),EmptyTree))
             define_ Y = num_nodes(L) define_ Z = num_nodes(A) define_ W = num_nodes(B)
             define_ P = num_nodes(plug_tree(path',EmptyTree))
             conclude suc((X + Y) + suc(Z + W)) = suc((X + suc(Y + Z)) + W)
                 by XYZW_equal[X,Y,Z,W]
    ... = suc(num_nodes(plug_tree(take_path(path'),TreeNode(L,y,A))) + num_nodes(B))
          by rewrite num_nodes_plug[E][take_path(path')][TreeNode(L,y,A)]
             definition {num_nodes, num_nodes}.
    ... = suc(ti_index(TrItr(node(RightD(L,y),path'),A,x,B)) + num_nodes(B))
          by definition {ti_index, ti_take, take_path, plug_tree}.

That completes the last case of the proof of next_up_index. Here’s the completed proof.

lemma next_up_index: all E:type. all path:List<Direction<E>>. all A:Tree<E>, x:E, B:Tree<E>.
  if suc(ti_index(TrItr(path, A, x, B)) + num_nodes(B)) < num_nodes(ti2tree(TrItr(path, A, x, B)))
  then ti_index(next_up(path, A, x, B)) = suc(ti_index(TrItr(path, A,x,B)) + num_nodes(B))
proof
  arbitrary E:type
  induction List<Direction<E>>
  case empty {
    arbitrary A:Tree<E>, x:E, B:Tree<E>
    suppose prem: suc(ti_index(TrItr(empty,A,x,B)) + num_nodes(B)) 
                  < num_nodes(ti2tree(TrItr(empty,A,x,B)))
    have AB_l_AB: suc(num_nodes(A) + num_nodes(B)) < suc(num_nodes(A) + num_nodes(B))
      by definition {ti_index, ti_take, take_path, plug_tree, ti2tree, num_nodes} 
         in prem
    conclude false  by apply less_irreflexive to AB_l_AB
  }
  case node(f, path') suppose IH {
    arbitrary A:Tree<E>, x:E, B:Tree<E>
    suppose prem
    switch f {
      case LeftD(y, R) {
        definition {next_up, ti_index, ti_take, take_path}
        rewrite num_nodes_plug[E][take_path(path')][TreeNode(A,x,B)]
        rewrite num_nodes_plug[E][take_path(path')][A]
        definition num_nodes
        define_ X = num_nodes(plug_tree(take_path(path'),EmptyTree))
        define_ Y = num_nodes(A)
        define_ Z = num_nodes(B)
        conclude X + suc(Y + Z) = suc((X + Y) + Z)
            by rewrite add_suc[X][Y+Z] | add_assoc[X][Y,Z].
      }
      case RightD(L, y) suppose f_eq {
        definition {next_up}
        have IH_prem: suc(num_nodes(plug_tree(take_path(path'),L)) 
                          + suc(num_nodes(A) + num_nodes(B))) 
                      < num_nodes(plug_tree(path',TreeNode(L,y,TreeNode(A,x,B))))
          by rewrite num_nodes_plug[E][take_path(path')][L]
              | num_nodes_plug[E][path'][TreeNode(L,y,TreeNode(A,x,B))]
             definition {num_nodes, num_nodes}
             define_ X = num_nodes(plug_tree(take_path(path'),EmptyTree))
             define_ Y = num_nodes(L) define_ Z = num_nodes(A) define_ W = num_nodes(B)
             define_ P = num_nodes(plug_tree(path',EmptyTree))
             suffices suc((X + Y) + suc(Z + W)) < P + suc(Y + suc(Z + W))
             have prem2: suc((X + suc(Y + Z)) + W) < P + suc(Y + suc(Z + W))
               by enable {X,Y,Z,W,P}
                  definition {num_nodes, num_nodes} in
                  rewrite num_nodes_plug[E][take_path(path')][TreeNode(L,y,A)]
                        | num_nodes_plug[E][path'][TreeNode(L,y,TreeNode(A,x,B))] in
                  definition {ti_index, ti_take, take_path, ti2tree, plug_tree} in
                  rewrite f_eq in prem
             rewrite XYZW_equal[X,Y,Z,W]
             prem2
        equations
              ti_index(next_up(path',L,y,TreeNode(A,x,B))) 
            = suc(ti_index(TrItr(path',L,y,TreeNode(A,x,B))) + num_nodes(TreeNode(A,x,B)))
                by apply IH[L,y,TreeNode(A,x,B)] 
                   to definition {ti_index, ti_take, num_nodes, ti2tree} IH_prem
        ... = suc(num_nodes(plug_tree(take_path(path'),L)) + suc(num_nodes(A) + num_nodes(B)))
              by definition {ti_index, ti_take, num_nodes}.
        ... = suc((num_nodes(plug_tree(take_path(path'),EmptyTree)) + num_nodes(L))
                  + suc(num_nodes(A) + num_nodes(B)))
              by rewrite num_nodes_plug[E][take_path(path')][L].
        ... = suc((num_nodes(plug_tree(take_path(path'),EmptyTree)) 
                  + suc(num_nodes(L) + num_nodes(A))) + num_nodes(B))
              by define_ X = num_nodes(plug_tree(take_path(path'),EmptyTree))
                 define_ Y = num_nodes(L) define_ Z = num_nodes(A) define_ W = num_nodes(B)
                 define_ P = num_nodes(plug_tree(path',EmptyTree))
                 conclude suc((X + Y) + suc(Z + W)) = suc((X + suc(Y + Z)) + W)
                     by XYZW_equal[X,Y,Z,W]
        ... = suc(num_nodes(plug_tree(take_path(path'),TreeNode(L,y,A))) + num_nodes(B))
              by rewrite num_nodes_plug[E][take_path(path')][TreeNode(L,y,A)]
                 definition {num_nodes, num_nodes}.
        ... = suc(ti_index(TrItr(node(RightD(L,y),path'),A,x,B)) + num_nodes(B))
              by definition {ti_index, ti_take, take_path, plug_tree}.
      }
    }
  }
end

Back to the proof of ti_next_index

With the next_up_index lemma complete, we can get back to proving the ti_next_index theorem. Recall that we were in the case R = EmptyTree and needed to prove the following.

ti_index(next_up(path,L,x,EmptyTree)) = suc(ti_index(TrItr(path,L,x,EmptyTree)))

To use the next_up_index lemma, we need to prove its premise:

    have next_up_index_prem:
        suc(ti_index(TrItr(path,L,x,EmptyTree)) + num_nodes(EmptyTree))
        < num_nodes(ti2tree(TrItr(path,L,x,EmptyTree)))
      by enable num_nodes
         rewrite add_zero[ti_index(TrItr(path,L,x,EmptyTree))]
         rewrite iter_eq | R_eq in prem

We can finish the proof of the equation using the definition of num_nodes and the add_zero property.

    equations
          ti_index(next_up(path,L,x,EmptyTree))
        = suc(ti_index(TrItr(path,L,x,EmptyTree)) + num_nodes(EmptyTree))
          by apply next_up_index[E][path][L, x, EmptyTree] to next_up_index_prem
    ... = suc(ti_index(TrItr(path,L,x,EmptyTree)))
          by definition num_nodes
             rewrite add_zero[ti_index(TrItr(path,L,x,EmptyTree))].

The next case in the proof of ti_next_index is for R = TreeNode(RL, y, RR). We need to prove

  ti_index(first_path(RL,y,RR,node(RightD(L,x),path))) 
= suc(ti_index(TrItr(path,L,x,TreeNode(RL,y,RR))))

We can start by applying the first_path_index lemma, which gives us

equations
      ti_index(first_path(RL,y,RR,node(RightD(L,x),path))) 
    = num_nodes(plug_tree(take_path(node(RightD(L,x),path)),EmptyTree))

We have opportunities to expand take_path and then plug_tree.

... = num_nodes(plug_tree(take_path(path),TreeNode(L,x,EmptyTree)))
        by definition {take_path,plug_tree}.

We can separate out the TreeNode(L,x,EmptyTree) using num_nodes_plug.

... = num_nodes(plug_tree(take_path(path),EmptyTree)) + suc(num_nodes(L))
        by rewrite num_nodes_plug[E][take_path(path)][TreeNode(L,x,EmptyTree)]
           definition {num_nodes, num_nodes}
           rewrite add_zero[num_nodes(L)].

Then we can move the L back into the plug_tree with num_nodes_plug.

... = suc(num_nodes(plug_tree(take_path(path),L)))
       by rewrite add_suc[num_nodes(plug_tree(take_path(path),EmptyTree))][num_nodes(L)]
          rewrite num_nodes_plug[E][take_path(path)][L].

We conclude the equational reasoning with the definition of ti_index and ti_take.

... = suc(ti_index(TrItr(path,L,x,TreeNode(RL,y,RR))))
        by definition {ti_index, ti_take}.

Here is the complete proof of ti_next_index.

theorem ti_next_index: all E:type, iter : TreeIter<E>.
  if suc(ti_index(iter)) < num_nodes(ti2tree(iter))
  then ti_index(ti_next(iter)) = suc(ti_index(iter))
proof
  arbitrary E:type, iter : TreeIter<E>
  suppose prem: suc(ti_index(iter)) < num_nodes(ti2tree(iter))
  switch iter {
    case TrItr(path, L, x, R) suppose iter_eq {
      definition ti_next
      switch R {
        case EmptyTree suppose R_eq {
          have next_up_index_prem:
              suc(ti_index(TrItr(path,L,x,EmptyTree)) + num_nodes(EmptyTree))
              < num_nodes(ti2tree(TrItr(path,L,x,EmptyTree)))
            by enable num_nodes
               rewrite add_zero[ti_index(TrItr(path,L,x,EmptyTree))]
               rewrite iter_eq | R_eq in prem
          equations
                ti_index(next_up(path,L,x,EmptyTree))
              = suc(ti_index(TrItr(path,L,x,EmptyTree)) + num_nodes(EmptyTree))
                by apply next_up_index[E][path][L, x, EmptyTree] to next_up_index_prem
          ... = suc(ti_index(TrItr(path,L,x,EmptyTree)))
                by definition num_nodes
                   rewrite add_zero[ti_index(TrItr(path,L,x,EmptyTree))].
        }
        case TreeNode(RL, y, RR) suppose R_eq {
          equations
                ti_index(first_path(RL,y,RR,node(RightD(L,x),path))) 
              = num_nodes(plug_tree(take_path(node(RightD(L,x),path)),EmptyTree))
                  by first_path_index[E][RL][y,RR,node(RightD(L,x),path)]
          ... = num_nodes(plug_tree(take_path(path),TreeNode(L,x,EmptyTree)))
                  by definition {take_path,plug_tree}.
          ... = num_nodes(plug_tree(take_path(path),EmptyTree)) + suc(num_nodes(L))
                  by rewrite num_nodes_plug[E][take_path(path)][TreeNode(L,x,EmptyTree)]
                     definition {num_nodes, num_nodes}
                     rewrite add_zero[num_nodes(L)].
          ... = suc(num_nodes(plug_tree(take_path(path),L)))
                 by rewrite add_suc[num_nodes(plug_tree(take_path(path),EmptyTree))][num_nodes(L)]
                    rewrite num_nodes_plug[E][take_path(path)][L].
          ... = suc(ti_index(TrItr(path,L,x,TreeNode(RL,y,RR))))
                  by definition {ti_index, ti_take}.

        }
      }
   }
  }
end

Proof of ti_next_stable

The second correctness condition for ti_next(iter) is that it is stable with respect to ti2tree. Following the definition of ti_next, we switch on the iterator and then on the right child of the current node.

theorem ti_next_stable: all E:type, iter:TreeIter<E>.
  ti2tree(ti_next(iter)) = ti2tree(iter)
proof
  arbitrary E:type, iter:TreeIter<E>
  switch iter {
    case TrItr(path, L, x, R) {
      switch R {
        case EmptyTree {
          definition {ti2tree, ti_next}
          ?
        }
        case TreeNode(RL, y, RR) {
          definition {ti2tree, ti_next}
          ?
        }
      }
    }
  }
end

For the case R = EmptyTree, we need to prove the following, which amounts to proving that next_up is stable.

ti2tree(next_up(path,L,x,EmptyTree)) = plug_tree(path,TreeNode(L,x,EmptyTree))

We’ll pause the current proof to prove the next_up_stable lemma.

Exercise: next_up_stable lemma

lemma next_up_stable: all E:type. all path:List<Direction<E>>. all A:Tree<E>, y:E, B:Tree<E>.
  ti2tree(next_up(path, A, y, B)) = plug_tree(path, TreeNode(A,y,B))

Back to ti_next_stable

Now we conclude the R = EmptyTree case of the ti_next_stable theorem.

    conclude ti2tree(next_up(path,L,x,EmptyTree))
       = plug_tree(path,TreeNode(L,x,EmptyTree))
      by next_up_stable[E][path][L,x,EmptyTree]

In the case R = TreeNode(RL, y, RR), we need prove the following, which is to say that first_path is stable. Thankfully we already proved that lemma!

    conclude ti2tree(first_path(RL,y,RR,node(RightD(L,x),path))) 
           = plug_tree(path,TreeNode(L,x,TreeNode(RL,y,RR)))
      by rewrite first_path_stable[E][RL][y,RR,node(RightD(L,x),path)]
         definition {plug_tree}.

Here is the completed proof of ti_next_stable.

theorem ti_next_stable: all E:type, iter:TreeIter<E>.
  ti2tree(ti_next(iter)) = ti2tree(iter)
proof
  arbitrary E:type, iter:TreeIter<E>
  switch iter {
    case TrItr(path, L, x, R) {
      switch R {
        case EmptyTree {
          definition {ti2tree, ti_next}
          conclude ti2tree(next_up(path,L,x,EmptyTree))
             = plug_tree(path,TreeNode(L,x,EmptyTree))
            by next_up_stable[E][path][L,x,EmptyTree]
        }
        case TreeNode(RL, y, RR) {
          definition {ti2tree, ti_next}
          conclude ti2tree(first_path(RL,y,RR,node(RightD(L,x),path))) 
                 = plug_tree(path,TreeNode(L,x,TreeNode(RL,y,RR)))
            by rewrite first_path_stable[E][RL][y,RR,node(RightD(L,x),path)]
               definition {plug_tree}.
        }
      }
    }
  }
end

Correctness of ti_get and ti_index

Recall that ti_get(iter) should return the data in the current node of iter and ti_index should return the position of iter as a natural number with respect to in-order traversal. Thus, if we apply in_order to the tree, the element at position ti_index(iter) should be the same as ti_get(iter). So we have the following theorem to prove.

theorem ti_index_get_in_order: all E:type, iter:TreeIter<E>, a:E.
  ti_get(iter) = nth(in_order(ti2tree(iter)), a)(ti_index(iter))
proof
  arbitrary E:type, iter:TreeIter<E>, a:E
  switch iter {
    case TrItr(path, L, x, R) {
      definition {ti2tree, ti_get, ti_index, ti_take}
      ?
    }
  }
end

After expanding with some definitions, we are left to prove

x = nth(in_order(plug_tree(path,TreeNode(L,x,R))),a)
       (num_nodes(plug_tree(take_path(path),L)))

We see num_nodes applied to plug_tree, so we can use the num_nodes_plug lemma

      rewrite num_nodes_plug[E][take_path(path)][L]

The goal now is to prove

x = nth(in_order(plug_tree(path, TreeNode(L,x,R))),a)
       (num_nodes(plug_tree(take_path(path), EmptyTree)) + num_nodes(L))

The next step to take is not so obvious. Perhaps one hint is that we have the following theorem about nth from List.pf that also involves addition in the index argument of nth.

theorem nth_append_back: all T:type. all xs:List<T>. all ys:List<T>, i:Nat, d:T.
  nth(append(xs, ys), d)(length(xs) + i) = nth(ys, d)(i)

So we would need to prove a lemma that relates in_order and plug_tree to append. Now the take_path function returns the part of the tree before the path, so perhaps it can be used to create the xs in nth_append_back. But what about ys? It seems like we need a function that returns the part of the tree after the path. Let us call this function drop_path.

function drop_path<E>(List<Direction<E>>) -> List<Direction<E>> {
  drop_path(empty) = empty
  drop_path(node(f, path')) =
    switch f {
      case RightD(L, x) {
        drop_path(path')
      }
      case LeftD(x, R) {
        node(LeftD(x, R), drop_path(path'))
      }
    }
}

So using take_path and drop_path, we should be able to come up with an equation for in_order(plug_tree(path, TreeNode(A, x, B))). The part of tree before x should be take_path(path) followed by the subtree A. The part of the tree after x should be the subtree B followed by drop_path(path).

lemma in_order_plug_take_drop: all E:type. all path:List<Direction<E>>. all A:Tree<E>, x:E, B:Tree<E>.
  in_order(plug_tree(path, TreeNode(A, x, B)))
  = append(in_order(plug_tree(take_path(path), A)), 
           node(x, in_order(plug_tree(drop_path(path), B))))

It turns out that to prove this, we will also need a lemma about the combination of plug_tree and take_path:

lemma in_order_plug_take: all E:type. all path:List<Direction<E>>. all t:Tree<E>.
  in_order(plug_tree(take_path(path), t)) 
  = append( in_order(plug_tree(take_path(path),EmptyTree)), in_order(t))

and a lemma about the combination of plug_tree and drop_path:

lemma in_order_plug_drop: all E:type. all path:List<Direction<E>>. all t:Tree<E>.
  in_order(plug_tree(drop_path(path), t)) = append( in_order(t), in_order(plug_tree(drop_path(path),EmptyTree)))

Exercise: prove the in_order_plug... lemmas

Prove the three lemmas in_order_plug_take_drop, in_order_plug_take, and in_order_plug_drop.

Back to the proof of ti_index_get_in_order

Our goal was to prove

x = nth(in_order(plug_tree(path,TreeNode(L,x,R))), a)
       (num_nodes(plug_tree(take_path(path),EmptyTree)) + num_nodes(L))

So we use lemma in_order_plug_take_drop to get the following

  in_order(plug_tree(path,TreeNode(L,x,R)))
= append(in_order(plug_tree(take_path(path),L)), node(x, in_order(plug_tree(drop_path(path),R))))

and then lemma in_order_plug_take separates out the L.

  in_order(plug_tree(take_path(path), L))
= append(in_order(plug_tree(take_path(path),EmptyTree)), in_order(L))

So rewriting with the above equations

    rewrite in_order_plug_take_drop[E][path][L,x,R]
    rewrite in_order_plug_take[E][path][L]

transforms our goal to

x = nth(append(append(in_order(plug_tree(take_path(path),EmptyTree)), in_order(L)),
               node(x,in_order(plug_tree(drop_path(path),R)))),a)
       (num_nodes(plug_tree(take_path(path),EmptyTree)) + num_nodes(L))

Recall that our plan is to use the nth_append_back lemma, in which the index argument to nth is length(xs), but in the above we have the index expressed in terms of num_nodes. The following exercise proves a theorem that relates length and in_order to num_nodes.

Exercise: prove the length_in_order theorem

theorem length_in_order: all E:type. all t:Tree<E>.
  length(in_order(t)) = num_nodes(t)

Back to ti_index_get_in_order

Now we rewrite with the length_in_order lemma a couple times, give some short names to these big expressions, and apply length_append from List.pf.

      rewrite symmetric length_in_order[E][L]
            | symmetric length_in_order[E][plug_tree(take_path(path),EmptyTree)]
      define_ X = in_order(plug_tree(take_path(path),EmptyTree))
      define_ Y = in_order(L)
      define_ Z = in_order(plug_tree(drop_path(path),R))
      rewrite symmetric length_append[E][X][Y]

Now we’re in a position to use nth_append_back.

x = nth(append(append(X,Y), node(x, Z)), a)
       (length(append(X,Y)))

In particular, nth_append_back[E][append(X,Y)][node(x,Z), 0, a] gives us

  nth(append(append(X,Y), node(x,Z)),a)(length(append(X,Y)) + 0) 
= nth(node(x,Z),a)(0)

With that we prove the goal using add_zero and the definition of nth.

  conclude x = nth(append(append(X,Y), node(x,Z)), a)(length(append(X,Y)))
    by rewrite (rewrite add_zero[length(append(X,Y))] in
                nth_append_back[E][append(X,Y)][node(x,Z), 0, a])
       definition nth.

Here is the complete proof of ti_index_get_in_order.

theorem ti_index_get_in_order: all E:type, z:TreeIter<E>, a:E.
  ti_get(z) = nth(in_order(ti2tree(z)), a)(ti_index(z))
proof
  arbitrary E:type, z:TreeIter<E>, a:E
  switch z {
    case TrItr(path, L, x, R) {
      definition {ti2tree, ti_get, ti_index, ti_take}
      rewrite num_nodes_plug[E][take_path(path)][L]
      
      suffices x = nth(in_order(plug_tree(path,TreeNode(L,x,R))),a)
                      (num_nodes(plug_tree(take_path(path),EmptyTree)) + num_nodes(L))
      rewrite in_order_plug_take_drop[E][path][L,x,R]
      rewrite in_order_plug_take[E][path][L]
      
      suffices x = nth(append(append(in_order(plug_tree(take_path(path),EmptyTree)),
                                     in_order(L)),
                              node(x,in_order(plug_tree(drop_path(path),R)))),a)
                      (num_nodes(plug_tree(take_path(path),EmptyTree)) + num_nodes(L))
      rewrite symmetric length_in_order[E][L]
            | symmetric length_in_order[E][plug_tree(take_path(path),EmptyTree)]
      define_ X = in_order(plug_tree(take_path(path),EmptyTree))
      define_ Y = in_order(L)
      define_ Z = in_order(plug_tree(drop_path(path),R))
      rewrite symmetric length_append[E][X][Y]
      
      conclude x = nth(append(append(X,Y), node(x,Z)), a)(length(append(X,Y)))
        by rewrite (rewrite add_zero[length(append(X,Y))] in
                    nth_append_back[E][append(X,Y)][node(x,Z), 0, a])
           definition nth.
    }
  }
end

This concludes the proofs of correctness for in-order iterator and the five operations ti2tree, ti_first, ti_get, ti_next, and ti_index.

Exercise: Prove that ti_prev is correct

In the previous post there was an exercise to implement ti_prev, which moves the iterator backwards one position with respect to in-order traversal. This exercise is to prove that your implementation of ti_prev is correct. There are two theorems to prove. The first one makes sure that ti_prev reduces the index of the iterator by one.

theorem ti_prev_index: all E:type, iter : TreeIter<E>.
  if 0 < ti_index(iter)
  then ti_index(ti_prev(iter)) = pred(ti_index(iter))

The second theorem makes sure that the resulting iterator is still an iterator for the same tree.

theorem ti_prev_stable: all E:type, iter:TreeIter<E>.
  ti2tree(ti_prev(iter)) = ti2tree(iter)

Thursday, July 18, 2024

Binary Trees with In-order Iterators (Part 1)

This is the fifth blog post in a series about developing correct implementations of basic data structures and algorithms using the Deduce language and proof checker.

In this blog post we study binary trees, that is, trees in which each node has at most two children. We study the in-order tree traversal, as that will become important when we study binary search trees. Furthermore, we implement tree iterators that keep track of a location within the tree and can move forward with respect to the in-order traversal. We shall prove that our implementation of tree iterators is correct in Part 2 of this blog post.

Binary Trees

We begin by defining a union for binary trees:

union Tree<E> {
  EmptyTree
  TreeNode(Tree<E>, E, Tree<E>)
}

For example, we can represent the following binary tree

Diagram of a Binary Tree

with a bunch of tree nodes like so:

define T0 = TreeNode(EmptyTree, 0, EmptyTree)
define T2 = TreeNode(EmptyTree, 2, EmptyTree)
define T1 = TreeNode(T0, 1, T2)
define T4 = TreeNode(EmptyTree, 4, EmptyTree)
define T5 = TreeNode(T4, 5, EmptyTree)
define T7 = TreeNode(EmptyTree, 7, EmptyTree)
define T6 = TreeNode(T5, 6, T7)
define T3 = TreeNode(T1, 3, T6)

We define the height of a tree with the following recursive function.

function height<E>(Tree<E>) -> Nat {
  height(EmptyTree) = 0
  height(TreeNode(L, x, R)) = suc(max(height(L), height(R)))
}

The example tree has height 4.

assert height(T3) = 4

We count the number of nodes in a binary tree with the num_nodes function.

function num_nodes<E>(Tree<E>) -> Nat {
  num_nodes(EmptyTree) = 0
  num_nodes(TreeNode(L, x, R)) = suc(num_nodes(L) + num_nodes(R))
}

The example tree has 8 nodes.

assert num_nodes(T3) = 8

In-order Tree Traversal

Now for the main event of this blog post, the in-order tree traversal. The idea of this traversal is that for each node in the tree, we follow this recipe:

  1. process the left subtree
  2. process the current node
  3. process the right subtree

What it means to process a node can be different for different instantiations of the in-order traversal. But to make things concrete, we study an in-order traversal that produces a list. So here is our definition of the in_order function.

function in_order<E>(Tree<E>) -> List<E> {
  in_order(EmptyTree) = empty
  in_order(TreeNode(L, x, R)) = append(in_order(L), node(x, in_order(R)))
}

The result of in_order for T3 is the list 0,1,2,3,4,5,6,7. As you can see, we chose the data values in T3 to match their position within the in-order traversal.

assert in_order(T3) = interval(8, 0)

In-order Tree Iterators

A tree iterator keeps track of a position with a tree. Our goal is to create a data structure to represent a tree iterator and also to implement the following operations on iterators, which we describe in the following paragraph.

ti2tree : < E > fn TreeIter<E> -> Tree<E>
ti_first : < E > fn Tree<E>,E,Tree<E> -> TreeIter<E>
ti_get : < E > fn TreeIter<E> -> E
ti_next : < E > fn TreeIter<E> -> TreeIter<E>
ti_index : < E > fn(TreeIter<E>) -> Nat
  • The ti2tree operator returns the tree that the iterator is traversing.

  • The ti_first operator returns an iterator pointing to the first node (with respect to the in-order traversal) of a non-empty tree. We represent non-empty trees with three things: the left subtree, the data in the root node, and the right subtree.

  • The ti_get operator returns the data of the node at the current position.

  • The ti_next operator moves the iterator forward by one position.

  • The ti_index operator returns the position of the iterator as a natural number.

Here is an example of creating an iterator for T3 and moving it forward.

define iter0 = ti_first(T1, 3, T6)
assert ti_get(iter0) = 0
assert ti_index(iter0) = 0

define iter3 = ti_next(ti_next(ti_next(iter0)))
assert ti_get(iter3) = 3
assert ti_index(iter3) = 3

define iter7 = ti_next(ti_next(ti_next(ti_next(iter3))))
assert ti_get(iter7) = 7
assert ti_index(iter7) = 7

Iterator Representation

We represent a position in the tree by recording a path of left-or-right decisions. For example, to represent the position of node 4 of the example tree, we record the path R,L,L (R for right and L for left).

Diagram of the iterator at position 4

When we come to implement the ti_next operation, we will sometimes need to climb the tree. For example, to get from 4 to 5. To make that easier, we will store the path in reverse. So the path to node 4 will be stored as L,L,R.

It would seem natural to store an iterator’s path separately from the tree, but doing so would complicate many of the upcoming proofs because only certain paths make sense for certain trees. Instead, we combine the path and the tree into a single data structure called a zipper (Huet, The Zipper, Journal of Functional Programming, Vol 7. Issue 5, 1997). The idea is to attach extra data to the left and right decisions and to store the subtree at the current position. So we define a union named Direction with constructors for left and right, and we define a union named TreeIter that contains a path and the non-empty tree at the current position.

union Direction<E> {
  LeftD(E, Tree<E>)
  RightD(Tree<E>, E)
}

union TreeIter<E> {
  TrItr(List<Direction<E>>, Tree<E>, E, Tree<E>)
}

The ti2tree Operation

Of the tree iterator operations, we will first implement ti2tree because it will help to explain this zipper-style representation. We start by defining the auxiliary function plug_tree, which reconstructs a tree from a path and the subtree at the specified position. The plug_tree function is defined by recursion on the path, so it moves upward in the tree with each recursive call. Consider the case for LeftD(x, R) below. To plug tree t into the path node(LeftD(x, R), path'), we used the extra data stored in LeftD(x, R) to create TreeNode(t, x, R) which we then pass to the recursive call, to plug the new tree node into the rest of the path.

function plug_tree<E>(List<Direction<E>>, Tree<E>) -> Tree<E> {
  plug_tree(empty, t) = t
  plug_tree(node(f, path'), t) =
    switch f {
      case LeftD(x, R) {
        plug_tree(path', TreeNode(t, x, R))
      }
      case RightD(L, x) {
        plug_tree(path', TreeNode(L, x, t))
      }
    }
}

The ti2tree operator simply invokes plug_tree.

function ti2tree<E>(TreeIter<E>) -> Tree<E> {
  ti2tree(TrItr(path, L, x, R)) = plug_tree(path, TreeNode(L, x, R))
}

Creating an iterator from a tree using ti_first and then applying ti2tree produces the original tree. Furthermore, moving an iterator does not change the tree that it is traversing, so ti2tree returns T3 for iterators iter0, iter3, and iter7.

assert ti2tree(iter0) = T3
assert ti2tree(iter3) = T3
assert ti2tree(iter7) = T3

The ti_first Operation

Recall that the ti_first operation returns an iterator pointing to the first node (with respect to the in-order traversal) of a non-empty tree. For example, applying ti_first to T3 should give us node 0. The idea to implement ti_first is simple: we walk down the tree going left at each step, until we get to a leaf.

To implement ti_first we define the auxiliary function first_path that takes a non-empty tree and the path-so-far and proceeds going to the left down the tree. (The first_path function will also come in handy when implementing ti_next.)

function first_path<E>(Tree<E>, E, Tree<E>, List<Direction<E>>) -> TreeIter<E> {
  first_path(EmptyTree, x, R, path) = TrItr(path, EmptyTree, x, R)
  first_path(TreeNode(LL, y, LR), x, R, path) = first_path(LL, y, LR, node(LeftD(x, R), path))
}

We implement ti_first simply as a call to first_path where the path-so-far is empty.

define ti_first : < E > fn Tree<E>,E,Tree<E> -> TreeIter<E>
    = λ L,x,R { first_path(L, x, R, empty) }

As promised above, applying ti_first to T3 gives us node 0.

assert ti_get(ti_first(T1, 3, T6)) = 0

The ti_get Operation

Recall that the ti_get operator should return the data of the node at the current position. This is straightforward to implement because that data is stored directly in the tree iterator.

function ti_get<E>(TreeIter<E>) -> E {
  ti_get(TrItr(path, L, x, R)) = x
}

The ti_next Operation

Recall that the ti_next operator moves the iterator forward by one position with respect to the in-order traversal. This operation is non-trivial to implement. Consider again our example tree.

Diagram of a Binary Tree

Suppose the current node is 2. Then the next node is 3, which requires climbing a fair ways up the tree. On the other hand, if the current node is 3, then the next node is 4, way back down the tree. So there are two different scenarios that we need to handle.

  1. If the current node has a right child, then the next node is the first node of the right child’s subtree (with respect to in-order traversal). For example, node 3 has right child 6, and the first node of that subtree is 4.

  2. If the current node does not have a right child, then the next node is the ancestor after the first left branch. For example, node 2 does not have a right child, so we go up the tree. We go up to 1 via a right branch and then up to 3 via a left branch, so 3 is the next node of 2.

For (1) we already have first_path, so we just need an auxiliary function for (2), which we call next_up. This function takes a path and the current non-empty subtree and returns the iterator for the next position. If the direction is RightD, we keep going up the tree. If the direction is LeftD(x, R), we stop and return an iterator for the parent node x.

function next_up<E>(List<Direction<E>>, Tree<E>, E, Tree<E>) -> TreeIter<E> {
  next_up(empty, A, z, B) = TrItr(empty, A, z, B)
  next_up(node(f, path'), A, z, B) =
    switch f {
      case RightD(L, x) {
        next_up(path', L, x, TreeNode(A, z, B))
      }
      case LeftD(x, R) {
        TrItr(path', TreeNode(A, z, B), x, R)
      }
    }
}

Now that we have both next_up and first_path, we implement ti_next by checking whether the right child R is empty. If it is, we invoke next_up, and if not, we invoke first_path.

function ti_next<E>(TreeIter<E>) -> TreeIter<E> {
  ti_next(TrItr(path, L, x, R)) =
    switch R {
      case EmptyTree {
        next_up(path, L, x, R)
      }
      case TreeNode(RL, y, RR) {
        first_path(RL, y, RR, node(RightD(L, x), path))
      }
    }
}

To see ti_next in action, in the following we go from position 2 up to position 3 and then back down to position 4.

define iter2 = ti_next(ti_next(iter0))
assert ti_get(iter2) = 2

define iter3_ = ti_next(iter2)
assert ti_get(iter3_) = 3

define iter4 = ti_next(iter3_)
assert ti_get(iter4) = 4

The ti_index Operation

Recall that the ti_index operator returns the position of the iterator as a natural number. More specifically, ti_index returns the position of the current node with respect to the in the in-order traversal. The following demonstrates this invariant on iter0 and iter7.

define L0 = in_order(ti2tree(iter0))
define i0 = ti_index(iter0)
assert ti_get(iter0) = nth(L0, 42)(i0)

define L7 = in_order(ti2tree(iter7))
define i7 = ti_index(iter7)
assert ti_get(iter7) = nth(L7, 42)(i7)

The idea for implementing ti_index is that we’ll count how many nodes are in the portion of the tree that comes before the current position. We define an auxiliary function that constructs this portion of the tree, calling it ti_take because it is reminiscent of the take(n, ls) function in List.pf, which returns the prefix of list ls of length n. Furthermore, we use a second auxiliary function named take_path that applies this idea to the path of the iterator. So to implement the take_path function, we throw away the subtrees to the right of the path (by removing LeftD(x, R)) and we keep the subtrees to the left of the path (by keeping Right(L, x)).

function take_path<E>(List<Direction<E>>) -> List<Direction<E>> {
  take_path(empty) = empty
  take_path(node(f, path')) =
    switch f {
      case RightD(L, x) {
        node(RightD(L,x), take_path(path'))
      }
      case LeftD(x, R) {
        take_path(path')
      }
    }
}

We implement ti_take by applying take_path to the path of the iterator, and then plug the left subtree L into the result. (The node x and subtree R are not before node x with respect to in-order traversal.)

function ti_take<E>(TreeIter<E>) -> Tree<E> {
  ti_take(TrItr(path, L, x, R)) = plug_tree(take_path(path), L)
}

Finally, we implement ti_index by counting the number of nodes in the tree returned by ti_take.

define ti_index : < E > fn(TreeIter<E>) -> Nat = λ iter { num_nodes(ti_take(iter))}

Exercise: Implement and test the ti_prev Operation

The ti_prev operation (for previous) moves the iterator backward by one position with respect to in-order traversal.

ti_prev : < E > fn TreeIter<E> -> TreeIter<E>

Implement and test the ti_prev operation.

Conclusion

This completes the implementation of the 5 tree iterator operations. In Part 2 of this blog post, we will prove that these operations are correct.