从顺序遍历开始。它是空的（在这种情况下您已经完成了），或者它有第一个元素r0树的根。现在搜索的遍历顺序r0。左子树都将在该点之前，而右子树将在该点之后。因此，您可以将该点的有序遍历分为左子树il的有序遍历和右子树的有序遍历ir。

如果il为空，则其余的遍历遍历属于正确的子树，您可以归纳继续。如果ir为空，则在另一侧发生相同的事情。如果两者都不为空，则ir在剩余遍历中查找第一个元素。这将其分为左子树和右子树之一的预遍历。感应是立即的。

如果有人对 正式
证明感兴趣，我（最后）设法在伊德里斯生产了一个。但是，我还没有花时间尝试使其变得非常可读，因此实际上很难阅读很多内容。我建议您主要研究顶级类型（即引理，定理和定义），并尽量避免过于费解证明（术语）。

首先是一些准备：

module PreIn
import Data.List
%default total

现在，第一个真正的想法是：二叉树。

data Tree : Type -> Type where
  Tip : Tree a
  Node : (l : Tree a) -> (v : a) -> (r : Tree a) -> Tree a
%name Tree t, u

现在是第二个大想法：一种在特定树中找到特定元素的方法的想法。这紧密地基于Elemin Data.List，它表示一种在特定 _列表中_查找特定元素的方法。

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)

再就是可怕引理，一对夫妇这些都是由埃里克·梅尔滕斯（建议整体转换glguy）在他的回答我的疑问的。

可怕的引理

size : Tree a -> Nat
size Tip = Z
size (Node l v r) = size l + (S Z + size r)

onLeftInjective : OnLeft p = OnLeft q -> p = q
onLeftInjective Refl = Refl

onRightInjective : OnRight p = OnRight q -> p = q
onRightInjective Refl = Refl

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

instance Uninhabited (Here = There y) where
  uninhabited Refl impossible

instance Uninhabited (x `InTree` Tip) where
  uninhabited AtRoot impossible

elemAppend : {x : a} -> (ys,xs : List a) -> x `Elem` xs -> x `Elem` (ys ++ xs)
elemAppend [] xs xInxs = xInxs
elemAppend (y :: ys) xs xInxs = There (elemAppend ys xs xInxs)

appendElem : {x : a} -> (xs,ys : List a) -> x `Elem` xs -> x `Elem` (xs ++ ys)
appendElem (x :: zs) ys Here = Here
appendElem (y :: zs) ys (There pr) = There (appendElem zs ys pr)

tThenInorder : {x : a} -> (t : Tree a) -> x `InTree` t -> x `Elem` inorder t
tThenInorder (Node l x r) AtRoot = elemAppend _ _ Here
tThenInorder (Node l v r) (OnLeft pr) = appendElem _ _ (tThenInorder _ pr)
tThenInorder (Node l v r) (OnRight pr) = elemAppend _ _ (There (tThenInorder _ pr))

listSplit_lem : (x,z : a) -> (xs,ys:List a) -> Either (x `Elem` xs) (x `Elem` ys)
  -> Either (x `Elem` (z :: xs)) (x `Elem` ys)
listSplit_lem x z xs ys (Left prf) = Left (There prf)
listSplit_lem x z xs ys (Right prf) = Right prf


listSplit : {x : a} -> (xs,ys : List a) -> x `Elem` (xs ++ ys) -> Either (x `Elem` xs) (x `Elem` ys)
listSplit [] ys xelem = Right xelem
listSplit (z :: xs) ys Here = Left Here
listSplit {x} (z :: xs) ys (There pr) = listSplit_lem x z xs ys (listSplit xs ys pr)

