Inductive Indexed Binary Trees

A Note about Process/API when working with this

I am trying to follow a process of making simp theorems and procedures that decompose the trees as much as possible.

1. Use casework to take a tree of a known structure and specify the parts of that structure
2. Push maps or other functions on this down to the bottom of the (tree / syntax tree)
3. I then have e.g. FullData.internal value1 left1 right1 = FullData.internal value2 left2 right2
4. and then I can congruence the values and subtrees

Notes & TODOs

• aesop extension for the above?

• Split off a Defs.lean file

• Functions for navigating tree

  • Go to parent if it exists
  • Go to left child if it exists
  • Go to right child if it exists
  • Go to sibling if it exists
  • Return pair of left and right children if they exist

• Define a datatype for indices of trees agnostic of the skeleton,

  • This type has an equivalence to lists of bools,
  • and maps from the the other indexing types.
  • get? functions

inductive BinaryTree.Skeleton : Type

Inductive data type for a binary tree skeleton. A skeleton is a binary tree without values, used to represent the structure of the tree.

• leaf : Skeleton
• internal : Skeleton → Skeleton → Skeleton

inductive BinaryTree.SkeletonLeafIndex : Skeleton → Type

Type of indices of leaves of a skeleton

• ofLeaf : SkeletonLeafIndex Skeleton.leaf
• ofLeft {left right : Skeleton} (idxLeft : SkeletonLeafIndex left) : SkeletonLeafIndex (left.internal right)
• ofRight {left right : Skeleton} (idxRight : SkeletonLeafIndex right) : SkeletonLeafIndex (left.internal right)

inductive BinaryTree.SkeletonInternalIndex : Skeleton → Type

Type of indices of internal nodes of a skeleton

• ofInternal {left right : Skeleton} : SkeletonInternalIndex (left.internal right)
• ofLeft {left right : Skeleton} (idxLeft : SkeletonInternalIndex left) : SkeletonInternalIndex (left.internal right)
• ofRight {left right : Skeleton} (idxRight : SkeletonInternalIndex right) : SkeletonInternalIndex (left.internal right)

inductive BinaryTree.SkeletonNodeIndex : Skeleton → Type

Type of indices of any node of a skeleton

• ofLeaf : SkeletonNodeIndex Skeleton.leaf
• ofInternal {left right : Skeleton} : SkeletonNodeIndex (left.internal right)
• ofLeft {left right : Skeleton} (idxLeft : SkeletonNodeIndex left) : SkeletonNodeIndex (left.internal right)
• ofRight {left right : Skeleton} (idxRight : SkeletonNodeIndex right) : SkeletonNodeIndex (left.internal right)

def BinaryTree.SkeletonLeafIndex.toNodeIndex {s : Skeleton} (idx : SkeletonLeafIndex s) : SkeletonNodeIndex s

Construct a SkeletonNodeIndex from a SkeletonLeafIndex

def BinaryTree.SkeletonInternalIndex.toNodeIndex {s : Skeleton} (idx : SkeletonInternalIndex s) : SkeletonNodeIndex s

Construct a SkeletonNodeIndex from a SkeletonInternalIndex

This section contains predicates about indices determined by their neighborhood in the tree.

def BinaryTree.SkeletonLeafIndex.isRoot {s : Skeleton} (idx : SkeletonLeafIndex s) : Bool

Check whether a leaf index is the root of its tree.

def BinaryTree.SkeletonInternalIndex.isRoot {s : Skeleton} (idx : SkeletonInternalIndex s) : Bool

Check whether an internal-node index is the root of its tree.

def BinaryTree.SkeletonNodeIndex.isRoot {s : Skeleton} (idx : SkeletonNodeIndex s) : Bool

Check whether a node index is the root of its tree.

def BinaryTree.SkeletonLeafIndex.isLeaf {s : Skeleton} : SkeletonLeafIndex s → Bool

Every SkeletonLeafIndex points to a leaf.

def BinaryTree.SkeletonInternalIndex.isLeaf {s : Skeleton} : SkeletonInternalIndex s → Bool

No SkeletonInternalIndex points to a leaf.

def BinaryTree.SkeletonNodeIndex.isLeaf {s : Skeleton} (idx : SkeletonNodeIndex s) : Bool

Check whether a node index points to a leaf of the tree.

inductive BinaryTree.LeafData (α : Type u_1) : Skeleton → Type u_1

A binary tree with values stored at leaves.

• leaf {α : Type u_1} (value : α) : LeafData α Skeleton.leaf
• internal {α : Type u_1} {left right : Skeleton} (leftData : LeafData α left) (rightData : LeafData α right) : LeafData α (left.internal right)

