General Trees with Arbitrary Arities

This file defines general tree data structures where nodes can have an arbitrary number of children (represented as lists).

We provide two main variants:

• GeneralTree: Trees where every node (including internal nodes) holds a value
• GeneralLeafTree: Trees where only leaf nodes hold values, internal nodes are structural

Both support arbitrary arities and include helper functions for common operations like finding paths, checking properties, and accessing structure information.

inductive GeneralTree (α : Type u_1) : Type u_1

A general tree with arbitrary arity where every node (including internal nodes) holds a value. The children are represented as a list, allowing for any number of child nodes.

• leaf {α : Type u_1} : α → GeneralTree α
• node {α : Type u_1} : α → List (GeneralTree α) → GeneralTree α
• nil {α : Type u_1} : GeneralTree α

instance instInhabitedGeneralTree {a✝ : Type u_1} : Inhabited (GeneralTree a✝)

Equations

• instInhabitedGeneralTree = { default := GeneralTree.nil }

instance instReprGeneralTree {α✝ : Type u_1} [Repr α✝] : Repr (GeneralTree α✝)

Equations

• instReprGeneralTree = { reprPrec := reprGeneralTree✝ }

inductive GeneralLeafTree (α : Type u_1) : Type u_1

A general tree with arbitrary arity where only leaf nodes hold values. Internal nodes are purely structural and do not store values. Used as input to general Merkle tree construction.

• leaf {α : Type u_1} : α → GeneralLeafTree α
• node {α : Type u_1} : List (GeneralLeafTree α) → GeneralLeafTree α
• nil {α : Type u_1} : GeneralLeafTree α

instance instInhabitedGeneralLeafTree {a✝ : Type u_1} : Inhabited (GeneralLeafTree a✝)

Equations

• instInhabitedGeneralLeafTree = { default := GeneralLeafTree.node default }

instance instReprGeneralLeafTree {α✝ : Type u_1} [Repr α✝] : Repr (GeneralLeafTree α✝)

Equations

• instReprGeneralLeafTree = { reprPrec := reprGeneralLeafTree✝ }

def GeneralTree.getRoot {α : Type u_1} : GeneralTree α → Option α

Get the root value of a general tree, if it exists.

Equations

• GeneralTree.nil.getRoot = none
• (GeneralTree.leaf a).getRoot = some a
• (GeneralTree.node a a_1).getRoot = some a

def GeneralTree.arity {α : Type u_1} : GeneralTree α → ℕ

Get the number of children of a node.

Equations

• GeneralTree.nil.arity = 0
• (GeneralTree.leaf a).arity = 0
• (GeneralTree.node a a_1).arity = a_1.length

def GeneralTree.children {α : Type u_1} : GeneralTree α → List (GeneralTree α)

Get the children of a node.

Equations

• GeneralTree.nil.children = []
• (GeneralTree.leaf a).children = []
• (GeneralTree.node a a_1).children = a_1

def GeneralTree.isLeaf {α : Type u_1} : GeneralTree α → Bool

Check if the tree is a leaf.

Equations

• (GeneralTree.leaf a).isLeaf = true
• x✝.isLeaf = false

def GeneralTree.isEmpty {α : Type u_1} : GeneralTree α → Bool

Check if the tree is empty.

Equations

• GeneralTree.nil.isEmpty = true
• x✝.isEmpty = false

def GeneralTree.findPath {α : Type u_1} [DecidableEq α] (a : α) : GeneralTree α → Option (List ℕ)

Find the path from root to a leaf with the given value. The path is represented as a list of child indices.

Equations

• GeneralTree.findPath a GeneralTree.nil = none
• GeneralTree.findPath a (GeneralTree.leaf a_1) = if a = a_1 then some [] else none
• GeneralTree.findPath a (GeneralTree.node a_1 a_2) = GeneralTree.findPath.findPathInChildren a a_2 0

def GeneralTree.findPath.findPathInChildren {α : Type u_1} [DecidableEq α] (a : α) (children : List (GeneralTree α)) (idx : ℕ) : Option (List ℕ)

Equations

• One or more equations did not get rendered due to their size.
• GeneralTree.findPath.findPathInChildren a [] idx = none

def GeneralLeafTree.arity {α : Type u_1} : GeneralLeafTree α → ℕ

Get the number of children of a node.

Equations

• GeneralLeafTree.nil.arity = 0
• (GeneralLeafTree.leaf a).arity = 0
• (GeneralLeafTree.node children).arity = children.length

def GeneralLeafTree.children {α : Type u_1} : GeneralLeafTree α → List (GeneralLeafTree α)

Get the children of a node.

Equations

• GeneralLeafTree.nil.children = []
• (GeneralLeafTree.leaf a).children = []
• (GeneralLeafTree.node children).children = children

def GeneralLeafTree.isLeaf {α : Type u_1} : GeneralLeafTree α → Bool

Check if the tree is a leaf.

Equations

• (GeneralLeafTree.leaf a).isLeaf = true
• x✝.isLeaf = false

def GeneralLeafTree.isEmpty {α : Type u_1} : GeneralLeafTree α → Bool

Check if the tree is empty.

Equations

• GeneralLeafTree.nil.isEmpty = true
• x✝.isEmpty = false

def GeneralLeafTree.findPath {α : Type u_1} [DecidableEq α] (a : α) : GeneralLeafTree α → Option (List ℕ)

Find the path from root to a leaf with the given value. The path is represented as a list of child indices.

Equations

• GeneralLeafTree.findPath a GeneralLeafTree.nil = none
• GeneralLeafTree.findPath a (GeneralLeafTree.leaf a_1) = if a = a_1 then some [] else none
• GeneralLeafTree.findPath a (GeneralLeafTree.node children) = GeneralLeafTree.findPath.findPathInChildren a children 0

def GeneralLeafTree.findPath.findPathInChildren {α : Type u_1} [DecidableEq α] (a : α) (children : List (GeneralLeafTree α)) (idx : ℕ) : Option (List ℕ)

Equations

• One or more equations did not get rendered due to their size.
• GeneralLeafTree.findPath.findPathInChildren a [] idx = none

def GeneralTree.example : GeneralTree (Fin 10)

Equations

• One or more equations did not get rendered due to their size.

def GeneralLeafTree.example : GeneralLeafTree (Fin 10)

Equations

• One or more equations did not get rendered due to their size.