如何在树及其遍历之间建立双射？

Question

我正在查看并认为在 Idris 中编写它的正式证明会很有趣。不幸的是，我很早就陷入困境，试图证明在树中查找元素的方法对应于在其中序遍历中查找它的方法（当然，我也需要为前序遍历这样做） .欢迎任何想法。我对完整的解决方案不是特别感兴趣——更多的只是帮助在正确的方向上开始。

给出

data Tree a = Tip
            | Node (Tree a) a (Tree a)

我至少可以通过两种方式将其转换为列表：

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

或

foldrTree : (a -> b -> b) -> b -> Tree a -> b
foldrTree c n Tip = n
foldrTree c n (Node l v r) = foldr c (v `c` foldrTree c n r) l
inorder = foldrTree (::) []

第二种方法似乎让几乎一切变得困难，所以我的大部分努力都集中在第一种上。我这样描述树中的位置：

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

很容易（使用inorder的第一个定义）写

inTreeThenInorder : {x : a} -> (t : Tree a) -> x `InTree` t -> x `Elem` inorder t

并且结果具有非常简单的结构，似乎相当适合证明。

写一个

的版本也不难

inorderThenInTree : x `Elem` inorder t -> x `InTree` t

不幸的是，到目前为止，我还没有想出任何方法来编写我能够证明的 inorderThenInTree 版本是 inTreeThenInorder 的逆版本。我想出的唯一一个使用

listSplit : x `Elem` xs ++ ys -> Either (x `Elem` xs) (x `Elem` ys)

我运行在试图从那里返回时遇到了麻烦。

我尝试过的一些一般想法：

使用 Vect 而不是 List 来尝试更容易地计算出左边和右边的内容。我陷入其中 "green slime"。
玩转树的旋转，甚至证明树根处的旋转会导致有充分根据的关系。（我没有玩下面的旋转，因为我从来没有想出一种方法来使用关于这些旋转的任何东西）。
尝试用有关如何到达树节点的信息来装饰树节点。我没有在这上面花很长时间，因为我想不出一种方法来通过这种方式表达任何有趣的东西。
试图构建证据证明我们在构建这样做的函数时会回到我们开始的地方。这变得非常混乱，我被困在某个地方。

Answer 1

你的 listSplit 引理是正确的。您可以使用该函数来了解目标元素是在树的左侧还是右侧。在 Agda 标准库中 listSplit 被称为 ++⁻

这是我实现中的相关行

with ++⁻ (inorder l) x∈t

这是完整的实现。我将它作为外部 link 包括在内，以避免不必要的剧透，并利用 Agda 精彩的 HTML hyperlinked，语法高亮输出。您可以点击查看任何支持词条的类型和定义。

https://glguy.net/agda-tree-inorder-elem/Tree.html

Answer 2

我能够弄清楚如何证明可以从树位置转到列表位置并从读取中引用的引理类型返回。最终，我也设法走了另一条路，尽管代码（下面）相当糟糕。幸运的是，我能够重用可怕的列表引理来证明关于前序遍历的相应定理。

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

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)

onLeftInjective : OnLeft p = OnLeft q -> p = q
onLeftInjective Refl = Refl

onRightInjective : OnRight p = OnRight q -> p = q
onRightInjective Refl = Refl

noDups : Tree a -> Type
noDups t = (x : a) -> (here, there : x `InTree` t) -> here = there

noDupsList : List a -> Type
noDupsList xs = (x : a) -> (here, there : x `Elem` xs) -> here = there

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

rotateInorder : (ll : Tree a) ->
                (vl : a) ->
                (rl : Tree a) ->
                (v : a) ->
                (r : Tree a) ->
                inorder (Node (Node ll vl rl) v r) = inorder (Node ll vl (Node rl v r))
rotateInorder ll vl rl v r =
   rewrite appendAssociative (vl :: inorder rl) [v] (inorder r)
   in rewrite sym $ appendAssociative (inorder rl) [v] (inorder r)
   in rewrite appendAssociative (inorder ll) (vl :: inorder rl) (v :: inorder r)
   in Refl


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

Answer 3

我在 Idris 中写了 inorderToFro 和 inorderFroTo 以及相关的引理。 Here's the link.

关于您的解决方案，我可以提出以下几点（无需详细说明）：

首先，splitMiddle 并不是真正必要的。如果您为 splitRight 使用更通用的 Right p = listSplit xs ys loc -> elemAppend xs ys p = loc 类型，则可以覆盖相同的地面。

其次，您可以使用更多 with 模式而不是明确的 _lem 函数；我认为它也会更清晰和更简洁。

第三，你做了大量的工作来证明 splitLeft 和合作。通常将函数的属性 移到函数内部 是有意义的。因此，我们可以将 listSplit 修改为 return 所需的证明，而不是单独编写 listSplit 及其结果的证明。这通常更容易实现。在我的解决方案中，我使用了以下类型：

data SplitRes : (x : a) -> (xs, ys : List a) -> (e : Elem x (xs ++ ys)) -> Type where
  SLeft  : (e' : Elem x xs) -> e' ++^ ys = e -> SplitRes x xs ys e
  SRight : (e' : Elem x ys) -> xs ^++ e' = e -> SplitRes x xs ys e

listSplit : (xs, ys : List a) -> (e : Elem x (xs ++ ys)) -> SplitRes x xs ys e

我也可以使用 Either (e' : Elem x xs ** (e' ++^ ys = e)) (e' : Elem x ys ** (xs ^++ e' = e)) 而不是 SplitRes。但是，我运行遇到了 Either 的问题。在我看来，Idris 中的高阶统一太不稳定了；我无法理解为什么我的 unsplitLeft 函数不会用 Either 进行类型检查。 SplitRes 在它的类型中不包含函数，所以我想这就是它工作得更顺畅的原因。

一般来说，目前我推荐 Agda 而不是 Idris 来编写这样的证明。它的检查速度更快，而且更加稳健和方便。我很惊讶你能在这里写这么多 Idris 以及关于树遍历的其他问题。

如何在树及其遍历之间建立双射？

How can I establish a bijection between a tree and its traversal?

agda

idris

如何在树及其遍历之间建立​​双射？

How can I establish a bijection between a tree and its traversal?

agda

idris

如何在树及其遍历之间建立双射？