def BinaryTree.instReprLeafData.repr {α✝ : Type u_1} {a✝ : Skeleton} [Repr α✝] : LeafData α✝ a✝ → ℕ → Std.Format

@[implicit_reducible]

instance BinaryTree.instReprLeafData {α✝ : Type u_1} {a✝ : Skeleton} [Repr α✝] : Repr (LeafData α✝ a✝)

inductive BinaryTree.InternalData (α : Type u_1) : Skeleton → Type u_1

A binary tree with values stored in internal nodes.

• leaf {α : Type u_1} : InternalData α Skeleton.leaf
• internal {α : Type u_1} {left right : Skeleton} (value : α) (leftData : InternalData α left) (rightData : InternalData α right) : InternalData α (left.internal right)

def BinaryTree.instReprInternalData.repr {α✝ : Type u_1} {a✝ : Skeleton} [Repr α✝] : InternalData α✝ a✝ → ℕ → Std.Format

@[implicit_reducible]

instance BinaryTree.instReprInternalData {α✝ : Type u_1} {a✝ : Skeleton} [Repr α✝] : Repr (InternalData α✝ a✝)

inductive BinaryTree.FullData (α : Type u_1) : Skeleton → Type u_1

A binary tree with values stored at both leaves and internal nodes.

• leaf {α : Type u_1} (value : α) : FullData α Skeleton.leaf
• internal {α : Type u_1} {left right : Skeleton} (value : α) (leftData : FullData α left) (rightData : FullData α right) : FullData α (left.internal right)

@[implicit_reducible]

instance BinaryTree.instReprFullData {α✝ : Type u_1} {a✝ : Skeleton} [Repr α✝] : Repr (FullData α✝ a✝)

def BinaryTree.instReprFullData.repr {α✝ : Type u_1} {a✝ : Skeleton} [Repr α✝] : FullData α✝ a✝ → ℕ → Std.Format

def BinaryTree.LeafData.leftSubtree {α : Type u_1} {s_left s_right : Skeleton} (tree : LeafData α (s_left.internal s_right)) : LeafData α s_left

Get the left subtree of a LeafData.

def BinaryTree.LeafData.rightSubtree {α : Type u_1} {s_left s_right : Skeleton} (tree : LeafData α (s_left.internal s_right)) : LeafData α s_right

Get the right subtree of a LeafData.

def BinaryTree.InternalData.leftSubtree {α : Type u_1} {s_left s_right : Skeleton} (tree : InternalData α (s_left.internal s_right)) : InternalData α s_left

Get the left subtree of a InternalData.

def BinaryTree.InternalData.rightSubtree {α : Type u_1} {s_left s_right : Skeleton} (tree : InternalData α (s_left.internal s_right)) : InternalData α s_right

Get the right subtree of a InternalData.

def BinaryTree.FullData.leftSubtree {α : Type u_1} {s_left s_right : Skeleton} (tree : FullData α (s_left.internal s_right)) : FullData α s_left

Get the left subtree of a FullData.

def BinaryTree.FullData.rightSubtree {α : Type u_1} {s_left s_right : Skeleton} (tree : FullData α (s_left.internal s_right)) : FullData α s_right

Get the right subtree of a FullData.

@[simp]

theorem BinaryTree.LeafData.leftSubtree_internal {α : Type u_1} {s_left s_right : Skeleton} (left : LeafData α s_left) (right : LeafData α s_right) : (left.internal right).leftSubtree = left

@[simp]

theorem BinaryTree.LeafData.rightSubtree_internal {α : Type u_1} {s_left s_right : Skeleton} (left : LeafData α s_left) (right : LeafData α s_right) : (left.internal right).rightSubtree = right

@[simp]

theorem BinaryTree.InternalData.leftSubtree_internal {α : Type u_1} {s_left s_right : Skeleton} (value : α) (left : InternalData α s_left) (right : InternalData α s_right) : (internal value left right).leftSubtree = left

@[simp]

theorem BinaryTree.InternalData.rightSubtree_internal {α : Type u_1} {s_left s_right : Skeleton} (value : α) (left : InternalData α s_left) (right : InternalData α s_right) : (internal value left right).rightSubtree = right

@[simp]

theorem BinaryTree.FullData.leftSubtree_internal {α : Type u_1} {s_left s_right : Skeleton} (value : α) (left : FullData α s_left) (right : FullData α s_right) : (internal value left right).leftSubtree = left

@[simp]

