本文将带您了解关于inorder+preorder如何构造唯一的二叉树？的新内容，同时我们还将为您解释唯一二叉排序树的相关知识，另外，我们还将为您提供关于105.ConstructBinaryTree

本文将带您了解关于inorder + preorder如何构造唯一的二叉树？的新内容，同时我们还将为您解释唯一二叉排序树的相关知识，另外，我们还将为您提供关于105. Construct Binary Tree from Preorder and Inorder Traversal、889. Construct Binary Tree from Preorder and Postorder Traversal、889.Construct Binary Tree from Preorder and Postorder Traversal、Binary Tree Preorder/Postorder Traversal的实用信息。

• inorder + preorder如何构造唯一的二叉树？（唯一二叉排序树）
• 105. Construct Binary Tree from Preorder and Inorder Traversal
• 889. Construct Binary Tree from Preorder and Postorder Traversal
• 889.Construct Binary Tree from Preorder and Postorder Traversal
• Binary Tree Preorder/Postorder Traversal

inorder + preorder如何构造唯一的二叉树？（唯一二叉排序树）

最近，我的问题是重复的标记，像这样，即使他们没有。因此，让我从关注开始，然后我将解释我的问题。

为什么这个问题不是重复的？

我 没有问 给出有序遍历和预遍历遍历时如何创建二叉树。我要求提供证明，即有序+预定序遍历定义了唯一的二叉树。

现在，提出 原始问题 。我去面试，面试官问了这个问题。我被卡住了，无法继续。：|

问题： 给定二叉树的有序和预遍历遍历。证明给定数据 只有一棵二叉树
。换句话说，证明两个不同的二叉树不能具有相同的有序遍历和预遍历遍历。假设树中的所有元素都是唯一的（感谢@envy_intelligence指出了这一假设）。

我尝试使用示例说服面试官，但面试官要求数学/直觉证明。谁能帮我证明一下？

答案1

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

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

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

主要目标！

如果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 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)

105. Construct Binary Tree from Preorder and Inorder Traversal

preorder = [3,9,20,15,7]
inorder = [9,3,7]

    3
   /   9  20
    /     15   7

public TreeNode buildTree(int[] preorder,int[] inorder) {
         int preLength = preorder.length;
         int inLength = inorder.length;
        return buildTree(preorder,preLength-1,inorder,inLength-1);
     }
   
    public TreeNode buildTree(int[] pre,int preStart,int preEnd,int[] in,int inStart,int inEnd){
         if(inStart > inEnd || preStart > preEnd)
             return null;
             
        int rootVal = pre[preStart];
        int rootIndex = 0;
        for(int i = inStart; i <= inEnd; i++){
             if(in[i] == rootVal){
                 rootIndex = i;
                 break;
             }
         }
       
         int len = rootIndex - inStart;
         TreeNode root = new TreeNode(rootVal);
         root.left = buildTree(pre,preStart+1,preStart+len,in,inStart,rootIndex-1);
         root.right = buildTree(pre,preStart+len+1,preEnd,rootIndex+1,inEnd);
       
        return root;
     }

     1       
    / \   
   2   3   
  / \ / \   
 4  5 6  7

对于上图的树来说，
        index: 0 1 2 3 4 5 6
     先序遍历为: 1 2 4 5 3 6 7 
     中序遍历为: 4 2 5 1 6 3 7
为了清晰表示，我给节点上了颜色，红色是根节点，蓝色为左子树，绿色为右子树。
可以发现的规律是：
1. 先序遍历的从左数第一个为整棵树的根节点。
2. 中序遍历中根节点是左子树右子树的分割点。

再看这个树的左子树：
     先序遍历为: 2 4 5 
     中序遍历为: 4 2 5
依然可以套用上面发现的规律。

右子树：
     先序遍历为: 3 6 7 
     中序遍历为: 6 3 7
也是可以套用上面的规律的。