mutual
  inorderThenT : {x : a} -> (t : Tree a) -> x `Elem` inorder t -> InTree x t
  inorderThenT Tip xInL = absurd xInL
  inorderThenT {x} (Node l v r) xInL = inorderThenT_lem x l v r xInL (listSplit (inorder l) (v :: inorder r) xInL)

  inorderThenT_lem : (x : a) ->
                     (l : Tree a) -> (v : a) -> (r : Tree a) ->
                     x `Elem` inorder (Node l v r) ->
                     Either (x `Elem` inorder l) (x `Elem` (v :: inorder r)) ->
                     InTree x (Node l v r)
  inorderThenT_lem x l v r xInL (Left locl) = OnLeft (inorderThenT l locl)
  inorderThenT_lem x l x r xInL (Right Here) = AtRoot
  inorderThenT_lem x l v r xInL (Right (There locr)) = OnRight (inorderThenT r locr)

unsplitRight : {x : a} -> (e : x `Elem` ys) -> listSplit xs ys (elemAppend xs ys e) = Right e
unsplitRight {xs = []} e = Refl
unsplitRight {xs = (x :: xs)} e = rewrite unsplitRight {xs} e in Refl

unsplitLeft : {x : a} -> (e : x `Elem` xs) -> listSplit xs ys (appendElem xs ys e) = Left e
unsplitLeft {xs = []} Here impossible
unsplitLeft {xs = (x :: xs)} Here = Refl
unsplitLeft {xs = (x :: xs)} {ys} (There pr) =
  rewrite unsplitLeft {xs} {ys} pr in Refl

splitLeft_lem1 : (Left (There w) = listSplit_lem x y xs ys (listSplit xs ys z)) ->
                 (Left w = listSplit xs ys z)

splitLeft_lem1 {w} {xs} {ys} {z} prf with (listSplit xs ys z)
  splitLeft_lem1 {w}  Refl | (Left w) = Refl
  splitLeft_lem1 {w}  Refl | (Right s) impossible

splitLeft_lem2 : Left Here = listSplit_lem x x xs ys (listSplit xs ys z) -> Void
splitLeft_lem2 {x} {xs} {ys} {z} prf with (listSplit xs ys z)
  splitLeft_lem2 {x = x} {xs = xs} {ys = ys} {z = z} Refl | (Left y) impossible
  splitLeft_lem2 {x = x} {xs = xs} {ys = ys} {z = z} Refl | (Right y) impossible

splitLeft : {x : a} -> (xs,ys : List a) ->
            (loc : x `Elem` (xs ++ ys)) ->
            Left e = listSplit {x} xs ys loc ->
            appendElem {x} xs ys e = loc
splitLeft {e} [] ys loc prf = absurd e
splitLeft (x :: xs) ys Here prf = rewrite leftInjective prf in Refl
splitLeft {e = Here} (x :: xs) ys (There z) prf = absurd (splitLeft_lem2 prf)
splitLeft {e = (There w)} (y :: xs) ys (There z) prf =
  cong $ splitLeft xs ys z (splitLeft_lem1 prf)

splitMiddle_lem3 : Right Here = listSplit_lem y x xs (y :: ys) (listSplit xs (y :: ys) z) ->
                   Right Here = listSplit xs (y :: ys) z

splitMiddle_lem3 {y} {x} {xs} {ys} {z} prf with (listSplit xs (y :: ys) z)
  splitMiddle_lem3 {y = y} {x = x} {xs = xs} {ys = ys} {z = z} Refl | (Left w) impossible
  splitMiddle_lem3 {y = y} {x = x} {xs = xs} {ys = ys} {z = z} prf | (Right w) =
    cong $ rightInjective prf  -- This funny dance strips the Rights off and then puts them
                               -- back on so as to change type.


splitMiddle_lem2 : Right Here = listSplit xs (y :: ys) pl ->
                   elemAppend xs (y :: ys) Here = pl