theorem BinaryTree.FullData.rightSubtree_internal {α : Type u_1} {s_left s_right : Skeleton} (value : α) (left : FullData α s_left) (right : FullData α s_right) : (internal value left right).rightSubtree = right

def BinaryTree.LeafData.get {s : Skeleton} {α : Type u_1} (tree : LeafData α s) (idx : SkeletonLeafIndex s) : α

Get a value of a LeafData at an index.

def BinaryTree.InternalData.get {s : Skeleton} {α : Type u_1} (tree : InternalData α s) (idx : SkeletonInternalIndex s) : α

Get a value of a InternalData at an index.

def BinaryTree.FullData.get {s : Skeleton} {α : Type u_1} (tree : FullData α s) (idx : SkeletonNodeIndex s) : α

Get a value of a FullData at an index.

@[simp]

theorem BinaryTree.LeafData.get_leaf {α : Type u_1} (a : α) : (leaf a).get SkeletonLeafIndex.ofLeaf = a

@[simp]

theorem BinaryTree.LeafData.get_ofLeft {s_left s_right : Skeleton} {α : Type u_1} (tree : LeafData α (s_left.internal s_right)) (idxLeft : SkeletonLeafIndex s_left) : tree.get idxLeft.ofLeft = tree.leftSubtree.get idxLeft

@[simp]

theorem BinaryTree.LeafData.get_ofRight {s_left s_right : Skeleton} {α : Type u_1} (tree : LeafData α (s_left.internal s_right)) (idxRight : SkeletonLeafIndex s_right) : tree.get idxRight.ofRight = tree.rightSubtree.get idxRight

@[simp]

theorem BinaryTree.LeafData.get_internal_ofLeft {α : Type u_1} {s_left s_right : Skeleton} (left : LeafData α s_left) (right : LeafData α s_right) (idxLeft : SkeletonLeafIndex s_left) : (left.internal right).get idxLeft.ofLeft = left.get idxLeft

@[simp]

theorem BinaryTree.LeafData.get_internal_ofRight {α : Type u_1} {s_left s_right : Skeleton} (left : LeafData α s_left) (right : LeafData α s_right) (idxRight : SkeletonLeafIndex s_right) : (left.internal right).get idxRight.ofRight = right.get idxRight

@[simp]

theorem BinaryTree.FullData.get_leaf {α : Type u_1} (a : α) : (leaf a).get SkeletonNodeIndex.ofLeaf = a

@[simp]

theorem BinaryTree.InternalData.get_internal {α : Type u_1} {s_left s_right : Skeleton} (value : α) (left : InternalData α s_left) (right : InternalData α s_right) : (internal value left right).get SkeletonInternalIndex.ofInternal = value

@[simp]

theorem BinaryTree.InternalData.get_ofLeft {s_left s_right : Skeleton} {α : Type u_1} (tree : InternalData α (s_left.internal s_right)) (idxLeft : SkeletonInternalIndex s_left) : tree.get idxLeft.ofLeft = tree.leftSubtree.get idxLeft

@[simp]

theorem BinaryTree.InternalData.get_ofRight {s_left s_right : Skeleton} {α : Type u_1} (tree : InternalData α (s_left.internal s_right)) (idxRight : SkeletonInternalIndex s_right) : tree.get idxRight.ofRight = tree.rightSubtree.get idxRight

@[simp]

theorem BinaryTree.InternalData.get_internal_ofLeft {α : Type u_1} {s_left s_right : Skeleton} (value : α) (left : InternalData α s_left) (right : InternalData α s_right) (idxLeft : SkeletonInternalIndex s_left) : (internal value left right).get idxLeft.ofLeft = left.get idxLeft

@[simp]

theorem BinaryTree.InternalData.get_internal_ofRight {α : Type u_1} {s_left s_right : Skeleton} (value : α) (left : InternalData α s_left) (right : InternalData α s_right) (idxRight : SkeletonInternalIndex s_right) : (internal value left right).get idxRight.ofRight = right.get idxRight

@[simp]

theorem BinaryTree.FullData.get_internal {α : Type u_1} {s_left s_right : Skeleton} (value : α) (left : FullData α s_left) (right : FullData α s_right) : (internal value left right).get SkeletonNodeIndex.ofInternal = value

@[simp]

theorem BinaryTree.FullData.get_ofLeft {s_left s_right : Skeleton} {α : Type u_1} (tree : FullData α (s_left.internal s_right)) (idxLeft : SkeletonNodeIndex s_left) : tree.get idxLeft.ofLeft = tree.leftSubtree.get idxLeft

@[simp]

