我在看中序+预序如何构造唯一的二叉树？并认为用 Idris 写一个正式的证明会很有趣。不幸的是，我很早就被卡住了，试图证明在树中找到元素的方法对应于在它的中序遍历中找到它的方法（当然，我还需要为前序遍历这样做） . 任何想法都会受到欢迎。我对一个完整的解决方案不是特别感兴趣——更多的是帮助我们朝着正确的方向开始。
给定
data Tree a = Tip
| Node (Tree a) a (Tree a)
我至少可以通过两种方式将其转换为列表：
inorder : Tree a -> List a
inorder Tip = []
inorder (Node l v r) = inorder l ++ [v] ++ inorder r
或者
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 (::) []
第二种方法似乎使几乎所有事情都变得困难，所以我的大部分努力都集中在第一种上。我这样描述树中的位置：
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
写起来很容易（使用 的第一个定义inorder）
inTreeThenInorder : {x : a} -> (t : Tree a) -> x `InTree` t -> x `Elem` inorder t
结果有一个非常简单的结构，对于证明来说似乎相当不错。
编写一个版本也不是很困难
inorderThenInTree : x `Elem` inorder t -> x `InTree` t
不幸的是，到目前为止，我还没有想出任何方法来编写inorderThenInTree我能够证明是inTreeThenInorder. 我想出的唯一一个用途
listSplit : x `Elem` xs ++ ys -> Either (x `Elem` xs) (x `Elem` ys)
我在试图回到那里时遇到了麻烦。
我尝试了一些一般的想法：
使用
Vect而不是List尝试使计算左侧和右侧的内容变得更容易。我陷入了它的“绿色粘液”中。玩弄树的旋转，甚至证明树根处的旋转会导致有充分根据的关系。（我没有玩下面的旋转，因为我从来没有想出一种方法来使用这些旋转的任何东西）。
尝试用有关如何到达它们的信息来装饰树节点。我并没有在这上面花很长时间，因为我想不出一种方法来通过这种方法表达任何有趣的东西。
试图构建我们将回到我们开始的地方的证明，同时构建这样做的函数。这变得非常混乱，我被困在某个地方或其他地方。