splitMiddle_lem2 {xs} {y} {ys} {pl} prf with (listSplit xs (y :: ys) pl) proof prpr
  splitMiddle_lem2 {xs = xs} {y = y} {ys = ys} {pl = pl} Refl | (Left loc) impossible
  splitMiddle_lem2 {xs = []} {y = y} {ys = ys} {pl = pl} Refl | (Right Here) = rightInjective prpr
  splitMiddle_lem2 {xs = (x :: xs)} {y = x} {ys = ys} {pl = Here} prf | (Right Here) = (\Refl impossible) prpr
  splitMiddle_lem2 {xs = (x :: xs)} {y = y} {ys = ys} {pl = (There z)} prf | (Right Here) =
    cong $ splitMiddle_lem2 {xs} {y} {ys} {pl = z} (splitMiddle_lem3 prpr)

splitMiddle_lem1 : Right Here = listSplit_lem y x xs (y :: ys) (listSplit xs (y :: ys) pl) ->
                   elemAppend xs (y :: ys) Here = pl

splitMiddle_lem1 {y} {x} {xs} {ys} {pl} prf with (listSplit xs (y :: ys) pl) proof prpr
  splitMiddle_lem1 {y = y} {x = x} {xs = xs} {ys = ys} {pl = pl} Refl | (Left z) impossible
  splitMiddle_lem1 {y = y} {x = x} {xs = xs} {ys = ys} {pl = pl} Refl | (Right Here) = splitMiddle_lem2 prpr

splitMiddle : Right Here = listSplit xs (y::ys) loc ->
              elemAppend xs (y::ys) Here = loc

splitMiddle {xs = []} prf = rightInjective prf
splitMiddle {xs = (x :: xs)} {loc = Here} Refl impossible
splitMiddle {xs = (x :: xs)} {loc = (There y)} prf = cong $ splitMiddle_lem1 prf

splitRight_lem1 : Right (There pl) = listSplit (q :: xs) (y :: ys) (There z) ->
                  Right (There pl) = listSplit xs (y :: ys) z

splitRight_lem1 {xs} {ys} {y} {z} prf with (listSplit xs (y :: ys) z)
  splitRight_lem1 {xs = xs} {ys = ys} {y = y} {z = z} Refl | (Left x) impossible
  splitRight_lem1 {xs = xs} {ys = ys} {y = y} {z = z} prf | (Right x) =
    cong $ rightInjective prf  -- Type dance: take the Right off and put it back on.

splitRight : Right (There pl) = listSplit xs (y :: ys) loc ->
             elemAppend xs (y :: ys) (There pl) = loc
splitRight {pl = pl} {xs = []} {y = y} {ys = ys} {loc = loc} prf = rightInjective prf
splitRight {pl = pl} {xs = (x :: xs)} {y = y} {ys = ys} {loc = Here} Refl impossible
splitRight {pl = pl} {xs = (x :: xs)} {y = y} {ys = ys} {loc = (There z)} prf =
  let rec = splitRight {pl} {xs} {y} {ys} {loc = z} in cong $ rec (splitRight_lem1 prf)

一棵树与其有序遍历之间的对应关系

这些可怕的引理导致了以下关于有序遍历的定理，它们共同证明了在树中查找特定元素的方式与在有序遍历中查找该元素的方式之间的一对一对应关系。

---------------------------
-- tThenInorder is a bijection from ways to find a particular element in a tree
-- and ways to find that element in its inorder traversal. `inorderToFro`
-- and `inorderFroTo` together demonstrate this by showing that `inorderThenT` is
-- its inverse.

||| `tThenInorder t` is a retraction of `inorderThenT t`
inorderFroTo : {x : a} -> (t : Tree a) -> (loc : x `Elem` inorder t) -> tThenInorder t (inorderThenT t loc) = loc
inorderFroTo Tip loc = absurd loc
inorderFroTo (Node l v r) loc with (listSplit (inorder l) (v :: inorder r) loc) proof prf
  inorderFroTo (Node l v r) loc | (Left here) =
    rewrite inorderFroTo l here in splitLeft _ _ loc prf
  inorderFroTo (Node l v r) loc | (Right Here) = splitMiddle prf
  inorderFroTo (Node l v r) loc | (Right (There x)) =
    rewrite inorderFroTo r x in splitRight prf

