Я смотрел на Как сделать inorder + preorder конструкцию уникальным бинарным деревом? и подумал, что было бы интересно написать официальное доказательство этого в 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, чтобы попытаться облегчить работу слева и справа. Я увяз в "зеленой слизи" этого. -
Играя с вращением дерева, дойдя до доказательства того, что вращение в корне дерева приводит к обоснованному отношению. (Я не играл с поворотами внизу, потому что я никогда не мог найти способ использовать что-либо об этих поворотах).
-
Попытка украсить узлы дерева информацией о том, как их достичь. Я не очень долго занимался этим, потому что я не мог придумать способ выразить что-либо интересное с помощью этого подхода.
-
Попытка построить доказательство того, что мы возвращаемся туда, где мы начали при создании функции, которая делает это. Это стало довольно грязным, и я где-то застрял.