theorem BinaryTree.FullData.get_ofRight {s_left s_right : Skeleton} {α : Type u_1} (tree : FullData α (s_left.internal s_right)) (idxRight : SkeletonNodeIndex s_right) : tree.get idxRight.ofRight = tree.rightSubtree.get idxRight

@[simp]

theorem BinaryTree.FullData.get_internal_ofLeft {α : Type u_1} {s_left s_right : Skeleton} (value : α) (left : FullData α s_left) (right : FullData α s_right) (idxLeft : SkeletonNodeIndex s_left) : (internal value left right).get idxLeft.ofLeft = left.get idxLeft

@[simp]

theorem BinaryTree.FullData.get_internal_ofRight {α : Type u_1} {s_left s_right : Skeleton} (value : α) (left : FullData α s_left) (right : FullData α s_right) (idxRight : SkeletonNodeIndex s_right) : (internal value left right).get idxRight.ofRight = right.get idxRight

def BinaryTree.FullData.toLeafData {α : Type u_1} {s : Skeleton} (tree : FullData α s) : LeafData α s

Convert a FullData to a LeafData by dropping the internal node values.

def BinaryTree.FullData.toInternalData {α : Type u_1} {s : Skeleton} (tree : FullData α s) : InternalData α s

Convert a FullData to a InternalData by dropping the leaf node values.

@[simp]

theorem BinaryTree.FullData.toLeafData_leaf {α : Type u_1} (a : α) : (leaf a).toLeafData = LeafData.leaf a

@[simp]

theorem BinaryTree.FullData.toLeafData_leftSubtree {α : Type u_1} {s_left s_right : Skeleton} (tree : FullData α (s_left.internal s_right)) : tree.toLeafData.leftSubtree = tree.leftSubtree.toLeafData

@[simp]

theorem BinaryTree.FullData.toLeafData_rightSubtree {α : Type u_1} {s_left s_right : Skeleton} (tree : FullData α (s_left.internal s_right)) : tree.toLeafData.rightSubtree = tree.rightSubtree.toLeafData

theorem BinaryTree.FullData.toLeafData_eq_leaf {α : Type u_1} (a : α) (tree : FullData α Skeleton.leaf) (h : LeafData.leaf a = tree.toLeafData) : tree = leaf a

@[simp]

theorem BinaryTree.FullData.toLeafData_internal {α : Type u_1} {s_left s_right : Skeleton} (value : α) (left : FullData α s_left) (right : FullData α s_right) : (internal value left right).toLeafData = left.toLeafData.internal right.toLeafData

def BinaryTree.getRootIndex (s : Skeleton) : SkeletonNodeIndex s

Get the root index of a skeleton.

def BinaryTree.FullData.getRootValue {s : Skeleton} {α : Type u_1} (tree : FullData α s) : α

Get the root value of a FullData.

@[simp]

theorem BinaryTree.FullData.getRootValue_leaf {α : Type u_1} (a : α) : (leaf a).getRootValue = a

@[simp]

theorem BinaryTree.FullData.internal_getRootValue {s_left s_right : Skeleton} {α : Type u_1} (value : α) (left : FullData α s_left) (right : FullData α s_right) : (internal value left right).getRootValue = value

def BinaryTree.SkeletonLeafIndex.depth {s : Skeleton} : SkeletonLeafIndex s → ℕ

Depth of a SkeletonLeafIndex

def BinaryTree.SkeletonInternalIndex.depth {s : Skeleton} : SkeletonInternalIndex s → ℕ

Depth of a SkeletonInternalIndex

def BinaryTree.SkeletonNodeIndex.depth {s : Skeleton} : SkeletonNodeIndex s → ℕ

Depth of a SkeletonNodeIndex

def BinaryTree.SkeletonNodeIndex.parent {s : Skeleton} (idx : SkeletonNodeIndex s) : Option (SkeletonNodeIndex s)

Get the parent of a SkeletonNodeIndex, or none if the index is the root.

def BinaryTree.SkeletonNodeIndex.sibling {s : Skeleton} (idx : SkeletonNodeIndex s) : Option (SkeletonNodeIndex s)

Return the sibling node index of a given SkeletonNodeIndex. Or none if the node is the root.

def BinaryTree.SkeletonNodeIndex.leftChild {s : Skeleton} (idx : SkeletonNodeIndex s) : Option (SkeletonNodeIndex s)

Return the left child of a SkeletonNodeIndex, or none if the index is a leaf.

def BinaryTree.SkeletonNodeIndex.rightChild {s : Skeleton} (idx : SkeletonNodeIndex s) : Option (SkeletonNodeIndex s)

Return the right child of a SkeletonNodeIndex, or none if the index is a leaf.

