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.
https://glguy.net/agda-tree-inorder-elem/Tree.html
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With