||| `inorderThenT t` is a retraction of `tThenInorder t`
inorderToFro : {x : a} -> (t : Tree a) -> (loc : x `InTree` t) -> inorderThenT t (tThenInorder t loc) = loc
inorderToFro (Node l v r) (OnLeft xInL) =
  rewrite unsplitLeft {ys = v :: inorder r} (tThenInorder l xInL)
  in cong $ inorderToFro _ xInL
inorderToFro (Node l x r) AtRoot =
  rewrite unsplitRight {x} {xs = inorder l} {ys = x :: inorder r} (tThenInorder (Node Tip x r) AtRoot)
  in Refl
inorderToFro {x} (Node l v r) (OnRight xInR) =
  rewrite unsplitRight {x} {xs = inorder l} {ys = v :: inorder r} (tThenInorder (Node Tip v r) (OnRight xInR))
  in cong $ inorderToFro _ xInR

一棵树与其前序遍历之间的对应关系

然后，可以使用许多相同的引理证明预遍历的相应定理：

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

tThenPreorder : (t : Tree a) -> x `InTree` t -> x `Elem` preorder t
tThenPreorder Tip AtRoot impossible
tThenPreorder (Node l x r) AtRoot = Here
tThenPreorder (Node l v r) (OnLeft loc) = appendElem _ _ (There (tThenPreorder _ loc))
tThenPreorder (Node l v r) (OnRight loc) = elemAppend (v :: preorder l) (preorder r) (tThenPreorder _ loc)

mutual
  preorderThenT : (t : Tree a) -> x `Elem` preorder t -> x `InTree` t
  preorderThenT {x = x} (Node l x r) Here = AtRoot
  preorderThenT {x = x} (Node l v r) (There y) = preorderThenT_lem (listSplit _ _ y)

  preorderThenT_lem : Either (x `Elem` preorder l) (x `Elem` preorder r) -> x `InTree` (Node l v r)
  preorderThenT_lem {x = x} {l = l} {v = v} {r = r} (Left lloc) = OnLeft (preorderThenT l lloc)
  preorderThenT_lem {x = x} {l = l} {v = v} {r = r} (Right rloc) = OnRight (preorderThenT r rloc)

splitty : Right pl = listSplit xs ys loc -> elemAppend xs ys pl = loc
splitty {pl = Here} {xs = xs} {ys = (x :: zs)} {loc = loc} prf = splitMiddle prf
splitty {pl = (There x)} {xs = xs} {ys = (y :: zs)} {loc = loc} prf = splitRight prf

preorderFroTo : {x : a} -> (t : Tree a) -> (loc : x `Elem` preorder t) ->
                tThenPreorder t (preorderThenT t loc) = loc
preorderFroTo Tip Here impossible
preorderFroTo (Node l x r) Here = Refl
preorderFroTo (Node l v r) (There loc) with (listSplit (preorder l) (preorder r) loc) proof spl
  preorderFroTo (Node l v r) (There loc) | (Left pl) =
    rewrite sym (splitLeft {e=pl} (preorder l) (preorder r) loc spl)
    in cong {f = There} $ cong {f = appendElem (preorder l) (preorder r)} (preorderFroTo _ _)
  preorderFroTo (Node l v r) (There loc) | (Right pl) =
      rewrite preorderFroTo r pl in cong {f = There} (splitty spl)

preorderToFro : {x : a} -> (t : Tree a) -> (loc : x `InTree` t) -> preorderThenT t (tThenPreorder t loc) = loc
preorderToFro (Node l x r) AtRoot = Refl
preorderToFro (Node l v r) (OnLeft loc) =
  rewrite unsplitLeft {ys = preorder r} (tThenPreorder l loc)
  in cong {f = OnLeft} (preorderToFro l loc)
preorderToFro (Node l v r) (OnRight loc) =
  rewrite unsplitRight {xs = preorder l} (tThenPreorder r loc)
  in cong {f = OnRight} (preorderToFro r loc)

