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

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)然后有一大堆可怕的引理，其中一些是由 Eric Mertens (glguy) 在他对我的问题的回答.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.size : Tree a -> Natsize Tip = Zsize (Node l v r) = size l + (S Z + size r)onLeftInjective : OnLeft p = OnLeft q -> p = qonLeftInjective Refl = ReflonRightInjective : OnRight p = OnRight q -> p = qonRightInjective Refl = Reflinorder : Tree a -> List ainorder Tip = []inorder (Node l v r) = inorder l ++ [v] ++ inorder rinstance Uninhabited (Here = There y) where uninhabited Refl impossibleinstance Uninhabited (x `InTree` Tip) where uninhabited AtRoot impossibleelemAppend : {x : a} -> (ys,xs : List a) -> x `Elem` xs -> x `Elem` (ys ++ xs)elemAppend [] xs xInxs = xInxselemAppend (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 = HereappendElem (y :: zs) ys (There pr) = There (appendElem zs ys pr)tThenInorder : {x : a} -> (t : Tree a) -> x `InTree` t -> x `Elem` inorder ttThenInorder (Node l x r) AtRoot = elemAppend _ _ HeretThenInorder (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 prflistSplit : {x : a} -> (xs,ys : List a) -> x `Elem` (xs ++ ys) -> Either (x `Elem` xs) (x `Elem` ys)listSplit [] ys xelem = Right xelemlistSplit (z :: xs) ys Here = Left HerelistSplit {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 eunsplitRight {xs = []} e = ReflunsplitRight {xs = (x :: xs)} e = rewrite unsplitRight {xs} e in ReflunsplitLeft : {x : a} -> (e : x `Elem` xs) -> listSplit xs ys (appendElem xs ys e) = Left eunsplitLeft {xs = []} Here impossibleunsplitLeft {xs = (x :: xs)} Here = ReflunsplitLeft {xs = (x :: xs)} {ys} (There pr) = rewrite unsplitLeft {xs} {ys} pr in ReflsplitLeft_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) impossiblesplitLeft_lem2 : Left Here = listSplit_lem x x xs ys (listSplit xs ys z) -> VoidsplitLeft_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) impossiblesplitLeft : {x : a} -> (xs,ys : List a) -> (loc : x `Elem` (xs ++ ys)) -> Left e = listSplit {x} xs ys loc -> appendElem {x} xs ys e = locsplitLeft {e} [] ys loc prf = absurd esplitLeft (x :: xs) ys Here prf = rewrite leftInjective prf in ReflsplitLeft {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) zsplitMiddle_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 = plsplitMiddle_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 = plsplitMiddle_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 prprsplitMiddle : Right Here = listSplit xs (y::ys) loc -> elemAppend xs (y::ys) Here = locsplitMiddle {xs = []} prf = rightInjective prfsplitMiddle {xs = (x :: xs)} {loc = Here} Refl impossiblesplitMiddle {xs = (x :: xs)} {loc = (There y)} prf = cong $ splitMiddle_lem1 prfsplitRight_lem1 : Right (There pl) = listSplit (q :: xs) (y :: ys) (There z) -> Right (There pl) = listSplit xs (y :: ys) zsplitRight_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) = locsplitRight {pl = pl} {xs = []} {y = y} {ys = ys} {loc = loc} prf = rightInjective prfsplitRight {pl = pl} {xs = (x :: xs)} {y = y} {ys = ys} {loc = Here} Refl impossiblesplitRight {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 traversalThese 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) = locinorderFroTo Tip loc = absurd locinorderFroTo (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) = locinorderToFro (Node l v r) (OnLeft xInL) = rewrite unsplitLeft {ys = v :: inorder r} (tThenInorder l xInL) in cong $ inorderToFro _ xInLinorderToFro (Node l x r) AtRoot = rewrite unsplitRight {x} {xs = inorder l} {ys = x :: inorder r} (tThenInorder (Node Tip x r) AtRoot) in ReflinorderToFro {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一棵树与其前序遍历的对应关系许多相同的引理可以用来证明前序遍历的相应定理:Correspondence between a tree and its preorder traversalMany of those same lemmas can then be used to prove the corresponding theorems for preorder traversals:preorder : Tree a -> List apreorder Tip = []preorder (Node l v r) = v :: (preorder l ++ preorder r)tThenPreorder : (t : Tree a) -> x `InTree` t -> x `Elem` preorder ttThenPreorder Tip AtRoot impossibletThenPreorder (Node l x r) AtRoot = HeretThenPreorder (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 = locsplitty {pl = Here} {xs = xs} {ys = (x :: zs)} {loc = loc} prf = splitMiddle prfsplitty {pl = (There x)} {xs = xs} {ys = (y :: zs)} {loc = loc} prf = splitRight prfpreorderFroTo : {x : a} -> (t : Tree a) -> (loc : x `Elem` preorder t) -> tThenPreorder t (preorderThenT t loc) = locpreorderFroTo Tip Here impossiblepreorderFroTo (Node l x r) Here = ReflpreorderFroTo (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) = locpreorderToFro (Node l x r) AtRoot = ReflpreorderToFro (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)到目前为止还好吗?很高兴听见.您寻求的定理正在快速逼近！首先，我们需要一个树是内射"的概念，我认为这是在这种情况下没有重复"的最简单的概念.如果您不喜欢这个概念，请不要担心；南边还有一个.如果每当 loc1 和 loc1 是在 x 中找到值的方法t, loc1 必须等于 loc2.Good so far? Glad to hear it. The theorem you seek is fast approaching! First, we need a notion of a tree being "injective", which I think is the simplest notion of "has no duplicates" in this context. Don't worry if you don't like this notion; there's another one down south a ways. This one says that a tree t is injective if whenever loc1 and loc1 are ways to find a value x in t, loc1 must equal loc2.InjTree : Tree a -> TypeInjTree 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 -> TypeInjList xs = (x : a) -> (loc1, loc2 : x `Elem` xs) -> loc1 = loc2||| If a tree is injective, so is its preorder traversaltreePreInj : (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 traversaltreeInInj : (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 tinjPreTree {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 tinjInTree {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 = yheadsSame Refl = RefltailsSame : {x:a} -> {xs : List a} -> {y : a} -> {ys : List a} -> (x :: xs) = (y :: ys) -> xs = ystailsSame Refl = ReflappendLeftCancel : {xs,ys,ys' : List a} -> xs ++ ys = xs ++ ys' -> ys = ys'appendLeftCancel {xs = []} prf = prfappendLeftCancel {xs = (x :: xs)} prf = appendLeftCancel {xs} (tailsSame prf)lengthDrop : (xs,ys : List a) -> drop (length xs) (xs ++ ys) = yslengthDrop [] ys = RefllengthDrop (x :: xs) ys = lengthDrop xs yslengthTake : (xs,ys : List a) -> take (length xs) (xs ++ ys) = xslengthTake [] ys = RefllengthTake (x :: xs) ys = cong $ lengthTake xs ysappendRightCancel_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 =  => length b = length xs + length ys} eq foo baz = trans (sym bar) $ lengthAppend xs' ys in plusRightCancel (length xs) (length xs') (length ys) bazappendRightCancel : {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 foolistPartsEqLeft : {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 appeqthereInjective : There loc1 = There loc2 -> loc1 = loc2thereInjective Refl = ReflinjTail : InjList (x :: xs) -> InjList xsinjTail {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) -> VoidsplitInorder_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 tpreorderLength Tip = ReflpreorderLength (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 tinorderLength Tip = ReflinorderLength (Node l v r) = rewrite lengthAppend (inorder l) (v :: inorder r) in rewrite inorderLength l in rewrite inorderLength r in ReflpreInLength : (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 = yslsplitInorder_lem1 v [] xsr [] ysr xsInj ysInj eq locxs locys = ReflsplitInorder_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 impossiblesplitInorder_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 zsplitInorder_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 = ysrsplitInorder_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 linjLeft {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 = ReflinjRight : {l : Tree a} -> {v : a} -> {r : Tree a} -> InjTree (Node l v r) -> InjTree rinjRight {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 相等.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 emptytravsDet Tip Tip x prf prf1 = Refl-- Impossible cases: only one tree is emptytravsDet Tip (Node l v r) x Refl prf1 impossibletravsDet (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 -> TypeNoDups {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)这就证明了Nodups t意味着InjTree t:noDupsInj : (t : Tree a) -> NoDups t -> InjTree tnoDupsInj 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 立即完成工作.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 = utravsDet2 t u ndt = travsDet t u (noDupsInj t ndt) 这篇关于inorder+preorder如何构造唯一二叉树?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！ 上岸，阿里云！