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

从顺序遍历开始。它是空的（在这种情况下您已经完成了），或者它有第一个元素

r0

树的根。现在搜索的遍历顺序

r0

。左子树都将在该点之前，而右子树将在该点之后。因此，您可以将该点的有序遍历分为左子树

il

的有序遍历和右子树的有序遍历

ir

。

如果

il

为空，则其余的遍历遍历属于正确的子树，您可以归纳继续。如果

ir

为空，则在另一侧发生相同的事情。如果两者都不为空，则

ir

在剩余遍历中查找第一个元素。这将其分为左子树和右子树之一的预遍历。感应是立即的。

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

首先是一些准备：

module PreInimport 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)

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

可怕的引理

size : Tree a -> Natsize Tip = Zsize (Node l v r) = size l + (S Z + size r)onLeftInjective : onLeft p = onLeft q -> p = qonLeftInjective Refl = ReflonRightInjective : onRight p = onRight q -> p = qonRightInjective Refl = Reflinorder : Tree a -> List ainorder Tip = []inorder (Node l v r) = inorder l ++ [v] ++ inorder rinstance Uninhabited (Here = There y) where  uninhabited Refl impossibleinstance Uninhabited (x `InTree` Tip) where  uninhabited AtRoot impossibleelemAppend : {x : a} -> (ys,xs : List a) -> x `Elem` xs -> x `Elem` (ys ++ xs)elemAppend [] xs xInxs = xInxselemAppend (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 = HereappendElem (y :: zs) ys (There pr) = There (appendElem zs ys pr)tThenInorder : {x : a} -> (t : Tree a) -> x `InTree` t -> x `Elem` inorder ttThenInorder (Node l x r) AtRoot = elemAppend _ _ HeretThenInorder (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 prflistSplit : {x : a} -> (xs,ys : List a) -> x `Elem` (xs ++ ys) -> Either (x `Elem` xs) (x `Elem` ys)listSplit [] ys xelem = Right xelemlistSplit (z :: xs) ys Here = Left HerelistSplit {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 eunsplitRight {xs = []} e = ReflunsplitRight {xs = (x :: xs)} e = rewrite unsplitRight {xs} e in ReflunsplitLeft : {x : a} -> (e : x `Elem` xs) -> listSplit xs ys (appendElem xs ys e) = Left eunsplitLeft {xs = []} Here impossibleunsplitLeft {xs = (x :: xs)} Here = ReflunsplitLeft {xs = (x :: xs)} {ys} (There pr) =  rewrite unsplitLeft {xs} {ys} pr in ReflsplitLeft_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) impossiblesplitLeft_lem2 : Left Here = listSplit_lem x x xs ys (listSplit xs ys z) -> VoidsplitLeft_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) impossiblesplitLeft : {x : a} -> (xs,ys : List a) -> (loc : x `Elem` (xs ++ ys)) -> Left e = listSplit {x} xs ys loc -> appendElem {x} xs ys e = locsplitLeft {e} [] ys loc prf = absurd esplitLeft (x :: xs) ys Here prf = rewrite leftInjective prf in ReflsplitLeft {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) zsplitMiddle_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 = plsplitMiddle_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 = plsplitMiddle_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 prprsplitMiddle : Right Here = listSplit xs (y::ys) loc ->   elemAppend xs (y::ys) Here = locsplitMiddle {xs = []} prf = rightInjective prfsplitMiddle {xs = (x :: xs)} {loc = Here} Refl impossiblesplitMiddle {xs = (x :: xs)} {loc = (There y)} prf = cong $ splitMiddle_lem1 prfsplitRight_lem1 : Right (There pl) = listSplit (q :: xs) (y :: ys) (There z) ->       Right (There pl) = listSplit xs (y :: ys) zsplitRight_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) = locsplitRight {pl = pl} {xs = []} {y = y} {ys = ys} {loc = loc} prf = rightInjective prfsplitRight {pl = pl} {xs = (x :: xs)} {y = y} {ys = ys} {loc = Here} Refl impossiblesplitRight {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) = locinorderFroTo Tip loc = absurd locinorderFroTo (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) = locinorderToFro (Node l v r) (onLeft xInL) =  rewrite unsplitLeft {ys = v :: inorder r} (tThenInorder l xInL)  in cong $ inorderToFro _ xInLinorderToFro (Node l x r) AtRoot =  rewrite unsplitRight {x} {xs = inorder l} {ys = x :: inorder r} (tThenInorder (Node Tip x r) AtRoot)  in ReflinorderToFro {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 apreorder Tip = []preorder (Node l v r) = v :: (preorder l ++ preorder r)tThenPreorder : (t : Tree a) -> x `InTree` t -> x `Elem` preorder ttThenPreorder Tip AtRoot impossibletThenPreorder (Node l x r) AtRoot = HeretThenPreorder (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 = locsplitty {pl = Here} {xs = xs} {ys = (x :: zs)} {loc = loc} prf = splitMiddle prfsplitty {pl = (There x)} {xs = xs} {ys = (y :: zs)} {loc = loc} prf = splitRight prfpreorderFroTo : {x : a} -> (t : Tree a) -> (loc : x `Elem` preorder t) ->     tThenPreorder t (preorderThenT t loc) = locpreorderFroTo Tip Here impossiblepreorderFroTo (Node l x r) Here = ReflpreorderFroTo (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) = locpreorderToFro (Node l x r) AtRoot = ReflpreorderToFro (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)

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

是内射的，如果每当

loc1

并且

loc1

是在中找到值

的方式

，

loc1

必须相等的话

loc2

。

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

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

InjList : List a -> TypeInjList xs = (x : a) -> (loc1, loc2 : x `Elem` xs) -> loc1 = loc2||| If a tree is injective, so is its preorder traversaltreePreInj : (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 traversaltreeInInj : (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 tinjPreTree {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 tinjInTree {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 = yheadsSame Refl = RefltailsSame : {x:a} -> {xs : List a} -> {y : a} -> {ys : List a} -> (x :: xs) = (y :: ys) -> xs = ystailsSame Refl = ReflappendLeftCancel : {xs,ys,ys' : List a} -> xs ++ ys = xs ++ ys' -> ys = ys'appendLeftCancel {xs = []} prf = prfappendLeftCancel {xs = (x :: xs)} prf = appendLeftCancel {xs} (tailsSame prf)lengthDrop : (xs,ys : List a) -> drop (length xs) (xs ++ ys) = yslengthDrop [] ys = RefllengthDrop (x :: xs) ys = lengthDrop xs yslengthTake : (xs,ys : List a) -> take (length xs) (xs ++ ys) = xslengthTake [] ys = RefllengthTake (x :: xs) ys = cong $ lengthTake xs ysappendRightCancel_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) bazappendRightCancel : {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 foolistPartsEqLeft : {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 appeqthereInjective : There loc1 = There loc2 -> loc1 = loc2thereInjective Refl = ReflinjTail : InjList (x :: xs) -> InjList xsinjTail {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) ->         VoidsplitInorder_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 tpreorderLength Tip = ReflpreorderLength (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 tinorderLength Tip = ReflinorderLength (Node l v r) =  rewrite lengthAppend (inorder l) (v :: inorder r)  in rewrite inorderLength l  in rewrite inorderLength r in ReflpreInLength : (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 = yslsplitInorder_lem1 v [] xsr [] ysr xsInj ysInj eq locxs locys = ReflsplitInorder_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 impossiblesplitInorder_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 zsplitInorder_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 = ysrsplitInorder_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 linjLeft {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 = ReflinjRight : {l : Tree a} -> {v : a} -> {r : Tree a} ->InjTree (Node l v r) -> InjTree rinjRight {l} {v} {r} injlvr x loc1 loc2 with (injlvr x (onRight loc1) (onRight loc2))  injRight {l} {v} {r} injlvr x loc1 loc1 | Refl = Refl

主要目标！

如果

和

是二叉树，

则是内射的，并且

和

具有相同的前序和有序遍历，则

和

相等。

travsDet : (t, u : Tree a) -> InjTree t -> preorder t = preorder u -> inorder t = inorder u -> t = u-- The base case--both trees are emptytravsDet Tip Tip x prf prf1 = Refl-- Impossible cases: only one tree is emptytravsDet Tip (Node l v r) x Refl prf1 impossibletravsDet (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 -> TypeNoDups {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 tnoDupsInj 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 = utravsDet2 t u ndt = travsDet t u (noDupsInj t ndt)