目前很好？听到那个消息很开心。您寻求的定理正在迅速接近！首先，我们需要树是“内射”的概念，在我看来，这是“没有重复”的最简单概念。如果您不喜欢这个概念，请不要担心。在南方还有另一条路。这说一棵树t是内射的，如果每当loc1并且loc1是在中找到值x的方式t，loc1必须相等的话loc2。

InjTree : Tree a -> Type
InjTree t = (x : a) -> (loc1, loc2 : x `InTree` t) -> loc1 = loc2

我们还希望有与列表相对应的概念，因为我们将证明，当且仅当遍历树时，树才是内射的。这些证明就在下面，并接续于前面。

InjList : List a -> Type
InjList xs = (x : a) -> (loc1, loc2 : x `Elem` xs) -> loc1 = loc2

||| If a tree is injective, so is its preorder traversal
treePreInj : (t : Tree a) -> InjTree t -> InjList (preorder t)
treePreInj {a} t it x loc1 loc2 =
  let foo = preorderThenT {a} {x} t loc1
      bar = preorderThenT {a} {x} t loc2
      baz = it x foo bar
  in rewrite sym $ preorderFroTo t loc1
  in rewrite sym $ preorderFroTo t loc2
  in cong baz

||| If a tree is injective, so is its inorder traversal
treeInInj : (t : Tree a) -> InjTree t -> InjList (inorder t)
treeInInj {a} t it x loc1 loc2 =
  let foo = inorderThenT {a} {x} t loc1
      bar = inorderThenT {a} {x} t loc2
      baz = it x foo bar
  in rewrite sym $ inorderFroTo t loc1
  in rewrite sym $ inorderFroTo t loc2
  in cong baz

||| If a tree's preorder traversal is injective, so is the tree.
injPreTree : (t : Tree a) -> InjList (preorder t) -> InjTree t
injPreTree {a} t il x loc1 loc2 =
  let
    foo = tThenPreorder {a} {x} t loc1
    bar = tThenPreorder {a} {x} t loc2
    baz = il x foo bar
  in rewrite sym $ preorderToFro t loc1
  in rewrite sym $ preorderToFro t loc2
  in cong baz

||| If a tree's inorder traversal is injective, so is the tree.
injInTree : (t : Tree a) -> InjList (inorder t) -> InjTree t
injInTree {a} t il x loc1 loc2 =
  let
    foo = tThenInorder {a} {x} t loc1
    bar = tThenInorder {a} {x} t loc2
    baz = il x foo bar
  in rewrite sym $ inorderToFro t loc1
  in rewrite sym $ inorderToFro t loc2
  in cong baz

更可怕的引理

headsSame : {x:a} -> {xs : List a} -> {y : a} -> {ys : List a} -> (x :: xs) = (y :: ys) -> x = y
headsSame Refl = Refl

tailsSame : {x:a} -> {xs : List a} -> {y : a} -> {ys : List a} -> (x :: xs) = (y :: ys) -> xs = ys
tailsSame Refl = Refl

