How can I establish a bijection between a tree and its traversal?

Question

I was looking at How does inorder+preorder construct unique binary tree? and thought it would be fun to write a formal proof of it in Idris. Unfortunately, I got stuck fairly early on, trying to prove that the ways to find an element in a tree correspond to the ways to find it in its inorder traversal (of course, I'll also need to do that for the preorder traversal). Any ideas would be welcome. I'm not particularly interested in a complete solution—more just help getting started in the right direction.

Given

data Tree a = Tip
            | Node (Tree a) a (Tree a)

I can convert it to a list in at least two ways:

inorder : Tree a -> List a
inorder Tip = []
inorder (Node l v r) = inorder l ++ [v] ++ inorder r

or

foldrTree : (a -> b -> b) -> b -> Tree a -> b
foldrTree c n Tip = n
foldrTree c n (Node l v r) = foldr c (v `c` foldrTree c n r) l
inorder = foldrTree (::) []

The second approach seems to make pretty much everything difficult, so most of my efforts have focused on the first. I describe locations in the tree like this:

data InTree : a -> Tree a -> Type where
  AtRoot : x `InTree` Node l x r
  OnLeft : x `InTree` l -> x `InTree` Node l v r
  OnRight : x `InTree` r -> x `InTree` Node l v r

It's quite easy (using the first definition of inorder) to write

inTreeThenInorder : {x : a} -> (t : Tree a) -> x `InTree` t -> x `Elem` inorder t

and the result has a pretty simple structure that seems reasonably good for proofs.

It's also not terribly difficult to write a version of

inorderThenInTree : x `Elem` inorder t -> x `InTree` t

Unfortunately, I have not, thus far, come up with any way to write a version of inorderThenInTree that I've been able to prove is the inverse of inTreeThenInorder. The only one I've come up with uses

listSplit : x `Elem` xs ++ ys -> Either (x `Elem` xs) (x `Elem` ys)

and I run into trouble trying to get back through there.

A few general ideas I tried:

1. Using Vect instead of List to try to make it easier to work out what's on the left and what's on the right. I got bogged down in the "green slime" of it.

2. Playing around with tree rotations, going as far as to prove that rotation at the root of the tree lead to a well-founded relation. (I didn't play around with rotations below, because I never was able to figure out a way to use anything about these rotations).

3. Trying to decorate tree nodes with information about how to reach them. I didn't spend very long on this because I couldn't think of a way to express anything interesting through that approach.

4. Trying to construct the proof that we're going back where we started while constructing the function that does so. This got pretty messy, and I got stuck somewhere or other.

Answer 1

You were on the right track with your listSplit lemma. You can use that function to learn whether the target element is on the left or right side of a Tree. In the Agda standard library listSplit is called ++⁻

This is the relevant line from my implementation

with ++⁻ (inorder l) x∈t

Here's the complete implementation. I've included it as an external link to avoid unwanted spoilers and also to take advantage of Agda's wonderful HTML hyperlinked, syntax highlighted output. You can click through to see the types and definitions of any of the supporting lemmas.

https://glguy.net/agda-tree-inorder-elem/Tree.html

Answer 2

I wrote inorderToFro and inorderFroTo and the associated lemmas in Idris. Here's the link.

There are a couple of points I can make about your solution (without going much into details):

First, splitMiddle isn't really necessary. If you use a more general Right p = listSplit xs ys loc -> elemAppend xs ys p = loc type for splitRight, then that can cover the same ground.

Second, you could use more with patterns instead of explicit _lem functions; I think it would be clearer and more succinct as well.

Third, you do considerable work proving splitLeft and co. Often it makes sense to move the properties of a function inside the function. So, instead of writing listSplit and the proofs about its result separately, we can modify listSplit to return the needed proofs. This is often simpler to implement. In my solution I used the following types:

data SplitRes : (x : a) -> (xs, ys : List a) -> (e : Elem x (xs ++ ys)) -> Type where
  SLeft  : (e' : Elem x xs) -> e' ++^ ys = e -> SplitRes x xs ys e
  SRight : (e' : Elem x ys) -> xs ^++ e' = e -> SplitRes x xs ys e

listSplit : (xs, ys : List a) -> (e : Elem x (xs ++ ys)) -> SplitRes x xs ys e

I could have also used Either (e' : Elem x xs ** (e' ++^ ys = e)) (e' : Elem x ys ** (xs ^++ e' = e)) instead of SplitRes. However, I ran into problems with Either. It seems to me that higher-order unification in Idris is just too wobbly; I couldn't comprehend why my unsplitLeft function wouldn't typecheck with Either. SplitRes doesn't contain functions in its type, so I guess that's why it works more smoothly.

In general, at this time I recommend Agda over Idris for writing proofs like this. It checks much faster and it's much more robust and convenient. I'm quite amazed you managed to write so much Idris here and for the other question about tree traversals.