如何序+ preorder构建独特的二叉树？ [英] How does inorder+preorder construct unique binary tree?
本文介绍了如何序+ preorder构建独特的二叉树？的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
最近，我的问题是重复的标记，如这样，即使他们没有。所以，让我先下，然后我会解释我的问题。
Recently, my questions were marked duplicate, like this , even if they weren't. So, let me start with following and then I'll explain my question.
为什么这个问题是不是重复？
我的不要求如何创建时序和二叉树放大器; preorder遍历给出。我所要求的证明，即序+ preorder穿越定义一个唯一的二进制树。
I'm not asking how to create a binary tree when inorder & preorder traversal are given. I'm asking for the proof, that inorder+preorder traversal define a unique binary tree.
现在，为原题。我去面试，面试官问我这个问题。我被卡住，无法继续。 ：|
Now, to original question. I went to an interview and interviewer asked me this question. I was stuck and couldn't proceed. :|
问：由于中序和放大器;二叉树preorder穿越。证明有只有一个二叉树可能与给定的数据。换句话说，证明两种不同的二叉树不能具有相同的序＆安培; preorder穿越。假设树中的所有元素都是唯一的（感谢@envy_intelligence指出这假设）。
Question: Given inorder & preorder traversal of a binary tree. Prove there is only one binary tree possible with given data. In other words, prove two different binary trees can't have same inorder & preorder traversal. Assume all the elements in the tree are unique (thanks to @envy_intelligence for pointing this assumption).
我试图说服面试官用的例子，但面试官问数学/直观的证明。谁能帮我证明它？
I tried convincing interviewer using examples, but interviewer was asking for mathematical/intuitive proof. Can anyone help me proving it?
推荐答案
先从preorder穿越。要么是空的，在这种情况下，你都做了，或者它有第一个元素， R0 树的根。现在搜索中序遍历 R0 。左子树将全部来了，是点之前和右子树将全部来了，是点之后。因此，你可以把中序遍历该点到左子树的中序遍历 IL 和右子树的中序遍历， IR 。
Start with the preorder traversal. Either it is empty, in which case you are done, or it has a first element, r0, the root of the tree. Now search the inorder traversal for r0. The left subtree will all come before that point and the right subtree will all come after that point. Thus you can divide the inorder traversal at that point into an inorder traversal of the left subtree il and an inorder traversal of the right subtree, ir.
如果 IL 是空的，那么preorder遍历其余属于右子树，您可以继续电感。如果 IR 是空的，同样的事情也发生在另一边。如果两者都不是空的，找到中的preorder遍历其余部分的第一个元素IR 。这将其分为左子树的preorder遍历，右子树之一。电磁炉是立竿见影的。
If il is empty, then the rest of the preorder traversal belongs to the right subtree, and you can continue inductively. If ir is empty, the same thing happens on the other side. If neither is empty, find the first element of ir in the remainder of the preorder traversal. This divides it into a preorder traversal of the left subtree and one of the right subtree. Induction is immediate.
如果有人有兴趣在正式的证据，我（终于）成功地产生一种在伊德里斯。我没有，但是，所花费的时间，以尽量做到非常可读的，所以它其实是相当难读太多。我建议你看看主要是在顶层类型（例如，引理，定理和定义），并尽量避免过于的证明（条款）越陷越深。
In case anyone is interested in a formal proof, I have (finally) managed to produce one in Idris. I have not, however, taken the time to try to make it terribly readable, so it is actually fairly hard to read much of it. I would recommend that you look mostly at the top-level types (i.e., lemmas, theorems, and definitions) and try to avoid getting too bogged down in the proofs (terms).
首先，一些preliminaries：
First some preliminaries:
module PreIn
import Data.List
%default total
现在的第一个真正的想法：一个二叉树
Now the first real idea: a binary tree.
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模块，其中EX presses办法找到一个紧密依托在一个特定的列表中特定的元素的。
Now the second big idea: the idea of a way to find a particular element in a particular tree. This is based closely on the Elem type in Data.List, which expresses a way to find a particular element in a particular 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穿越之间的对应关系
其中许多相同的引理可以用来证明相应的定理preorder遍历：
Correspondence between a tree and its preorder traversal
Many of those same lemmas can then be used to prove the corresponding theorems for preorder traversals:
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 。
Good so far? Glad to hear it. The theorem you seek is fast approaching! First, we need a notion of a tree being "injective", which I think is the simplest notion of "has no duplicates" in this context. Don't worry if you don't like this notion; there's another one down south a ways. This one says that a tree t is injective if whenever loc1 and loc1 are ways to find a value x in t, loc1 must equal loc2.
InjTree : Tree a -> Type
InjTree t = (x : a) -> (loc1, loc2 : x `InTree` t) -> loc1 = loc2
我们也希望为列出了相应的概念，因为我们会证明树木射当且仅当其遍历的。这些证明是对的下方，并按照从preceding。
We also want the corresponding notion for lists, since we'll be proving that trees are injective if and only if their traversals are. Those proofs are right below, and follow from the preceding.
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
简单的事实：如果一棵树是单射的，那么在其左，右子树
Simple fact: if a tree is injective, then so are its left and right subtrees.
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 具有相同的preorder和中序遍历，那么 T 和 U 都是平等的。
The main objective!
If t and u are binary trees, t is injective, and t and u have the same preorder and inorder traversals, then t and u are equal.
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
不重复
另一种观点有人可能会想指出，一棵树有没有重复，如果每当在树中的两个位置是不相等的，因此，它们并不拥有相同的元素。这可以用pssed EX $ P $的 NoDups 键入
An alternative notion of "no duplicates"
One might wish to say that a tree "has no duplicates" if whenever two locations in the tree are not equal, it follows that they do not hold the same element. This can be expressed using the NoDups type.
NoDups : Tree a -> Type
NoDups {a} t = (x, y : a) ->
(loc1 : x `InTree` t) ->
(loc2 : y `InTree` t) ->
Not (loc1 = loc2) ->
Not (x = y)
究其原因，这是强大到足以证明我们需要的是有确定在树上两个路径是否相同的过程：
The reason this is strong enough to prove what we need is that there is a procedure for determining whether two paths in a tree are equal:
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牛逼意味着 InjTree牛逼：
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牛逼能够完成任务。
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)
这篇关于如何序+ preorder构建独特的二叉树？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
查看全文