所以这道题可以用递归的方法解决。
具体解决方法是：
通过先序遍历找到第一个点作为根节点，在中序遍历中找到根节点并记录index。
因为中序遍历中根节点左边为左子树，所以可以记录左子树的长度并在先序遍历中依据这个长度找到左子树的区间，用同样方法可以找到右子树的区间。
递归的建立好左子树和右子树就好。

代码如下：

public TreeNode buildTree(int[] preorder,inEnd);
       
        return root;
     }

889. Construct Binary Tree from Preorder and Postorder Traversal

题目

Return any binary tree that matches the given preorder and postorder traversals.

Values in the traversals pre and post are distinct positive integers.

Example 1:

Input: pre = [1,2,4,5,3,6,7], post = [4,5,2,6,7,3,1]
Output: [1,2,3,4,5,6,7]

Note:

• 1 <= pre.length == post.length <= 30
• pre[] and post[] are both permutations of 1, 2, ..., pre.length.
• It is guaranteed an answer exists. If there exists multiple answers, you can return any of them.

讲解

先序遍历和后序遍历无法确定一颗二叉树，所以这里有可能返回多种不同的树，但只要是正确的就行。

解这道题的关键在于分割左右子树，先序遍历中紧跟根节点后的也有可能不是左子树，但如果是这样的话，后续遍历中也不会有左子树，那么右子树的根节点就会在两种遍历中都挨着总根节点。所以思路就出来了，我们在先序遍历中拿到根节点后面的那个节点，然后在后序遍历中找到这个节点，这个点就在后序遍历中分割出了左右子树。

递归之。

Java代码

/**
 * Definition for a binary tree node.
 * public class TreeNode {
 *     int val;
 *     TreeNode left;
 *     TreeNode right;
 *     TreeNode(int x) { val = x; }
 * }
 */
class Solution {
    public TreeNode constructFromPrePost(int[] pre, int[] post) {
        return constructFromPrePost(pre, 0, pre.length-1, post, 0, post.length-1);
    }
    
    private TreeNode constructFromPrePost(int[] pre, int preLeft, int preRight, int[] post, int postLeft, int postRight){
        if(preLeft>preRight || postLeft>postRight){
            return null;
        }else if(preLeft==preRight){
            return new TreeNode(pre[preLeft]);
        }
        TreeNode root = new TreeNode(pre[preLeft]);
        for(int i=postRight-1;i>=postLeft;i--){
            if(post[i]==pre[preLeft+1]){
                root.left = constructFromPrePost(pre, preLeft+1, preLeft+1+i-postLeft, post, postLeft, i);
                root.right = constructFromPrePost(pre, preLeft+2+i-postLeft, preRight, post, i+1, postRight-1);
            }
        }
        return root;
    }
}

889.Construct Binary Tree from Preorder and Postorder Traversal

Input: pre = [1,2,4,5,3,6,7],post = [4,7,1] Output: [1,7] 

#include<stdlib.h>
#include<vector>
#include<stack>
#include<queue>
#include <iostream>

using namespace std;

//DeFinition for a binary tree node.
struct TreeNode {
    int val;
    TreeNode *left;
    TreeNode *right;

    TreeNode(int x) : val(x),left(NULL),right(NULL) {}
};

class Solution {
public:
    TreeNode *constructFromPrePost(vector<int> &pre,vector<int> &post) {
        if (pre.size() == 0) return nullptr;
        stack<TreeNode *> st;
        TreeNode *root = new TreeNode(pre[0]);
        st.push(root);
        int j = 0;
        int i = 0;
        TreeNode *node = nullptr;
        for(int i=1;i<pre.size();++i){
            while (st.top()->val == post[j]) {
                node = st.top();
                st.pop();
                printf("pop %d\n",node->val);
                if (st.top()->left == nullptr) {
                    st.top()->left = node;
                    printf("%d left child is %d\n",st.top()->val,node->val);
                } else {
                    st.top()->right = node;
                    printf("%d right child is %d\n",node->val);
                }
                j++;
                printf("j: %d\n",j);
            }
            if (i < pre.size()){
                st.push(new TreeNode(pre[i]));
                printf("push %d\n",pre[i]);
            }
        }

        while (true) {
            node = st.top();
            st.pop();
            if(st.empty()) break;
            printf("pop %d\n",node->val);
            if (st.top()->left == nullptr) {
                st.top()->left = node;
                printf("%d left child is %d\n",node->val);
            } else {
                st.top()->right = node;
                printf("%d right child is %d\n",node->val);
            }
            j++;
            printf("j: %d\n",j);
        }
        return root;
//        printf("return\n");
//        printf("root->value %d\n",root->val);
//        return root;
    }
};

