Proving some properties of binary trees and rotation in idris.

TreeRotation.idr

{-
In this file I:
- Define a binary tree.
- Define a type level predicate for right rotation of a tree. That is, this type
  can only be instantiated for trees that can be right rotated.
- Prove that it's decidable if a tree can be right-rotated or not.
- Prove that right-rotating a tree preserves in-order traversal.
-}

-- A binary tree.
data BinTree : a -> Type where
  Node : BinTree a -> BinTree a -> BinTree a
  Leaf : a -> BinTree a

-- Type level predicate that states a given binary tree can be rotated right.
-- The tree must be of the following form:
--         /\
--        /\ c
--       a b
-- Where a, b, and c are subtrees.
data CanRotateRight : (BinTree a) -> Type where
  RotateRight : (leftLeft: BinTree a) ->
                (leftRight: BinTree a) ->
                (right: BinTree a) ->
                CanRotateRight (Node (Node leftLeft leftRight) right)

-- Lemma: A tree that is a single Leaf cannot be rotated.
cannotRotateLeafLemma : CanRotateRight (Leaf x) -> Void
cannotRotateLeafLemma (RotateRight _ _ _) impossible

-- Lemma: A tree that's already associated to the right cannot be right-rotated.
-- eg: /\
--    a /\
--      b c
cannotRotateLemma : CanRotateRight (Node (Leaf x) y) -> Void
cannotRotateLemma (RotateRight _ _ _) impossible

-- Whether a tree is rotatable or not is decidable.
-- Given a tree, either prove that it can be rotated, or prove
-- that it can't be rotated.
canRotate : (tree : BinTree a) -> Dec (CanRotateRight tree)
canRotate (Node (Node x z) y) = Yes (RotateRight x z y)
canRotate (Node (Leaf x) y) = No cannotRotateLemma
canRotate (Leaf x) = No cannotRotateLeafLemma

-- Rotate a tree, given a proof that the tree can be rotated.
--   /\                /\
--  /\ c    ----->    a /\
-- a b                 b c
rotateTreeRight : (tree : BinTree a) -> (CanRotateRight tree) -> BinTree a
rotateTreeRight (Node (Node leftLeft leftRight) right) (RotateRight leftLeft leftRight right) =
  Node leftLeft (Node leftRight right)

-- In order traversal of a binary tree:
--         /\
--        /\ c
--       a b
-- Yields: [a, b, c]
inOrder : BinTree a -> List a
inOrder (Node x y) = inOrder x ++ inOrder y
inOrder (Leaf x) = [x]

-- Proof: Rotating a tree preserves in-order traversal.
rotationSameOrder : (t : BinTree a) ->
                    (prf : CanRotateRight t) ->
                    (inOrder t) = inOrder (rotateTreeRight t prf)
rotationSameOrder (Node (Node leftLeft leftRight) right) (RotateRight leftLeft leftRight right) =
  rewrite sym (appendAssociative (inOrder leftLeft) (inOrder leftRight) (inOrder right)) in Refl