algorithm - inorder + preorder如何构造唯一的二叉树？

Question

最近，我的问题被标记为重复的，比如this，即使没有。所以，让我从下面开始，然后我将解释我的问题。
为什么这个问题不是重复的？
我不想问如何创建一个二叉树时，顺序和前序遍历给出。我要求证明，inorder+preorder遍历定义了一个唯一的二叉树。
现在，回到最初的问题。我去面试，面试官问我这个问题。我被卡住了，无法继续。：。|
问题：给定二叉树的顺序遍历和顺序遍历。证明给定的数据只有一棵二叉树。换句话说，证明两个不同的二叉树不能有相同的序遍历和序遍历。假设树中的所有元素都是唯一的（感谢@envy_intelligence指出了这个假设）。
我试着用例子说服面试官，但面试官要求提供数学/直观的证据。有人能帮我证明吗？

Answer 1

从预排序遍历开始。要么它是空的，在这种情况下就完成了，要么它有第一个元素r0，即树的根。现在搜索顺序遍历以查找r0。左子树都会在该点之前出现，右子树都会在该点之后出现。因此，您可以将该点的顺序遍历分为左子树的顺序遍历il和右子树的顺序遍历ir。
如果il为空，那么剩余的前序遍历属于右子树，您可以继续归纳。如果ir为空，则另一侧也会发生相同的情况。如果两者都不为空，则在预序遍历的剩余部分中找到ir的第一个元素。这将它分为左子树和右子树的一个按序遍历。入职是立即的。
如果有人对一个正式的证明感兴趣，我已经（最后）设法用idris制作了一个。然而，我并没有花时间努力使它可读性很强，所以实际上很难阅读其中的大部分内容。我建议您主要关注顶级类型（即引理、定理和定义），并尽量避免陷入证明（术语）的泥潭。
首先是一些准备工作：

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

现在第二个大的想法：在一棵树中找到一个特定元素的方法。这是基于 Elem输入 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)

然后有一大堆可怕的引理，其中有两个是由eric mertens（ glguy）在 his answer中提出的。
可怕的外稃

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。

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

主要目标！
如果 loc1和 loc2是二叉树， t是内射的， u和 t具有相同的前序和序遍历，则 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

“不重复”的另一种说法
如果树中的两个位置不相等，则可以说树“没有重复项”，这就意味着它们不包含相同的元素。这可以使用 t类型来表示。

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)

这证明 u意味着 NoDups：

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)