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

Question

最近,我的问题被标记为重复,就像这样,即使它们不是.所以,让我先从下面开始,然后我将解释我的问题.

为什么这个问题不重复？

我不是在询问如何在顺序和前序遍历时创建二叉树.我要求证明,inorder + preorder遍历定义了一个唯一的二叉树.

现在,原来的问题.我去面试,面试官问我这个问题.我被困住了,无法继续.:|

问题: 给定二进制树的inorder和preorder遍历.证明给定数据只有一个二叉树.换句话说,证明两个不同的二叉树不能具有相同的顺序和前序遍历.假设树中的所有元素都是唯一的(感谢@envy_intelligence指出这个假设).

我尝试使用例子说服采访者,但采访者要求数学/直觉证明.任何人都可以帮我证明吗？

Answer 1

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.

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).

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

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)

Then there are a whole slew of horrible lemmas, a couple of which were suggested by Eric Mertens (glguy) in his answer to my question about it.

Horrible lemmas

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)

Correspondence between a tree and its inorder traversal

These horrible lemmas lead up to the following theorems about inorder traversals, which together demonstrate a one-to-one correspondence between ways to find a particular element in a tree and ways to find that element in its inorder traversal.

---------------------------
-- tThenInorder is a bijection from ways to find a particular element in a tree
-- and ways to find that element in its inorder traversal. `inorderToFro`
-- and `inorderFroTo` together demonstrate this by showing that `inorderThenT` is
-- its inverse.

||| `tThenInorder t` is a retraction of `inorderThenT t`
inorderFroTo : {x : a} -> (t : Tree a) -> (loc : x `Elem` inorder t) -> tThenInorder t (inorderThenT t loc) = loc
inorderFroTo Tip loc = absurd loc
inorderFroTo (Node l v r) loc with (listSplit (inorder l) (v :: inorder r) loc) proof prf
  inorderFroTo (Node l v r) loc | (Left here) =
    rewrite inorderFroTo l here in splitLeft _ _ loc prf
  inorderFroTo (Node l v r) loc | (Right Here) = splitMiddle prf
  inorderFroTo (Node l v r) loc | (Right (There x)) =
    rewrite inorderFroTo r x in splitRight prf

||| `inorderThenT t` is a retraction of `tThenInorder t`
inorderToFro : {x : a} -> (t : Tree a) -> (loc : x `InTree` t) -> inorderThenT t (tThenInorder t loc) = loc
inorderToFro (Node l v r) (OnLeft xInL) =
  rewrite unsplitLeft {ys = v :: inorder r} (tThenInorder l xInL)
  in cong $ inorderToFro _ xInL
inorderToFro (Node l x r) AtRoot =
  rewrite unsplitRight {x} {xs = inorder l} {ys = x :: inorder r} (tThenInorder (Node Tip x r) AtRoot)
  in Refl
inorderToFro {x} (Node l v r) (OnRight xInR) =
  rewrite unsplitRight {x} {xs = inorder l} {ys = v :: inorder r} (tThenInorder (Node Tip v r) (OnRight xInR))
  in cong $ inorderToFro _ xInR

树与其前序遍历之间的对应关系

然后可以使用许多相同的引理来证明前序遍历的相应定理:

preorder : Tree a -> List a
preorder Tip = []
preorder (Node l v r) = v :: (preorder l ++ preorder r)

tThenPreorder : (t : Tree a) -> x `InTree` t -> x `Elem` preorder t
tThenPreorder Tip AtRoot impossible
tThenPreorder (Node l x r) AtRoot = Here
tThenPreorder (Node l v r) (OnLeft loc) = appendElem _ _ (There (tThenPreorder _ loc))
tThenPreorder (Node l v r) (OnRight loc) = elemAppend (v :: preorder l) (preorder r) (tThenPreorder _ loc)

mutual
  preorderThenT : (t : Tree a) -> x `Elem` preorder t -> x `InTree` t
  preorderThenT {x = x} (Node l x r) Here = AtRoot
  preorderThenT {x = x} (Node l v r) (There y) = preorderThenT_lem (listSplit _ _ y)

  preorderThenT_lem : Either (x `Elem` preorder l) (x `Elem` preorder r) -> x `InTree` (Node l v r)
  preorderThenT_lem {x = x} {l = l} {v = v} {r = r} (Left lloc) = OnLeft (preorderThenT l lloc)
  preorderThenT_lem {x = x} {l = l} {v = v} {r = r} (Right rloc) = OnRight (preorderThenT r rloc)

splitty : Right pl = listSplit xs ys loc -> elemAppend xs ys pl = loc
splitty {pl = Here} {xs = xs} {ys = (x :: zs)} {loc = loc} prf = splitMiddle prf
splitty {pl = (There x)} {xs = xs} {ys = (y :: zs)} {loc = loc} prf = splitRight prf

preorderFroTo : {x : a} -> (t : Tree a) -> (loc : x `Elem` preorder t) ->
                tThenPreorder t (preorderThenT t loc) = loc
preorderFroTo Tip Here impossible
preorderFroTo (Node l x r) Here = Refl
preorderFroTo (Node l v r) (There loc) with (listSplit (preorder l) (preorder r) loc) proof spl
  preorderFroTo (Node l v r) (There loc) | (Left pl) =
    rewrite sym (splitLeft {e=pl} (preorder l) (preorder r) loc spl)
    in cong {f = There} $ cong {f = appendElem (preorder l) (preorder r)} (preorderFroTo _ _)
  preorderFroTo (Node l v r) (There loc) | (Right pl) =
      rewrite preorderFroTo r pl in cong {f = There} (splitty spl)

preorderToFro : {x : a} -> (t : Tree a) -> (loc : x `InTree` t) -> preorderThenT t (tThenPreorder t loc) = loc
preorderToFro (Node l x r) AtRoot = Refl
preorderToFro (Node l v r) (OnLeft loc) =
  rewrite unsplitLeft {ys = preorder r} (tThenPreorder l loc)
  in cong {f = OnLeft} (preorderToFro l loc)
preorderToFro (Node l v r) (OnRight loc) =
  rewrite unsplitRight {xs = preorder l} (tThenPreorder r loc)
  in cong {f = OnRight} (preorderToFro r loc)

目前很好？很高兴听见.你寻求的定理快到了!首先,我们需要一个树是"内射"的概念,我认为这是在这种情况下"没有重复"的最简单的概念.如果你不喜欢这个概念,不要担心; 南方还有一个方向.这其中一个是说树t是单射,如果一旦loc1和loc1办法找到一个值x的t,loc1必须等于loc2.

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

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

More horrible lemmas

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

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

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)

This proves that Nodups t implies 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

Finally, it follows immediately that NoDups t gets the job done.

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)

Answer 2

想象一下,您有以下预订遍历: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在右子树.换句话说,a有序遍历中的s位置唯一地确定哪些节点将在其左/右子树中.

这很好,因为我们现在可以继续递归地解决两个子树:预订b,c/有序c,b和预订d,e,f,g/有序d,e,f,g.

并且您可以递归地继续此操作,直到所有子树只包含单个元素,其中解决方案非常简单.

并且因为在每一步我们都可以证明只有一种有效的方法可以继续,结果是一对给定的有序和预先遍历遍历只能属于一棵树.

如果您更喜欢更正式的符号,可以在这里找到完全相同的证明.