Как inorder + preorder создает уникальное бинарное дерево?

В последнее время мои вопросы были отмечены как дубликаты, например , даже если они не были. Итак, позвольте мне начать с следующего, а затем я объясню свой вопрос.

Почему этот вопрос не является дубликатом?

Я не спрашиваю, как создать двоичное дерево, когда заданы обход и предварительный обход. Я прошу доказательства, что inorder + preorder traversal определяет уникальное двоичное дерево.

Теперь, к оригинальному вопросу. Я пошел на собеседование, и интервьюер задал мне этот вопрос. Я застрял и не мог продолжить.: |

Вопрос: Предоставление обхода порядка и предзаказов двоичного дерева. Докажите, что существует только одно бинарное дерево с данными. Другими словами, доказать, что два разных бинарных дерева не могут иметь одинаковые обходы порядка и предзаказов. Предположим, что все элементы в дереве уникальны (благодаря @envy_intelligence для указания этого предположения).

Я попробовал убедить интервьюера, используя примеры, но интервьюер просил математическое/интуитивное доказательство. Может ли кто-нибудь помочь мне доказать это?

Ответ 1

Начните с обхода порядка. Либо он пуст, и в этом случае вы закончили, либо он имеет первый элемент, r0, корень дерева. Теперь выполните поиск обхода порядка r0. Левое поддерево все придет до этой точки, и после этого будет все поддерево. Таким образом, вы можете разделить обход ордера в этой точке на обход порядка левого поддерева il и обход по правому поддереву, ir.

Если il пусто, тогда остальная часть обхода предзаказа принадлежит правому поддереву, и вы можете продолжить индуктивно. Если ir пуст, то то же самое происходит с другой стороны. Если ни один из них не пуст, найдите первый элемент ir в оставшейся части обхода предзаказов. Это делит его на обход предварительного упорядочения левого поддерева и одного из правого поддерева. Индукция немедленно.

Если кто-то заинтересован в формальном доказательстве, мне (наконец) удалось создать его в Идрисе. Однако я не нашел времени, чтобы попытаться сделать его ужасно читаемым, поэтому на самом деле довольно сложно его прочитать. Я бы рекомендовал, чтобы вы смотрели в основном на типы верхнего уровня (например, леммы, теоремы и определения) и старались избегать слишком увязнуть в доказательствах (терминах).

Сначала несколько предварительных результатов:

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

Теперь вторая большая идея: идея способа найти определенный элемент в определенном дереве. Это тесно связано с типом Elem в Data.List, который выражает способ поиска определенного элемента в определенном списке.

data InTree : a -> Tree a -> Type where
  AtRoot : x `InTree` (Node l x r)
  OnLeft : x `InTree` l -> x `InTree` (Node l v r)
  OnRight : x `InTree` r -> x `InTree` (Node l v r)

Тогда есть целый ряд ужасных лемм, несколько из которых были предложены Эриком Мертенсом (glguy) в его ответ на мой вопрос об этом.

Ужасные леммы

size : Tree a -> 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)

Хорошо до сих пор? Рад слышать это. Теорема, которую вы ищете, быстро приближается! Во-первых, нам нужно понятие дерева, которое является "инъективным", что, по моему мнению, является самым простым понятием "не имеет дубликатов" в этом контексте. Не беспокойтесь, если вам не нравится это понятие; там еще один на юг пути. Это говорит о том, что дерево t является инъективным, если каждый раз loc1 и loc1 - это способы найти значение x в t, 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 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 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 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

Основная цель!

Если 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

Альтернативное понятие "без дубликатов"

Можно сказать, что дерево "не имеет дубликатов", если каждый раз, когда два дерева в дереве не равны, следует, что они не содержат один и тот же элемент. Это можно выразить с помощью типа 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)

Ответ 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 в обходном порядке однозначно определяет, какие узлы будут в своих левых/правых поддеревах.

И это здорово, потому что мы можем теперь продолжить и рекурсивно решить два поддеревья: предварительный порядок b,c/in-order c,b и предварительный порядок d,e,f,g/in-order d,e,f,g.

И вы можете продолжить эту рекурсию, пока все поддеревья не содержат только один элемент, где решение тривиально уникально.

И так как на каждом шаге мы могли бы доказать, что существует только один действительный путь, результат состоит в том, что данная пара обходов порядка и предзаказов может принадлежать только одному дереву.

Если вы предпочитаете более формальную нотацию, вы можете найти точно такое же доказательство здесь.

Ответ 3

Один вопрос, который я задал бы интервьюеру, касается повторных элементов. Два "разных" бинарных дерева могут иметь одинаковые предзаказы и обходные пути, если они имеют повторяющиеся элементы.

В качестве примера рассмотрим следующий случай:

inorder: {12, 12} preorder: {12, 12}

       12           12 

    /                  \

 12                     12

Теперь подходит к случаю, когда есть уникальные элементы. Когда мы рекурсивно подходим к проблеме, мы всегда можем разбить более крупные множества на кортежи 3. Скажем, мы обходим по порядку как {Left, Root, Right} и pre-order Traversal как {Root, Left, Right}.

Когда мы фиксируем Root из обхода предзаказов, остальную часть обхода предзаказа следует рассматривать как две части, чьи дальнейшие подробности могут быть получены из обхода порядка. Обратите внимание, что на каждом этапе мы пытаемся решить стандартную трехмерную проблему node: нам может не все равно, сколько "подзадач" каждый node имеет, потому что мы знаем, что мы доберемся до этого момента.