def BinaryTree.SkeletonNodeIndex.path {s : Skeleton} (idx : SkeletonNodeIndex s) : List (SkeletonNodeIndex s)

Given a Skeleton, and a node index of the skeleton, return a list of node indices which are the ancestors of the node, starting with the root node, and going down to but not including the node itself.

def BinaryTree.FullData.copath {α : Type u_1} {s : Skeleton} (cache_tree : FullData α s) : SkeletonLeafIndex s → List α

Find the siblings of a node and its ancestors, starting with the child of the root

def BinaryTree.LeafData.map {α : Type u_1} {β : Type u_2} (f : α → β) {s : Skeleton} (tree : LeafData α s) : LeafData β s

Apply a function to every value stored in a LeafData.

def BinaryTree.InternalData.map {α : Type u_1} {β : Type u_2} (f : α → β) {s : Skeleton} (tree : InternalData α s) : InternalData β s

Apply a function to every value stored in an InternalData.

def BinaryTree.FullData.map {α : Type u_1} {β : Type u_2} (f : α → β) {s : Skeleton} (tree : FullData α s) : FullData β s

Apply a function to every value stored in a FullData.

@[simp]

theorem BinaryTree.FullData.map_leaf {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : map f (leaf a) = leaf (f a)

@[simp]

theorem BinaryTree.FullData.map_internal {α : Type u_1} {β : Type u_2} {s_left s_right : Skeleton} (f : α → β) (value : α) (left : FullData α s_left) (right : FullData α s_right) : map f (internal value left right) = internal (f value) (map f left) (map f right)

@[simp]

theorem BinaryTree.LeafData.map_leaf {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : map f (leaf a) = leaf (f a)

@[simp]

theorem BinaryTree.LeafData.map_internal {α : Type u_1} {β : Type u_2} {s_left s_right : Skeleton} (f : α → β) (left : LeafData α s_left) (right : LeafData α s_right) : map f (left.internal right) = (map f left).internal (map f right)

theorem BinaryTree.FullData.map_getRootValue {α : Type u_1} {β : Type u_2} {s : Skeleton} (f : α → β) (tree : FullData α s) : (map f tree).getRootValue = f tree.getRootValue

Build

This section contains theorems about building full trees from leaf trees.

def BinaryTree.LeafData.composeBuild {α : Type u_1} {s : Skeleton} (leaf_data_tree : LeafData α s) (compose : α → α → α) : FullData α s

Build a FullData tree by hashing together the roots of child subtrees.

@[simp]

theorem BinaryTree.LeafData.composeBuild_leaf {α : Type u_1} (a : α) (compose : α → α → α) : (leaf a).composeBuild compose = FullData.leaf a

@[simp]

theorem BinaryTree.LeafData.composeBuild_internal {α : Type u_1} {s_left s_right : Skeleton} (left : LeafData α s_left) (right : LeafData α s_right) (compose : α → α → α) : (left.internal right).composeBuild compose = FullData.internal (compose (left.composeBuild compose).getRootValue (right.composeBuild compose).getRootValue) (left.composeBuild compose) (right.composeBuild compose)

@[simp]

theorem BinaryTree.LeafData.composeBuild_getRootValue {α : Type u_1} {s_left s_right : Skeleton} (left : LeafData α s_left) (right : LeafData α s_right) (compose : α → α → α) : ((left.internal right).composeBuild compose).getRootValue = compose (left.composeBuild compose).getRootValue (right.composeBuild compose).getRootValue

def BinaryTree.Option.doubleBind {α β γ : Type u_1} (f : α → β → Option γ) (x : Option α) (y : Option β) : Option γ

Lift a binary function through two Option arguments.

def BinaryTree.LeafData.optionComposeBuild {α : Type u_1} {s : Skeleton} (leaf_data_tree : LeafData α s) (compose : α → α → Option α) : FullData (Option α) s

Build a tree while allowing failures in the composition function.

@[simp]

theorem BinaryTree.LeafData.optionComposeBuild_leaf {α : Type u_1} (a : α) (compose : α → α → Option α) : (leaf a).optionComposeBuild compose = FullData.leaf (some a)

@[simp]

theorem BinaryTree.LeafData.optionComposeBuild_internal {α : Type u_1} {s_left s_right : Skeleton} (left : LeafData α s_left) (right : LeafData α s_right) (compose : α → α → Option α) : (left.internal right).optionComposeBuild compose = FullData.internal (Option.doubleBind compose (left.optionComposeBuild compose).getRootValue (right.optionComposeBuild compose).getRootValue) (left.optionComposeBuild compose) (right.optionComposeBuild compose)