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:
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.
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).
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.
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.
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.