inorder+preorder如何构造唯一二叉树？
How does inorder+preorder construct unique binary tree?
最近，我的问题被标记为重复，例如 this，即使它们不是。那么，让我从下面开始，然后我会解释我的问题。
为什么这个问题不是重复的？
我不问如何在给定中序和前序遍历时创建二叉树。我要证明，中序+先序遍历定义了一个唯一的二叉树。
现在，原问题。我去面试了，面试官问了我这个问题。我被卡住了，无法继续。 :|
问题：给定二叉树的中序和先序遍历。证明给定数据 只有一棵可能的二叉树 。换句话说，证明两个不同的二叉树不能有相同的中序和前序遍历。假设树中的所有元素都是唯一的（感谢@envy_intelligence 指出了这个假设）。
我试着用例子说服面试官，但面试官要求 mathematical/intuitive 证明。谁能帮我证明一下？
我会问面试官的一个问题是关于重复元素。如果两个 "different" 二叉树具有重复元素，则它们可以具有相同的前序和中序遍历。
例如，考虑以下情况：
顺序 : {12, 12}
预购：{12, 12}
12 12
/ \
12 12
现在谈到有独特元素的情况。
当我们递归处理一个问题时，我们总是可以将更大的集合分解为 3 个元组。假设我们有 中序遍历 作为 {Left,Root,Right} 和 pre -order Traversal as {Root, Left , Right}.
当我们从前序遍历固定根时，前序遍历的其余部分应该被认为是两个子部分，它们的进一步细节可以从中序遍历中获得.观察在每个阶段，我们尝试解决标准的三节点问题：我们可能不太关心每个节点有多少 "sub-problems" 因为我们知道我们稍后会到达那个点。
从前序遍历开始。要么它是空的，在这种情况下你就完成了，要么它有第一个元素，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
现在是第二个重要想法：在特定树中查找特定元素的方法的想法。这与 Data.List 中的 Elem 类型密切相关，它表达了一种在特定 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) in 我的问题。
可怕的引理
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)
到目前为止还好吗？很高兴听到。您寻求的定理正在快速接近！首先，我们需要一个树的概念 "injective"，我认为这是本文中最简单的 "has no duplicates" 概念。如果您不喜欢这个概念，请不要担心；南边还有一个。这个说树 t 是单射的，如果每当 loc1 和 loc1 是在 t 中找到值 x 的方法时，loc1 必须等于 loc2.
InjTree : Tree a -> Type
InjTree t = (x : a) -> (loc1, loc2 : x `InTree` t) -> loc1 = loc2
我们还需要列表的相应概念，因为我们将证明树是单射的当且仅当它们的遍历是单射的。这些证明就在下面，从前面开始。
InjList : List a -> Type
InjList xs = (x : a) -> (loc1, loc2 : x `Elem` xs) -> loc1 = loc2
||| If a tree is injective, so is its preorder traversal
treePreInj : (t : Tree a) -> InjTree t -> InjList (preorder t)
treePreInj {a} t it x loc1 loc2 =
let foo = preorderThenT {a} {x} t loc1
bar = preorderThenT {a} {x} t loc2
baz = it x foo bar
in rewrite sym $ preorderFroTo t loc1
in rewrite sym $ preorderFroTo t loc2
in cong baz
||| If a tree is injective, so is its inorder traversal
treeInInj : (t : Tree a) -> InjTree t -> InjList (inorder t)
treeInInj {a} t it x loc1 loc2 =
let foo = inorderThenT {a} {x} t loc1
bar = inorderThenT {a} {x} t loc2
baz = it x foo bar
in rewrite sym $ inorderFroTo t loc1
in rewrite sym $ inorderFroTo t loc2
in cong baz
||| If a tree's preorder traversal is injective, so is the tree.
injPreTree : (t : Tree a) -> InjList (preorder t) -> InjTree t
injPreTree {a} t il x loc1 loc2 =
let
foo = tThenPreorder {a} {x} t loc1
bar = tThenPreorder {a} {x} t loc2
baz = il x foo bar
in rewrite sym $ preorderToFro t loc1
in rewrite sym $ preorderToFro t loc2
in cong baz
||| If a tree's inorder traversal is injective, so is the tree.
injInTree : (t : Tree a) -> InjList (inorder t) -> InjTree t
injInTree {a} t il x loc1 loc2 =
let
foo = tThenInorder {a} {x} t loc1
bar = tThenInorder {a} {x} t loc2
baz = il x foo bar
in rewrite sym $ inorderToFro t loc1
in rewrite sym $ inorderToFro t loc2
in cong baz
更可怕的引理
headsSame : {x:a} -> {xs : List a} -> {y : a} -> {ys : List a} -> (x :: xs) = (y :: ys) -> x = y
headsSame Refl = Refl
tailsSame : {x:a} -> {xs : List a} -> {y : a} -> {ys : List a} -> (x :: xs) = (y :: ys) -> xs = ys
tailsSame Refl = Refl
appendLeftCancel : {xs,ys,ys' : List a} -> xs ++ ys = xs ++ ys' -> ys = ys'
appendLeftCancel {xs = []} prf = prf
appendLeftCancel {xs = (x :: xs)} prf = appendLeftCancel {xs} (tailsSame prf)
lengthDrop : (xs,ys : List a) -> drop (length xs) (xs ++ ys) = ys
lengthDrop [] ys = Refl
lengthDrop (x :: xs) ys = lengthDrop xs ys
lengthTake : (xs,ys : List a) -> take (length xs) (xs ++ ys) = xs
lengthTake [] ys = Refl
lengthTake (x :: xs) ys = cong $ lengthTake xs ys
appendRightCancel_lem : (xs,xs',ys : List a) -> xs ++ ys = xs' ++ ys -> length xs = length xs'
appendRightCancel_lem xs xs' ys eq =
let foo = lengthAppend xs ys
bar = replace {P = \b => length b = length xs + length ys} eq foo
baz = trans (sym bar) $ lengthAppend xs' ys
in plusRightCancel (length xs) (length xs') (length ys) baz
appendRightCancel : {xs,xs',ys : List a} -> xs ++ ys = xs' ++ ys -> xs = xs'
appendRightCancel {xs} {xs'} {ys} eq with (appendRightCancel_lem xs xs' ys eq)
| lenEq = rewrite sym $ lengthTake xs ys
in let foo : (take (length xs') (xs ++ ys) = xs') = rewrite eq in lengthTake xs' ys
in rewrite lenEq in foo
listPartsEqLeft : {xs, xs', ys, ys' : List a} ->
length xs = length xs' ->
xs ++ ys = xs' ++ ys' ->
xs = xs'
listPartsEqLeft {xs} {xs'} {ys} {ys'} leneq appeq =
rewrite sym $ lengthTake xs ys
in rewrite leneq
in rewrite appeq
in lengthTake xs' ys'
listPartsEqRight : {xs, xs', ys, ys' : List a} ->
length xs = length xs' ->
xs ++ ys = xs' ++ ys' ->
ys = ys'
listPartsEqRight leneq appeq with (listPartsEqLeft leneq appeq)
listPartsEqRight leneq appeq | Refl = appendLeftCancel appeq
thereInjective : There loc1 = There loc2 -> loc1 = loc2
thereInjective Refl = Refl
injTail : InjList (x :: xs) -> InjList xs
injTail {x} {xs} xxsInj v vloc1 vloc2 = thereInjective $
xxsInj v (There vloc1) (There vloc2)
splitInorder_lem2 : ((loc1 : Elem v (v :: xs ++ v :: ysr)) ->
(loc2 : Elem v (v :: xs ++ v :: ysr)) -> loc1 = loc2) ->
Void
splitInorder_lem2 {v} {xs} {ysr} f =
let
loc2 = elemAppend {x=v} xs (v :: ysr) Here
in (\Refl impossible) $ f Here (There loc2)
-- preorderLength and inorderLength could be proven using the bijections
-- between trees and their traversals, but it's much easier to just prove
-- them directly.
preorderLength : (t : Tree a) -> length (preorder t) = size t
preorderLength Tip = Refl
preorderLength (Node l v r) =
rewrite sym (plusSuccRightSucc (size l) (size r))
in cong {f=S} $
rewrite sym $ preorderLength l
in rewrite sym $ preorderLength r
in lengthAppend _ _
inorderLength : (t : Tree a) -> length (inorder t) = size t
inorderLength Tip = Refl
inorderLength (Node l v r) =
rewrite lengthAppend (inorder l) (v :: inorder r)
in rewrite inorderLength l
in rewrite inorderLength r in Refl
preInLength : (t : Tree a) -> length (preorder t) = length (inorder t)
preInLength t = trans (preorderLength t) (sym $ inorderLength t)
splitInorder_lem1 : (v : a) ->
(xsl, xsr, ysl, ysr : List a) ->
(xsInj : InjList (xsl ++ v :: xsr)) ->
(ysInj : InjList (ysl ++ v :: ysr)) ->
xsl ++ v :: xsr = ysl ++ v :: ysr ->
v `Elem` (xsl ++ v :: xsr) ->
v `Elem` (ysl ++ v :: ysr) ->
xsl = ysl
splitInorder_lem1 v [] xsr [] ysr xsInj ysInj eq locxs locys = Refl
splitInorder_lem1 v [] xsr (v :: ysl) ysr xsInj ysInj eq Here Here with (ysInj v Here (elemAppend (v :: ysl) (v :: ysr) Here))
splitInorder_lem1 v [] xsr (v :: ysl) ysr xsInj ysInj eq Here Here | Refl impossible
splitInorder_lem1 v [] xsr (y :: ysl) ysr xsInj ysInj eq Here (There loc) with (headsSame eq)
splitInorder_lem1 v [] xsr (v :: ysl) ysr xsInj ysInj eq Here (There loc) | Refl = absurd $ splitInorder_lem2 (ysInj v)
splitInorder_lem1 v [] xsr (x :: xs) ysr xsInj ysInj eq (There loc) locys with (headsSame eq)
splitInorder_lem1 v [] xsr (v :: xs) ysr xsInj ysInj eq (There loc) locys | Refl = absurd $ splitInorder_lem2 (ysInj v)
splitInorder_lem1 v (v :: xs) xsr ysl ysr xsInj ysInj eq Here locys = absurd $ splitInorder_lem2 (xsInj v)
splitInorder_lem1 v (x :: xs) xsr [] ysr xsInj ysInj eq (There y) locys with (headsSame eq)
splitInorder_lem1 v (v :: xs) xsr [] ysr xsInj ysInj eq (There y) locys | Refl = absurd $ splitInorder_lem2 (xsInj v)
splitInorder_lem1 v (x :: xs) xsr (z :: ys) ysr xsInj ysInj eq (There y) locys with (headsSame eq)
splitInorder_lem1 v (v :: xs) xsr (_ :: ys) ysr xsInj ysInj eq (There y) Here | Refl = absurd $ splitInorder_lem2 (ysInj v)
splitInorder_lem1 v (x :: xs) xsr (x :: ys) ysr xsInj ysInj eq (There y) (There z) | Refl = cong {f = ((::) x)} $
splitInorder_lem1 v xs xsr ys ysr (injTail xsInj) (injTail ysInj) (tailsSame eq) y z
splitInorder_lem3 : (v : a) ->
(xsl, xsr, ysl, ysr : List a) ->
(xsInj : InjList (xsl ++ v :: xsr)) ->
(ysInj : InjList (ysl ++ v :: ysr)) ->
xsl ++ v :: xsr = ysl ++ v :: ysr ->
v `Elem` (xsl ++ v :: xsr) ->
v `Elem` (ysl ++ v :: ysr) ->
xsr = ysr
splitInorder_lem3 v xsl xsr ysl ysr xsInj ysInj prf locxs locys with (splitInorder_lem1 v xsl xsr ysl ysr xsInj ysInj prf locxs locys)
splitInorder_lem3 v xsl xsr xsl ysr xsInj ysInj prf locxs locys | Refl =
tailsSame $ appendLeftCancel prf
一个简单的事实：如果一棵树是内射的，那么它的左右子树也是内射的。
injLeft : {l : Tree a} -> {v : a} -> {r : Tree a} ->
InjTree (Node l v r) -> InjTree l
injLeft {l} {v} {r} injlvr x loc1 loc2 with (injlvr x (OnLeft loc1) (OnLeft loc2))
injLeft {l = l} {v = v} {r = r} injlvr x loc1 loc1 | Refl = Refl
injRight : {l : Tree a} -> {v : a} -> {r : Tree a} ->
InjTree (Node l v r) -> InjTree r
injRight {l} {v} {r} injlvr x loc1 loc2 with (injlvr x (OnRight loc1) (OnRight loc2))
injRight {l} {v} {r} injlvr x loc1 loc1 | Refl = Refl
主要objective!
如果t和u是二叉树，t是单射的，t和u有相同的前序和中序遍历，那么t 和 u 相等。
travsDet : (t, u : Tree a) -> InjTree t -> preorder t = preorder u -> inorder t = inorder u -> t = u
-- The base case--both trees are empty
travsDet Tip Tip x prf prf1 = Refl
-- Impossible cases: only one tree is empty
travsDet Tip (Node l v r) x Refl prf1 impossible
travsDet (Node l v r) Tip x Refl prf1 impossible
-- The interesting case. `headsSame presame` proves
-- that the roots of the trees are equal.
travsDet (Node l v r) (Node t y u) lvrInj presame insame with (headsSame presame)
travsDet (Node l v r) (Node t v u) lvrInj presame insame | Refl =
let
foo = elemAppend (inorder l) (v :: inorder r) Here
bar = elemAppend (inorder t) (v :: inorder u) Here
inlvrInj = treeInInj _ lvrInj
intvuInj : (InjList (inorder (Node t v u))) = rewrite sym insame in inlvrInj
inorderRightSame = splitInorder_lem3 v (inorder l) (inorder r) (inorder t) (inorder u) inlvrInj intvuInj insame foo bar
preInL : (length (preorder l) = length (inorder l)) = preInLength l
inorderLeftSame = splitInorder_lem1 v (inorder l) (inorder r) (inorder t) (inorder u) inlvrInj intvuInj insame foo bar
inPreT : (length (inorder t) = length (preorder t)) = sym $ preInLength t
preLenlt : (length (preorder l) = length (preorder t))
= trans preInL (trans (cong inorderLeftSame) inPreT)
presame' = tailsSame presame
baz : (preorder l = preorder t) = listPartsEqLeft preLenlt presame'
quux : (preorder r = preorder u) = listPartsEqRight preLenlt presame'
-- Putting together the lemmas, we see that the
-- left and right subtrees are equal
recleft = travsDet l t (injLeft lvrInj) baz inorderLeftSame
recright = travsDet r u (injRight lvrInj) quux inorderRightSame
in rewrite recleft in rewrite recright in Refl
"no duplicates"
的替代概念
有人可能想说一棵树 "has no duplicates" 如果树中的两个位置不相等，则它们不包含相同的元素。这可以使用 NoDups 类型来表示。
NoDups : Tree a -> Type
NoDups {a} t = (x, y : a) ->
(loc1 : x `InTree` t) ->
(loc2 : y `InTree` t) ->
Not (loc1 = loc2) ->
Not (x = y)
之所以这足以证明我们需要什么，是因为有一个程序可以确定树中的两条路径是否相等：
instance DecEq (x `InTree` t) where
decEq AtRoot AtRoot = Yes Refl
decEq AtRoot (OnLeft x) = No (\Refl impossible)
decEq AtRoot (OnRight x) = No (\Refl impossible)
decEq (OnLeft x) AtRoot = No (\Refl impossible)
decEq (OnLeft x) (OnLeft y) with (decEq x y)
decEq (OnLeft x) (OnLeft x) | (Yes Refl) = Yes Refl
decEq (OnLeft x) (OnLeft y) | (No contra) = No (contra . onLeftInjective)
decEq (OnLeft x) (OnRight y) = No (\Refl impossible)
decEq (OnRight x) AtRoot = No (\Refl impossible)
decEq (OnRight x) (OnLeft y) = No (\Refl impossible)
decEq (OnRight x) (OnRight y) with (decEq x y)
decEq (OnRight x) (OnRight x) | (Yes Refl) = Yes Refl
decEq (OnRight x) (OnRight y) | (No contra) = No (contra . onRightInjective)
这证明Nodups t蕴含InjTree t:
noDupsInj : (t : Tree a) -> NoDups t -> InjTree t
noDupsInj t nd x loc1 loc2 with (decEq loc1 loc2)
noDupsInj t nd x loc1 loc2 | (Yes prf) = prf
noDupsInj t nd x loc1 loc2 | (No contra) = absurd $ nd x x loc1 loc2 contra Refl
最后，NoDups t 完成了工作。
travsDet2 : (t, u : Tree a) -> NoDups t -> preorder t = preorder u -> inorder t = inorder u -> t = u
travsDet2 t u ndt = travsDet t u (noDupsInj t ndt)
假设您有以下预序遍历：a,b,c,d,e,f,g。这告诉你什么？
你知道 a 是树的根，这是从前序遍历的定义得出的。到目前为止，还不错。
你也知道你列表的其余部分是先遍历左子树再遍历右子树。不幸的是你不知道分裂在哪里。可以是都属于左树，也可以是都属于右树，或者b,c向左d,e,f,g向右等等
如何解决歧义？那么我们来看一下中序遍历，它的定义属性是什么？在中序遍历中，a 左子树中的任何元素都将出现在 a 之前，而右子树中的任何元素都将出现在 a 之后。同样，这遵循中序遍历的定义。
所以我们需要做的是看一下中序遍历（假设是c,b,a,d,e,f,g）。我们可以看到 b 和 c 出现在 a 之前，因此它们在左子树中，而 d、e、f和 g 在右子树中。换句话说，as 在中序遍历中的位置唯一确定了哪些节点将在其 left/right 子树中。
这很好，因为我们现在可以继续递归求解两个子树：预序 b,c/in-order c,b 和预序 d,e,f,g/in -顺序 d,e,f,g.
并且您可以递归地继续此操作，直到所有子树仅包含一个元素，其中解决方案非常独特。
而且由于在每一步我们都可以证明只有一种有效的继续方式，结果是给定的一对中序和前序遍历只能属于一棵树。
如果你喜欢更正式的符号，你可以找到完全相同的证明here。
为了创建树，我们需要一个根节点和一个放置顺序。
Preorder/postorder 提供根节点，而 inorder 提供放置顺序。因此，根据这种推理，我们需要两次遍历，先序或后序以及中序来创建唯一的树。
如果它是 BST，那么 Preorder 或 Postorder 就足够了，因为我们已经知道节点的放置顺序。
这是对问题的直观推理。
最近，我的问题被标记为重复，例如 this，即使它们不是。那么，让我从下面开始，然后我会解释我的问题。
为什么这个问题不是重复的？
我不问如何在给定中序和前序遍历时创建二叉树。我要证明，中序+先序遍历定义了一个唯一的二叉树。
现在，原问题。我去面试了，面试官问了我这个问题。我被卡住了，无法继续。 :|
问题：给定二叉树的中序和先序遍历。证明给定数据 只有一棵可能的二叉树 。换句话说，证明两个不同的二叉树不能有相同的中序和前序遍历。假设树中的所有元素都是唯一的（感谢@envy_intelligence 指出了这个假设）。
我试着用例子说服面试官，但面试官要求 mathematical/intuitive 证明。谁能帮我证明一下？
我会问面试官的一个问题是关于重复元素。如果两个 "different" 二叉树具有重复元素，则它们可以具有相同的前序和中序遍历。
例如，考虑以下情况：
顺序 : {12, 12} 预购：{12, 12}
12 12
/ \
12 12
现在谈到有独特元素的情况。 当我们递归处理一个问题时，我们总是可以将更大的集合分解为 3 个元组。假设我们有 中序遍历 作为 {Left,Root,Right} 和 pre -order Traversal as {Root, Left , Right}.
当我们从前序遍历固定根时，前序遍历的其余部分应该被认为是两个子部分，它们的进一步细节可以从中序遍历中获得.观察在每个阶段，我们尝试解决标准的三节点问题：我们可能不太关心每个节点有多少 "sub-problems" 因为我们知道我们稍后会到达那个点。
从前序遍历开始。要么它是空的，在这种情况下你就完成了，要么它有第一个元素，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
现在是第二个重要想法：在特定树中查找特定元素的方法的想法。这与 Data.List 中的 Elem 类型密切相关，它表达了一种在特定 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) in
可怕的引理
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)
到目前为止还好吗？很高兴听到。您寻求的定理正在快速接近！首先，我们需要一个树的概念 "injective"，我认为这是本文中最简单的 "has no duplicates" 概念。如果您不喜欢这个概念，请不要担心；南边还有一个。这个说树 t 是单射的，如果每当 loc1 和 loc1 是在 t 中找到值 x 的方法时，loc1 必须等于 loc2.
InjTree : Tree a -> Type
InjTree t = (x : a) -> (loc1, loc2 : x `InTree` t) -> loc1 = loc2
我们还需要列表的相应概念，因为我们将证明树是单射的当且仅当它们的遍历是单射的。这些证明就在下面，从前面开始。
InjList : List a -> Type
InjList xs = (x : a) -> (loc1, loc2 : x `Elem` xs) -> loc1 = loc2
||| If a tree is injective, so is its preorder traversal
treePreInj : (t : Tree a) -> InjTree t -> InjList (preorder t)
treePreInj {a} t it x loc1 loc2 =
let foo = preorderThenT {a} {x} t loc1
bar = preorderThenT {a} {x} t loc2
baz = it x foo bar
in rewrite sym $ preorderFroTo t loc1
in rewrite sym $ preorderFroTo t loc2
in cong baz
||| If a tree is injective, so is its inorder traversal
treeInInj : (t : Tree a) -> InjTree t -> InjList (inorder t)
treeInInj {a} t it x loc1 loc2 =
let foo = inorderThenT {a} {x} t loc1
bar = inorderThenT {a} {x} t loc2
baz = it x foo bar
in rewrite sym $ inorderFroTo t loc1
in rewrite sym $ inorderFroTo t loc2
in cong baz
||| If a tree's preorder traversal is injective, so is the tree.
injPreTree : (t : Tree a) -> InjList (preorder t) -> InjTree t
injPreTree {a} t il x loc1 loc2 =
let
foo = tThenPreorder {a} {x} t loc1
bar = tThenPreorder {a} {x} t loc2
baz = il x foo bar
in rewrite sym $ preorderToFro t loc1
in rewrite sym $ preorderToFro t loc2
in cong baz
||| If a tree's inorder traversal is injective, so is the tree.
injInTree : (t : Tree a) -> InjList (inorder t) -> InjTree t
injInTree {a} t il x loc1 loc2 =
let
foo = tThenInorder {a} {x} t loc1
bar = tThenInorder {a} {x} t loc2
baz = il x foo bar
in rewrite sym $ inorderToFro t loc1
in rewrite sym $ inorderToFro t loc2
in cong baz
更可怕的引理
headsSame : {x:a} -> {xs : List a} -> {y : a} -> {ys : List a} -> (x :: xs) = (y :: ys) -> x = y
headsSame Refl = Refl
tailsSame : {x:a} -> {xs : List a} -> {y : a} -> {ys : List a} -> (x :: xs) = (y :: ys) -> xs = ys
tailsSame Refl = Refl
appendLeftCancel : {xs,ys,ys' : List a} -> xs ++ ys = xs ++ ys' -> ys = ys'
appendLeftCancel {xs = []} prf = prf
appendLeftCancel {xs = (x :: xs)} prf = appendLeftCancel {xs} (tailsSame prf)
lengthDrop : (xs,ys : List a) -> drop (length xs) (xs ++ ys) = ys
lengthDrop [] ys = Refl
lengthDrop (x :: xs) ys = lengthDrop xs ys
lengthTake : (xs,ys : List a) -> take (length xs) (xs ++ ys) = xs
lengthTake [] ys = Refl
lengthTake (x :: xs) ys = cong $ lengthTake xs ys
appendRightCancel_lem : (xs,xs',ys : List a) -> xs ++ ys = xs' ++ ys -> length xs = length xs'
appendRightCancel_lem xs xs' ys eq =
let foo = lengthAppend xs ys
bar = replace {P = \b => length b = length xs + length ys} eq foo
baz = trans (sym bar) $ lengthAppend xs' ys
in plusRightCancel (length xs) (length xs') (length ys) baz
appendRightCancel : {xs,xs',ys : List a} -> xs ++ ys = xs' ++ ys -> xs = xs'
appendRightCancel {xs} {xs'} {ys} eq with (appendRightCancel_lem xs xs' ys eq)
| lenEq = rewrite sym $ lengthTake xs ys
in let foo : (take (length xs') (xs ++ ys) = xs') = rewrite eq in lengthTake xs' ys
in rewrite lenEq in foo
listPartsEqLeft : {xs, xs', ys, ys' : List a} ->
length xs = length xs' ->
xs ++ ys = xs' ++ ys' ->
xs = xs'
listPartsEqLeft {xs} {xs'} {ys} {ys'} leneq appeq =
rewrite sym $ lengthTake xs ys
in rewrite leneq
in rewrite appeq
in lengthTake xs' ys'
listPartsEqRight : {xs, xs', ys, ys' : List a} ->
length xs = length xs' ->
xs ++ ys = xs' ++ ys' ->
ys = ys'
listPartsEqRight leneq appeq with (listPartsEqLeft leneq appeq)
listPartsEqRight leneq appeq | Refl = appendLeftCancel appeq
thereInjective : There loc1 = There loc2 -> loc1 = loc2
thereInjective Refl = Refl
injTail : InjList (x :: xs) -> InjList xs
injTail {x} {xs} xxsInj v vloc1 vloc2 = thereInjective $
xxsInj v (There vloc1) (There vloc2)
splitInorder_lem2 : ((loc1 : Elem v (v :: xs ++ v :: ysr)) ->
(loc2 : Elem v (v :: xs ++ v :: ysr)) -> loc1 = loc2) ->
Void
splitInorder_lem2 {v} {xs} {ysr} f =
let
loc2 = elemAppend {x=v} xs (v :: ysr) Here
in (\Refl impossible) $ f Here (There loc2)
-- preorderLength and inorderLength could be proven using the bijections
-- between trees and their traversals, but it's much easier to just prove
-- them directly.
preorderLength : (t : Tree a) -> length (preorder t) = size t
preorderLength Tip = Refl
preorderLength (Node l v r) =
rewrite sym (plusSuccRightSucc (size l) (size r))
in cong {f=S} $
rewrite sym $ preorderLength l
in rewrite sym $ preorderLength r
in lengthAppend _ _
inorderLength : (t : Tree a) -> length (inorder t) = size t
inorderLength Tip = Refl
inorderLength (Node l v r) =
rewrite lengthAppend (inorder l) (v :: inorder r)
in rewrite inorderLength l
in rewrite inorderLength r in Refl
preInLength : (t : Tree a) -> length (preorder t) = length (inorder t)
preInLength t = trans (preorderLength t) (sym $ inorderLength t)
splitInorder_lem1 : (v : a) ->
(xsl, xsr, ysl, ysr : List a) ->
(xsInj : InjList (xsl ++ v :: xsr)) ->
(ysInj : InjList (ysl ++ v :: ysr)) ->
xsl ++ v :: xsr = ysl ++ v :: ysr ->
v `Elem` (xsl ++ v :: xsr) ->
v `Elem` (ysl ++ v :: ysr) ->
xsl = ysl
splitInorder_lem1 v [] xsr [] ysr xsInj ysInj eq locxs locys = Refl
splitInorder_lem1 v [] xsr (v :: ysl) ysr xsInj ysInj eq Here Here with (ysInj v Here (elemAppend (v :: ysl) (v :: ysr) Here))
splitInorder_lem1 v [] xsr (v :: ysl) ysr xsInj ysInj eq Here Here | Refl impossible
splitInorder_lem1 v [] xsr (y :: ysl) ysr xsInj ysInj eq Here (There loc) with (headsSame eq)
splitInorder_lem1 v [] xsr (v :: ysl) ysr xsInj ysInj eq Here (There loc) | Refl = absurd $ splitInorder_lem2 (ysInj v)
splitInorder_lem1 v [] xsr (x :: xs) ysr xsInj ysInj eq (There loc) locys with (headsSame eq)
splitInorder_lem1 v [] xsr (v :: xs) ysr xsInj ysInj eq (There loc) locys | Refl = absurd $ splitInorder_lem2 (ysInj v)
splitInorder_lem1 v (v :: xs) xsr ysl ysr xsInj ysInj eq Here locys = absurd $ splitInorder_lem2 (xsInj v)
splitInorder_lem1 v (x :: xs) xsr [] ysr xsInj ysInj eq (There y) locys with (headsSame eq)
splitInorder_lem1 v (v :: xs) xsr [] ysr xsInj ysInj eq (There y) locys | Refl = absurd $ splitInorder_lem2 (xsInj v)
splitInorder_lem1 v (x :: xs) xsr (z :: ys) ysr xsInj ysInj eq (There y) locys with (headsSame eq)
splitInorder_lem1 v (v :: xs) xsr (_ :: ys) ysr xsInj ysInj eq (There y) Here | Refl = absurd $ splitInorder_lem2 (ysInj v)
splitInorder_lem1 v (x :: xs) xsr (x :: ys) ysr xsInj ysInj eq (There y) (There z) | Refl = cong {f = ((::) x)} $
splitInorder_lem1 v xs xsr ys ysr (injTail xsInj) (injTail ysInj) (tailsSame eq) y z
splitInorder_lem3 : (v : a) ->
(xsl, xsr, ysl, ysr : List a) ->
(xsInj : InjList (xsl ++ v :: xsr)) ->
(ysInj : InjList (ysl ++ v :: ysr)) ->
xsl ++ v :: xsr = ysl ++ v :: ysr ->
v `Elem` (xsl ++ v :: xsr) ->
v `Elem` (ysl ++ v :: ysr) ->
xsr = ysr
splitInorder_lem3 v xsl xsr ysl ysr xsInj ysInj prf locxs locys with (splitInorder_lem1 v xsl xsr ysl ysr xsInj ysInj prf locxs locys)
splitInorder_lem3 v xsl xsr xsl ysr xsInj ysInj prf locxs locys | Refl =
tailsSame $ appendLeftCancel prf
一个简单的事实：如果一棵树是内射的，那么它的左右子树也是内射的。
injLeft : {l : Tree a} -> {v : a} -> {r : Tree a} ->
InjTree (Node l v r) -> InjTree l
injLeft {l} {v} {r} injlvr x loc1 loc2 with (injlvr x (OnLeft loc1) (OnLeft loc2))
injLeft {l = l} {v = v} {r = r} injlvr x loc1 loc1 | Refl = Refl
injRight : {l : Tree a} -> {v : a} -> {r : Tree a} ->
InjTree (Node l v r) -> InjTree r
injRight {l} {v} {r} injlvr x loc1 loc2 with (injlvr x (OnRight loc1) (OnRight loc2))
injRight {l} {v} {r} injlvr x loc1 loc1 | Refl = Refl
主要objective!
如果t和u是二叉树，t是单射的，t和u有相同的前序和中序遍历，那么t 和 u 相等。
travsDet : (t, u : Tree a) -> InjTree t -> preorder t = preorder u -> inorder t = inorder u -> t = u
-- The base case--both trees are empty
travsDet Tip Tip x prf prf1 = Refl
-- Impossible cases: only one tree is empty
travsDet Tip (Node l v r) x Refl prf1 impossible
travsDet (Node l v r) Tip x Refl prf1 impossible
-- The interesting case. `headsSame presame` proves
-- that the roots of the trees are equal.
travsDet (Node l v r) (Node t y u) lvrInj presame insame with (headsSame presame)
travsDet (Node l v r) (Node t v u) lvrInj presame insame | Refl =
let
foo = elemAppend (inorder l) (v :: inorder r) Here
bar = elemAppend (inorder t) (v :: inorder u) Here
inlvrInj = treeInInj _ lvrInj
intvuInj : (InjList (inorder (Node t v u))) = rewrite sym insame in inlvrInj
inorderRightSame = splitInorder_lem3 v (inorder l) (inorder r) (inorder t) (inorder u) inlvrInj intvuInj insame foo bar
preInL : (length (preorder l) = length (inorder l)) = preInLength l
inorderLeftSame = splitInorder_lem1 v (inorder l) (inorder r) (inorder t) (inorder u) inlvrInj intvuInj insame foo bar
inPreT : (length (inorder t) = length (preorder t)) = sym $ preInLength t
preLenlt : (length (preorder l) = length (preorder t))
= trans preInL (trans (cong inorderLeftSame) inPreT)
presame' = tailsSame presame
baz : (preorder l = preorder t) = listPartsEqLeft preLenlt presame'
quux : (preorder r = preorder u) = listPartsEqRight preLenlt presame'
-- Putting together the lemmas, we see that the
-- left and right subtrees are equal
recleft = travsDet l t (injLeft lvrInj) baz inorderLeftSame
recright = travsDet r u (injRight lvrInj) quux inorderRightSame
in rewrite recleft in rewrite recright in Refl
"no duplicates"
的替代概念有人可能想说一棵树 "has no duplicates" 如果树中的两个位置不相等，则它们不包含相同的元素。这可以使用 NoDups 类型来表示。
NoDups : Tree a -> Type
NoDups {a} t = (x, y : a) ->
(loc1 : x `InTree` t) ->
(loc2 : y `InTree` t) ->
Not (loc1 = loc2) ->
Not (x = y)
之所以这足以证明我们需要什么，是因为有一个程序可以确定树中的两条路径是否相等：
instance DecEq (x `InTree` t) where
decEq AtRoot AtRoot = Yes Refl
decEq AtRoot (OnLeft x) = No (\Refl impossible)
decEq AtRoot (OnRight x) = No (\Refl impossible)
decEq (OnLeft x) AtRoot = No (\Refl impossible)
decEq (OnLeft x) (OnLeft y) with (decEq x y)
decEq (OnLeft x) (OnLeft x) | (Yes Refl) = Yes Refl
decEq (OnLeft x) (OnLeft y) | (No contra) = No (contra . onLeftInjective)
decEq (OnLeft x) (OnRight y) = No (\Refl impossible)
decEq (OnRight x) AtRoot = No (\Refl impossible)
decEq (OnRight x) (OnLeft y) = No (\Refl impossible)
decEq (OnRight x) (OnRight y) with (decEq x y)
decEq (OnRight x) (OnRight x) | (Yes Refl) = Yes Refl
decEq (OnRight x) (OnRight y) | (No contra) = No (contra . onRightInjective)
这证明Nodups t蕴含InjTree t:
noDupsInj : (t : Tree a) -> NoDups t -> InjTree t
noDupsInj t nd x loc1 loc2 with (decEq loc1 loc2)
noDupsInj t nd x loc1 loc2 | (Yes prf) = prf
noDupsInj t nd x loc1 loc2 | (No contra) = absurd $ nd x x loc1 loc2 contra Refl
最后，NoDups t 完成了工作。
travsDet2 : (t, u : Tree a) -> NoDups t -> preorder t = preorder u -> inorder t = inorder u -> t = u
travsDet2 t u ndt = travsDet t u (noDupsInj t ndt)
假设您有以下预序遍历：a,b,c,d,e,f,g。这告诉你什么？
你知道 a 是树的根，这是从前序遍历的定义得出的。到目前为止，还不错。
你也知道你列表的其余部分是先遍历左子树再遍历右子树。不幸的是你不知道分裂在哪里。可以是都属于左树，也可以是都属于右树，或者b,c向左d,e,f,g向右等等
如何解决歧义？那么我们来看一下中序遍历，它的定义属性是什么？在中序遍历中，a 左子树中的任何元素都将出现在 a 之前，而右子树中的任何元素都将出现在 a 之后。同样，这遵循中序遍历的定义。
所以我们需要做的是看一下中序遍历（假设是c,b,a,d,e,f,g）。我们可以看到 b 和 c 出现在 a 之前，因此它们在左子树中，而 d、e、f和 g 在右子树中。换句话说，as 在中序遍历中的位置唯一确定了哪些节点将在其 left/right 子树中。
这很好，因为我们现在可以继续递归求解两个子树：预序 b,c/in-order c,b 和预序 d,e,f,g/in -顺序 d,e,f,g.
并且您可以递归地继续此操作，直到所有子树仅包含一个元素，其中解决方案非常独特。
而且由于在每一步我们都可以证明只有一种有效的继续方式，结果是给定的一对中序和前序遍历只能属于一棵树。
如果你喜欢更正式的符号，你可以找到完全相同的证明here。
为了创建树，我们需要一个根节点和一个放置顺序。
Preorder/postorder 提供根节点，而 inorder 提供放置顺序。因此，根据这种推理，我们需要两次遍历，先序或后序以及中序来创建唯一的树。
如果它是 BST，那么 Preorder 或 Postorder 就足够了，因为我们已经知道节点的放置顺序。
这是对问题的直观推理。