Lemmas about Indexed Binary Trees

TODOs

• More relationships between tree navigations
  • Which navigation sequences are equivalent to each other?
  • How do these navigations affect depth?
• API for flattening a tree to a list
• Define Lattice structure on trees
  • a subset relation on trees, mappings of indices to indices of supertrees

theorem BinaryTree.SkeletonNodeIndex.leftChild_bind_parent {s : Skeleton} (idx : SkeletonNodeIndex s) : idx.leftChild >>= parent = Option.map (fun (x : SkeletonNodeIndex s) => idx) idx.leftChild

The parent of a left child, when it exists, is the node itself.

theorem BinaryTree.SkeletonNodeIndex.rightChild_bind_parent {s : Skeleton} (idx : SkeletonNodeIndex s) : idx.rightChild >>= parent = Option.map (fun (x : SkeletonNodeIndex s) => idx) idx.rightChild

The parent of a right child, when it exists, is the node itself.

theorem BinaryTree.SkeletonNodeIndex.parent_of_depth_zero {s : Skeleton} (idx : SkeletonNodeIndex s) (h : idx.depth = 0) : idx.parent = none

The parent of a node of depth zero is none.

@[implicit_reducible]

instance BinaryTree.instFunctorLeafData {s : Skeleton} : Functor fun (α : Type u_1) => LeafData α s

@[implicit_reducible]

instance BinaryTree.instFunctorInternalData {s : Skeleton} : Functor fun (α : Type u_1) => InternalData α s

@[implicit_reducible]

instance BinaryTree.instFunctorFullData {s : Skeleton} : Functor fun (α : Type u_1) => FullData α s

instance BinaryTree.instLawfulFunctorLeafData {s : Skeleton} : LawfulFunctor fun (α : Type u_1) => LeafData α s

instance BinaryTree.instLawfulFunctorInternalData {s : Skeleton} : LawfulFunctor fun (α : Type u_1) => InternalData α s

instance BinaryTree.instLawfulFunctorFullData {s : Skeleton} : LawfulFunctor fun (α : Type u_1) => FullData α s

Skeleton size: depth and leafCount

@[simp]

theorem BinaryTree.Skeleton.depth_leaf : leaf.depth = 0

@[simp]

theorem BinaryTree.Skeleton.depth_internal (left right : Skeleton) : (left.internal right).depth = max left.depth right.depth + 1

@[simp]

theorem BinaryTree.Skeleton.leafCount_leaf : leaf.leafCount = 1

@[simp]

theorem BinaryTree.Skeleton.leafCount_internal (left right : Skeleton) : (left.internal right).leafCount = left.leafCount + right.leafCount

theorem BinaryTree.Skeleton.leafCount_pos (s : Skeleton) : 0 < s.leafCount

Every skeleton has at least one leaf.

theorem BinaryTree.SkeletonLeafIndex.depth_le_skeleton_depth {s : Skeleton} (idx : SkeletonLeafIndex s) : idx.depth ≤ s.depth

The depth of any leaf index is bounded by the depth of its skeleton.

theorem BinaryTree.SkeletonNodeIndex.depth_le_skeleton_depth {s : Skeleton} (idx : SkeletonNodeIndex s) : idx.depth ≤ s.depth

The depth of any node index is bounded by the depth of its skeleton.