void show_tree(TreeNode *root) {
    if (root == nullptr) {
        cout<<"root is nullptr"<<endl;
        return;
    }
    cout<<"root is not nullptr"<<endl;
    queue<TreeNode *> qu;
    qu.push(root);
    int sz;
    while (!qu.empty()) {
        sz = qu.size();
        TreeNode* node= nullptr;
        for (int i = 0; i < sz; ++i) {
            node=qu.front();
            cout << node->val << " ";
            qu.pop();
            if (node->left)
                qu.push(node->left);
            if (node->right)
                qu.push(node->right);
        }
        cout << "\n";
    }
}

int main() {
    vector<int> pre{1,2,4,5,3,6,7};
    vector<int> post{4,7,1};
    Solution solution;
    TreeNode *res = solution.constructFromPrePost(pre,post);

//    solution.constructFromPrePost(pre,post);
    printf("res value %d\n",res->val);
    show_tree(res);
    return 0;

}

class Solution {
public:
    TreeNode *constructFromPrePost(vector<int> &pre,vector<int> &post) {
        if (pre.size() == 0) return nullptr;
        stack<TreeNode *> st;
        TreeNode *root = new TreeNode(pre[0]);
        st.push(root);
        int j = 0;
        TreeNode *node = nullptr;
        for(int i=1;i<=pre.size();++i){
            while (st.top()->val == post[j]) {
                node = st.top();
                st.pop();
                //printf("pop %d\n",node->val);
                if(st.empty())
                    return root;
                if (st.top()->left == nullptr) {
                    st.top()->left = node;
                    //printf("%d left child is %d\n",node->val);
                } else {
                    st.top()->right = node;
                    //printf("%d right child is %d\n",node->val);
                }
                j++;
                //printf("j: %d\n",j);
            }
            if (i < pre.size()){
                st.push(new TreeNode(pre[i]));
                //printf("push %d\n",pre[i]);
            }
        }
    }
};

Binary Tree Preorder/Postorder Traversal

树的前序和后序遍历是树相关算法的基本。就不多加解释了，直接上代码。

Binary Tree Preorder Traversal

javapublic class Solution {
    public List<Integer> preorderTraversal(TreeNode root) {
        List<Integer> result = new LinkedList<Integer>();
        generate(result, root);
        return result;
    }

    private void generate(List<Integer> sequence, TreeNode node) {
        if (node == null)
            return;
        sequence.add(node.val);
        generate(sequence, node.left);
        generate(sequence, node.right);
    }
}

Binary Tree Postorder Traversal

javapublic class Solution {
    public List<Integer> postorderTraversal(TreeNode root) {
        List<Integer> result = new LinkedList<Integer>();
        generate(result, root);
        return  result;
    }

    private void generate(List<Integer> result, TreeNode node) {
        if (node == null)
            return;
        generate(result, node.left);
        generate(result, node.right);
        result.add(node.val);
    }
}

我们今天的关于inorder + preorder如何构造唯一的二叉树？和唯一二叉排序树的分享就到这里，谢谢您的阅读，如果想了解更多关于105. Construct Binary Tree from Preorder and Inorder Traversal、889. Construct Binary Tree from Preorder and Postorder Traversal、889.Construct Binary Tree from Preorder and Postorder Traversal、Binary Tree Preorder/Postorder Traversal的相关信息，可以在本站进行搜索。