Начните с обхода предзаказа. Либо он пуст, и в этом случае все готово, либо в нем есть первый элемент 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)
person
dfeuer
schedule
01.06.2015
