Как inorder+preorder создает уникальное двоичное дерево?
Недавно мои вопросы были помечены как дубликаты, даже если это не так. Итак, позвольте мне начать со следующего, а затем я объясню свой вопрос.
Почему этот вопрос не является дубликатом?
Я не спрашиваю, как создать бинарное дерево, когда дан обход и порядок. Я прошу доказательства того, что обход inorder + preorder определяет уникальное двоичное дерево.
Теперь к оригинальному вопросу. Я пошел на собеседование, и интервьюер задал мне этот вопрос. Я застрял и не мог продолжить.:|
Вопрос: Учитывая обход и предварительный порядок бинарного дерева. Докажите, что с данными можно только одно двоичное дерево. Другими словами, докажите, что два разных бинарных дерева не могут иметь одинаковый обход и предварительный порядок. Предположим, что все элементы в дереве уникальны (спасибо @envy_intelligence за указание на это предположение).
Я пытался убедить интервьюера, используя примеры, но интервьюер спрашивал математическое / интуитивное доказательство. Может ли кто-нибудь помочь мне доказать это?
3 ответа
Начните с обхода предзаказа. Либо он пуст, в этом случае вы сделали, или у него есть первый элемент, 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'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
Основная цель!
Если 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)
Представьте, что у вас есть следующий обход предварительного заказа: 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,
И вы можете продолжать это рекурсивно, пока все поддеревья не содержат только один элемент, где решение тривиально уникально.
И поскольку на каждом шаге мы можем доказать, что существует только один действительный способ продолжения, результатом является то, что данная пара обходов по порядку и по предварительному заказу может принадлежать только одному дереву.
Если вы предпочитаете более формальную запись, вы можете найти точно такое же доказательство здесь.
Один вопрос, который я бы задал интервьюеру, касается повторяющихся элементов. Два "разных" бинарных дерева могут иметь одинаковые обходы предзаказов и обходов, если они имеют повторяющиеся элементы.
В качестве примера рассмотрим следующий случай:
заказ: {12, 12} заказ: {12, 12}
12 12
/ \
12 12
Теперь подходит к случаю, когда появляются уникальные элементы. Когда мы рекурсивно подходим к проблеме, мы всегда можем разбить большие наборы на кортежи по 3. Допустим, у нас есть обход по порядку как {Left,Root,Right} и предварительный порядок обхода как {Root, Left, Right}.
Когда мы фиксируем Root от обхода предварительного заказа, остальную часть обхода предварительного заказа следует рассматривать как две части, дальнейшие детали которых можно получить из обхода порядка. Заметьте, что на каждом этапе мы пытаемся решить стандартную проблему с тремя узлами: нас может не беспокоить, сколько "подзадач" у каждого узла, потому что мы знаем, что мы доберемся до этой точки позже.
Для создания дерева нам понадобится корневой узел и порядок размещения.
Preorder / postorder предоставляет корневой узел, а inorder обеспечивает порядок размещения. Таким образом, для создания уникального дерева нам понадобятся два обхода: предварительный или последующий и неупорядоченный.
Если бы это был BST, то было бы достаточно Preorder или Postorder, поскольку мы уже знаем порядок размещения узлов.
Это интуитивное обоснование вопроса.