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

def BinaryTree.Skeleton.depth : Skeleton → ℕ

Depth of a Skeleton, measured as the maximum number of edges from the root to a leaf. A standalone leaf has depth 0, and an internal node has depth one more than the deeper child.

def BinaryTree.Skeleton.leafCount : Skeleton → ℕ

Number of leaves of a Skeleton. A leaf contributes one, and an internal node sums the leaf counts of its children.

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)

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

@[implicit_reducible]

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

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

Building full trees

Two dual constructions of FullData trees:

• LeafData.populateUp — bottom-up. Given a leaf-valued tree and a binary composition function, fill internal nodes by recursively composing the child subtrees' root values. (This is the standard Merkle-tree build.)
• populateDown — top-down. Given a skeleton, a child-decomposition function α → α × α, and a root value, recursively expand each node by applying the function to obtain its two children.

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

Bottom-up tree population: fill internal nodes by composing child subtrees' root values via compose.

@[simp]

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

@[simp]

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

@[simp]

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

def BinaryTree.populateDown {α : Type u_1} (s : Skeleton) (children : α → α × α) (root : α) : FullData α s

Top-down tree population: fill nodes by recursively expanding the input root into a pair of child values via children.

@[simp]

theorem BinaryTree.populateDown_leaf {β : Type u_1} (children : β → β × β) (root : β) : populateDown Skeleton.leaf children root = FullData.leaf root

For a leaf skeleton, populateDown returns a single-leaf FullData carrying root.

@[simp]

theorem BinaryTree.populateDown_internal_def {β : Type u_1} {sl sr : Skeleton} (children : β → β × β) (root : β) : populateDown (sl.internal sr) children root = FullData.internal root (populateDown sl children (children root).fst) (populateDown sr children (children root).snd)

For an internal skeleton, populateDown unfolds to a FullData.internal whose subtrees are recursively populated from the projections of children root.

This holds by rfl thanks to Prod-eta: the let ⟨l, r⟩ := children root in the definition is Prod.casesOn (children root) _, and Prod-eta makes Prod.casesOn p f = f p.1 p.2 definitional.

@[simp]

theorem BinaryTree.populateDown_getRootValue {β : Type u_1} {s : Skeleton} (children : β → β × β) (root : β) : (populateDown s children root).getRootValue = root

The root value of populateDown is the input root.

theorem BinaryTree.populateDown_none_get_eq_none {α : Type u_1} {s : Skeleton} (children : Option α → Option α × Option α) (h_none : children none = (none, none)) (idx : SkeletonNodeIndex s) : (populateDown s children none).get idx = none

If children maps none ↦ (none, none), then populateDown started from none has value none at every node index.

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

Lift a binary function through two Option arguments.

def BinaryTree.Option.bindPair {α : Type u_1} {β : Type u_2} (f : α → Option (β × β)) (x : Option α) : Option β × Option β

Lift a partial child-decomposition function α → Option (β × β) through Option, returning a pair of Options. If the input or f fails, both projections are none.

@[simp]

theorem BinaryTree.Option.bindPair_some {α : Type u_1} {β : Type u_2} (f : α → Option (β × β)) (a : α) : bindPair f (some a) = (Option.map Prod.fst (f a), Option.map Prod.snd (f a))

@[simp]

theorem BinaryTree.Option.bindPair_none {α : Type u_1} {β : Type u_2} (f : α → Option (β × β)) : bindPair f none = (none, none)

def BinaryTree.optionPopulateUp {α : 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.optionPopulateUp_leaf {α : Type u_1} (a : α) (compose : α → α → Option α) : optionPopulateUp (LeafData.leaf a) compose = FullData.leaf (some a)

@[simp]

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

def BinaryTree.optionPopulateDown {α : Type u_1} (s : Skeleton) (children : α → Option (α × α)) (root : α) : FullData (Option α) s

Build a tree top-down while allowing failures in the children-decomposition function. children may return none to indicate failure; failure propagates to all descendants in the corresponding subtree.

@[simp]

theorem BinaryTree.optionPopulateDown_leaf {α : Type u_1} (children : α → Option (α × α)) (root : α) : optionPopulateDown Skeleton.leaf children root = FullData.leaf (some root)

@[simp]

theorem BinaryTree.optionPopulateDown_internal {α : Type u_1} {sl sr : Skeleton} (children : α → Option (α × α)) (root : α) : optionPopulateDown (sl.internal sr) children root = FullData.internal (some root) (populateDown sl (Option.bindPair children) (Option.map Prod.fst (children root))) (populateDown sr (Option.bindPair children) (Option.map Prod.snd (children root)))

@[simp]

theorem BinaryTree.optionPopulateDown_getRootValue {α : Type u_1} {s : Skeleton} (children : α → Option (α × α)) (root : α) : (optionPopulateDown s children root).getRootValue = some root