appendLeftCancel : {xs,ys,ys' : List a} -> xs ++ ys = xs ++ ys' -> ys = ys'
appendLeftCancel {xs = []} prf = prf
appendLeftCancel {xs = (x :: xs)} prf = appendLeftCancel {xs} (tailsSame prf)

lengthDrop : (xs,ys : List a) -> drop (length xs) (xs ++ ys) = ys
lengthDrop [] ys = Refl
lengthDrop (x :: xs) ys = lengthDrop xs ys

lengthTake : (xs,ys : List a) -> take (length xs) (xs ++ ys) = xs
lengthTake [] ys = Refl
lengthTake (x :: xs) ys = cong $ lengthTake xs ys

appendRightCancel_lem : (xs,xs',ys : List a) -> xs ++ ys = xs' ++ ys -> length xs = length xs'
appendRightCancel_lem xs xs' ys eq =
  let foo = lengthAppend xs ys
      bar = replace {P = \b => length b = length xs + length ys} eq foo
      baz = trans (sym bar) $ lengthAppend xs' ys
  in plusRightCancel (length xs) (length xs') (length ys) baz

appendRightCancel : {xs,xs',ys : List a} -> xs ++ ys = xs' ++ ys -> xs = xs'
appendRightCancel {xs} {xs'} {ys} eq with (appendRightCancel_lem xs xs' ys eq)
  | lenEq = rewrite sym $ lengthTake xs ys
            in let foo : (take (length xs') (xs ++ ys) = xs') = rewrite eq in lengthTake xs' ys
            in rewrite lenEq in foo

listPartsEqLeft : {xs, xs', ys, ys' : List a} ->
                  length xs = length xs' ->
                  xs ++ ys = xs' ++ ys' ->
                  xs = xs'
listPartsEqLeft {xs} {xs'} {ys} {ys'} leneq appeq =
  rewrite sym $ lengthTake xs ys
  in rewrite leneq
  in rewrite appeq
  in lengthTake xs' ys'

listPartsEqRight : {xs, xs', ys, ys' : List a} ->
                   length xs = length xs' ->
                   xs ++ ys = xs' ++ ys' ->
                   ys = ys'
listPartsEqRight leneq appeq with (listPartsEqLeft leneq appeq)
  listPartsEqRight leneq appeq | Refl = appendLeftCancel appeq


thereInjective : There loc1 = There loc2 -> loc1 = loc2
thereInjective Refl = Refl

injTail : InjList (x :: xs) -> InjList xs
injTail {x} {xs} xxsInj v vloc1 vloc2 = thereInjective $
    xxsInj v (There vloc1) (There vloc2)

splitInorder_lem2 : ((loc1 : Elem v (v :: xs ++ v :: ysr)) ->
                     (loc2 : Elem v (v :: xs ++ v :: ysr)) -> loc1 = loc2) ->
                    Void
splitInorder_lem2 {v} {xs} {ysr} f =
  let
    loc2 = elemAppend {x=v} xs (v :: ysr) Here
  in (\Refl impossible) $ f Here (There loc2)

-- preorderLength and inorderLength could be proven using the bijections
-- between trees and their traversals, but it's much easier to just prove
-- them directly.

preorderLength : (t : Tree a) -> length (preorder t) = size t
preorderLength Tip = Refl
preorderLength (Node l v r) =
  rewrite sym (plusSuccRightSucc (size l) (size r))
  in cong {f=S} $
     rewrite sym $ preorderLength l
     in rewrite sym $ preorderLength r
     in lengthAppend _ _

inorderLength : (t : Tree a) -> length (inorder t) = size t
inorderLength Tip = Refl
inorderLength (Node l v r) =
  rewrite lengthAppend (inorder l) (v :: inorder r)
  in rewrite inorderLength l
  in rewrite inorderLength r in Refl

preInLength : (t : Tree a) -> length (preorder t) = length (inorder t)
preInLength t = trans (preorderLength t) (sym $ inorderLength t)


splitInorder_lem1 : (v : a) ->
                    (xsl, xsr, ysl, ysr : List a) ->
                    (xsInj : InjList (xsl ++ v :: xsr)) ->
                    (ysInj : InjList (ysl ++ v :: ysr)) ->
                    xsl ++ v :: xsr = ysl ++ v :: ysr ->
                    v `Elem` (xsl ++ v :: xsr) ->
                    v `Elem` (ysl ++ v :: ysr) ->
                    xsl = ysl
splitInorder_lem1 v [] xsr [] ysr xsInj ysInj eq locxs locys = Refl
splitInorder_lem1 v [] xsr (v :: ysl) ysr xsInj ysInj eq Here Here with (ysInj v Here (elemAppend (v :: ysl) (v :: ysr) Here))
  splitInorder_lem1 v [] xsr (v :: ysl) ysr xsInj ysInj eq Here Here | Refl impossible
splitInorder_lem1 v [] xsr (y :: ysl) ysr xsInj ysInj eq Here (There loc) with (headsSame eq)
  splitInorder_lem1 v [] xsr (v :: ysl) ysr xsInj ysInj eq Here (There loc) | Refl = absurd $ splitInorder_lem2 (ysInj v)
splitInorder_lem1 v [] xsr (x :: xs) ysr xsInj ysInj eq (There loc) locys with (headsSame eq)
  splitInorder_lem1 v [] xsr (v :: xs) ysr xsInj ysInj eq (There loc) locys | Refl = absurd $ splitInorder_lem2 (ysInj v)
splitInorder_lem1 v (v :: xs) xsr ysl ysr xsInj ysInj eq Here locys = absurd $ splitInorder_lem2 (xsInj v)
splitInorder_lem1 v (x :: xs) xsr [] ysr xsInj ysInj eq (There y) locys with (headsSame eq)
  splitInorder_lem1 v (v :: xs) xsr [] ysr xsInj ysInj eq (There y) locys | Refl = absurd $ splitInorder_lem2 (xsInj v)
splitInorder_lem1 v (x :: xs) xsr (z :: ys) ysr xsInj ysInj eq (There y) locys with (headsSame eq)
  splitInorder_lem1 v (v :: xs) xsr (_ :: ys) ysr xsInj ysInj eq (There y) Here | Refl = absurd $ splitInorder_lem2 (ysInj v)
  splitInorder_lem1 v (x :: xs) xsr (x :: ys) ysr xsInj ysInj eq (There y) (There z) | Refl = cong {f = ((::) x)} $
                           splitInorder_lem1 v xs xsr ys ysr (injTail xsInj) (injTail ysInj) (tailsSame eq) y z

splitInorder_lem3 : (v : a) ->
                    (xsl, xsr, ysl, ysr : List a) ->
                    (xsInj : InjList (xsl ++ v :: xsr)) ->
                    (ysInj : InjList (ysl ++ v :: ysr)) ->
                    xsl ++ v :: xsr = ysl ++ v :: ysr ->
                    v `Elem` (xsl ++ v :: xsr) ->
                    v `Elem` (ysl ++ v :: ysr) ->
                    xsr = ysr
splitInorder_lem3 v xsl xsr ysl ysr xsInj ysInj prf locxs locys with (splitInorder_lem1 v xsl xsr ysl ysr xsInj ysInj prf locxs locys)
  splitInorder_lem3 v xsl xsr xsl ysr xsInj ysInj prf locxs locys | Refl =
     tailsSame $ appendLeftCancel prf

一个简单的事实：如果一棵树是内射的，那么它的左和右子树也是如此。

injLeft : {l : Tree a} -> {v : a} -> {r : Tree a} ->
          InjTree (Node l v r) -> InjTree l
injLeft {l} {v} {r} injlvr x loc1 loc2 with (injlvr x (OnLeft loc1) (OnLeft loc2))
  injLeft {l = l} {v = v} {r = r} injlvr x loc1 loc1 | Refl = Refl

injRight : {l : Tree a} -> {v : a} -> {r : Tree a} ->
           InjTree (Node l v r) -> InjTree r
injRight {l} {v} {r} injlvr x loc1 loc2 with (injlvr x (OnRight loc1) (OnRight loc2))
  injRight {l} {v} {r} injlvr x loc1 loc1 | Refl = Refl

主要目标！

如果t和u是二叉树，t则是内射的，并且t和u具有相同的前序和有序遍历，则t和u相等。

travsDet : (t, u : Tree a) -> InjTree t -> preorder t = preorder u -> inorder t = inorder u -> t = u
-- The base case--both trees are empty
travsDet Tip Tip x prf prf1 = Refl
-- Impossible cases: only one tree is empty
travsDet Tip (Node l v r) x Refl prf1 impossible
travsDet (Node l v r) Tip x Refl prf1  impossible
-- The interesting case. `headsSame presame` proves
-- that the roots of the trees are equal.
travsDet (Node l v r) (Node t y u) lvrInj presame insame with (headsSame presame)
  travsDet (Node l v r) (Node t v u) lvrInj presame insame | Refl =
    let
      foo = elemAppend (inorder l) (v :: inorder r) Here
      bar = elemAppend (inorder t) (v :: inorder u) Here
      inlvrInj = treeInInj _ lvrInj
      intvuInj : (InjList (inorder (Node t v u))) = rewrite sym insame in inlvrInj
      inorderRightSame = splitInorder_lem3 v (inorder l) (inorder r) (inorder t) (inorder u) inlvrInj intvuInj insame foo bar
      preInL : (length (preorder l) = length (inorder l)) = preInLength l
      inorderLeftSame = splitInorder_lem1 v (inorder l) (inorder r) (inorder t) (inorder u) inlvrInj intvuInj insame foo bar
      inPreT : (length (inorder t) = length (preorder t)) = sym $ preInLength t
      preLenlt : (length (preorder l) = length (preorder t))
               = trans preInL (trans (cong inorderLeftSame) inPreT)
      presame' = tailsSame presame
      baz : (preorder l = preorder t) = listPartsEqLeft preLenlt presame'
      quux : (preorder r = preorder u) = listPartsEqRight preLenlt presame'
-- Putting together the lemmas, we see that the
-- left and right subtrees are equal
      recleft = travsDet l t (injLeft lvrInj) baz inorderLeftSame
      recright = travsDet r u (injRight lvrInj) quux inorderRightSame
    in rewrite recleft in rewrite recright in Refl

“没有重复”的替代概念

如果树中的两个位置不相等，则它们将不具有相同的元素，这可能使人想说一棵树“没有重复项”。可以使用NoDups类型表示。

NoDups : Tree a -> Type
NoDups {a} t = (x, y : a) ->
               (loc1 : x `InTree` t) ->
               (loc2 : y `InTree` t) ->
               Not (loc1 = loc2) ->
               Not (x = y)

之所以足以证明我们需要什么，是因为有一个确定树中两个路径是否相等的过程：

instance DecEq (x `InTree` t) where
  decEq AtRoot AtRoot = Yes Refl
  decEq AtRoot (OnLeft x) = No (\Refl impossible)
  decEq AtRoot (OnRight x) = No (\Refl impossible)
  decEq (OnLeft x) AtRoot = No (\Refl impossible)
  decEq (OnLeft x) (OnLeft y) with (decEq x y)
    decEq (OnLeft x) (OnLeft x) | (Yes Refl) = Yes Refl
    decEq (OnLeft x) (OnLeft y) | (No contra) = No (contra . onLeftInjective)
  decEq (OnLeft x) (OnRight y) = No (\Refl impossible)
  decEq (OnRight x) AtRoot = No (\Refl impossible)
  decEq (OnRight x) (OnLeft y) = No (\Refl impossible)
  decEq (OnRight x) (OnRight y) with (decEq x y)
    decEq (OnRight x) (OnRight x) | (Yes Refl) = Yes Refl
    decEq (OnRight x) (OnRight y) | (No contra) = No (contra . onRightInjective)

这证明这Nodups t意味着InjTree t：

noDupsInj : (t : Tree a) -> NoDups t -> InjTree t
noDupsInj t nd x loc1 loc2 with (decEq loc1 loc2)
  noDupsInj t nd x loc1 loc2 | (Yes prf) = prf
  noDupsInj t nd x loc1 loc2 | (No contra) = absurd $ nd x x loc1 loc2 contra Refl

最后，立即NoDups t完成工作。

travsDet2 : (t, u : Tree a) -> NoDups t -> preorder t = preorder u -> inorder t = inorder u -> t = u
travsDet2 t u ndt = travsDet t u (noDupsInj t ndt)