PossiblyInfiniteTree

This file defines a PossiblyInfiniteTree which is an InfiniteTreeSkeleton over an Option of the desired type. The offered functions are similar to the ones of InfiniteTreeSkeleton. The tree can still be infinite in both dimensions, i.e. it may have infinite depth and each node may have infinitely many (direct) children.

def InfiniteTreeSkeleton.no_orphans {α : Type u_1} (t : InfiniteTreeSkeleton (Option α)) : Prop

An InfiniteTreeSkeleton over Option has no_orphans if an element being none implies its InfiniteTreeSkeleton.childNodes also being none. That is, intuitively, every non-none node needs to have a non-none parent. This is a property that we want for possibly infinite trees but we need to be able to express it on the underlying infinite tree first.

Equations

• t.no_orphans = ∀ (subtree : InfiniteTreeSkeleton (Option α)), subtree <:+ t → subtree.root = none → ∀ (n : Option α), n ∈ subtree.childNodes → n = none

theorem InfiniteTreeSkeleton.no_orphans_closure {α : Type u_1} {t : InfiniteTreeSkeleton (Option α)} (no_orph : t.no_orphans) (subtree : InfiniteTreeSkeleton (Option α)) : subtree <:+ t → subtree.root = none → ∀ (n : Option α), n ∈ subtree → n = none

A closed version of the no_orphans property. That is, if an element is none, then not only its immediate childNodes but all nodes in all subtrees are none.

structure PossiblyInfiniteTree (α : Type u) : Type u

A PossiblyInfiniteTree is an InfiniteTreeSkeleton over Option that has no_orphans and also for each subtree, its InfiniteTreeSkeleton.childNodes have InfiniteList.no_holes. The last condition is necessary because we want the trees to be somewhat "compact", meaning that we want to forbid that e.g. the second child for a node is defined but the first child is none. Note that this would not be captured by the InfiniteTreeSkeleto.no_orphans property yet.

• infinite_tree : InfiniteTreeSkeleton (Option α)
• no_orphans : self.infinite_tree.no_orphans
• no_holes_in_children (subtree : InfiniteTreeSkeleton (Option α)) : subtree <:+ self.infinite_tree → subtree.childNodes.no_holes

Basics

The essential functions on infinite trees, mainly get, drop, and root. The childTrees function is defined separately here since it is more involved than for the InfiniteTreeSkeleton case.

def PossiblyInfiniteTree.get? {α : Type u_1} (t : PossiblyInfiniteTree α) (ns : List Nat) : Option α

Obtains the element of the tree at the given address.

Equations

• t.get? ns = t.infinite_tree.get ns

def PossiblyInfiniteTree.drop {α : Type u_1} (t : PossiblyInfiniteTree α) (ns : List Nat) : PossiblyInfiniteTree α

Obtains the subtree at the given address (by dropping everything else).

Equations

• t.drop ns = { infinite_tree := t.infinite_tree.drop ns, no_orphans := ⋯, no_holes_in_children := ⋯ }

def PossiblyInfiniteTree.root {α : Type u_1} (t : PossiblyInfiniteTree α) : Option α

Get the element at the root of the tree (i.e. at the empty address).

Equations

• t.root = t.infinite_tree.root

instance PossiblyInfiniteTree.instMembership {α : Type u_1} : Membership α (PossiblyInfiniteTree α)

Equations

• PossiblyInfiniteTree.instMembership = { mem := fun (t : PossiblyInfiniteTree α) (a : α) => some a ∈ t.infinite_tree }

theorem PossiblyInfiniteTree.mem_iff {α : Type u_1} {t : PossiblyInfiniteTree α} {e : α} : e ∈ t ↔ ∃ (ns : List Nat), t.get? ns = some e

An element is a member of the tree iff it occurs at some address.

theorem PossiblyInfiniteTree.ext {α : Type u_1} {t1 t2 : PossiblyInfiniteTree α} : (∀ (ns : List Nat), t1.get? ns = t2.get? ns) → t1 = t2

Two PossiblyInfiniteTrees are the same if they agree on all addresses.

theorem PossiblyInfiniteTree.ext_iff {α : Type u_1} {t1 t2 : PossiblyInfiniteTree α} : t1 = t2 ↔ ∀ (ns : List Nat), t1.get? ns = t2.get? ns

theorem PossiblyInfiniteTree.get?_drop {α : Type u_1} {t : PossiblyInfiniteTree α} {ns ns' : List Nat} : (t.drop ns).get? ns' = t.get? (ns ++ ns')

Get after drop can be rewritten into get.

theorem PossiblyInfiniteTree.drop_nil {α : Type u_1} {t : PossiblyInfiniteTree α} : t.drop [] = t

Dropping the empty address changes nothing.

theorem PossiblyInfiniteTree.drop_drop {α : Type u_1} {t : PossiblyInfiniteTree α} {ns ns' : List Nat} : (t.drop ns).drop ns' = t.drop (ns ++ ns')

Two calls to drop can be combined.

theorem PossiblyInfiniteTree.root_eq {α : Type u_1} {t : PossiblyInfiniteTree α} : t.root = t.get? []

The root is equal to getting the empty address.

theorem PossiblyInfiniteTree.root_mem {α : Type u_1} {t : PossiblyInfiniteTree α} (r : α) : r ∈ t.root → r ∈ t

The root is in the tree.

theorem PossiblyInfiniteTree.root_drop {α : Type u_1} {t : PossiblyInfiniteTree α} {ns : List Nat} : (t.drop ns).root = t.get? ns

The root of the dropped tree at address ns is exactly the element at address ns.

Empty Infinite Trees

The empty PossiblyInfiniteTree is simply the PossiblyInfiniteTree that is none on all addresses.

def PossiblyInfiniteTree.empty {α : Type u_1} : PossiblyInfiniteTree α

The empty PossiblyInfiniteTree is none everywhere.

Equations

• PossiblyInfiniteTree.empty = { infinite_tree := fun (x : List Nat) => none, no_orphans := ⋯, no_holes_in_children := ⋯ }

theorem PossiblyInfiniteTree.get?_empty {α : Type u_1} {n : List Nat} : empty.get? n = none

Getting from the empty tree always returns none.

theorem PossiblyInfiniteTree.drop_empty {α : Type u_1} {ns : List Nat} : empty.drop ns = empty

Dropping from the empty tree again yields the empty tree.

theorem PossiblyInfiniteTree.root_empty {α : Type u_1} : empty.root = none

The root of the empty tree is none.

theorem PossiblyInfiniteTree.empty_iff_root_none {α : Type u_1} {t : PossiblyInfiniteTree α} : t = empty ↔ t.root = none

A tree is empty if and only if the root is none.

Child Trees

Defining the childTrees function requires a bit of machinery. We only want to return the child trees that are not already empty. Then all returned trees have a non-none root, which we aim to capture directly in the return type.

@[reducible, inline]

abbrev PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot (α : Type u) : Type u

The PossiblyInfiniteTreeWithRoot is a PossiblyInfiniteTree where the root is not none.

Equations

• PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot α = { t : PossiblyInfiniteTree α // t.root ≠ none }

PossiblyInfiniteTreeWithRoot

For the PossiblyInfiniteTreeWithRoot we mainly provide some functions to convert PossiblyInfiniteTree to and from Option PossiblyInfiniteTreeWithRoot. Clearly, if a PossiblyInfiniteTree has a non-none root, we can convert it directly into a PossiblyInfiniteTreeWithRoot, otherwise, we simply convert it to none. Also in the other direction, none can just be converted to PossiblyInfiniteTree.empty and any PossiblyInfiniteTreeWithRoot is already a PossiblyInfiniteTree.

def PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot.opt_to_tree {α : Type u_1} (opt : Option (PossiblyInfiniteTreeWithRoot α)) : PossiblyInfiniteTree α

Equations

• PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot.opt_to_tree none = PossiblyInfiniteTree.empty
• PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot.opt_to_tree (some t) = t.val

def PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot.tree_to_opt {α : Type u_1} (t : PossiblyInfiniteTree α) : Option (PossiblyInfiniteTreeWithRoot α)

Equations

• PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot.tree_to_opt t = match eq : t.root with | none => none | some r => some ⟨t, ⋯⟩

theorem PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot.opt_to_tree_none_iff {α : Type u_1} {opt : Option (PossiblyInfiniteTreeWithRoot α)} : opt = none ↔ (opt_to_tree opt).root = none

theorem PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot.tree_to_opt_none_iff {α : Type u_1} {t : PossiblyInfiniteTree α} : tree_to_opt t = none ↔ t.root = none

theorem PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot.tree_to_opt_some_iff {α : Type u_1} {t : PossiblyInfiniteTree α} {t' : PossiblyInfiniteTreeWithRoot α} : tree_to_opt t = some t' ↔ t = t'.val ∧ t.root.isSome = true

theorem PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot.tree_to_opt_after_opt_to_tree {α : Type u_1} {opt : Option (PossiblyInfiniteTreeWithRoot α)} : tree_to_opt (opt_to_tree opt) = opt

theorem PossiblyInfiniteTree.PossiblyInfiniteTreeWithRoot.opt_to_tree_after_tree_to_opt {α : Type u_1} {t : PossiblyInfiniteTree α} : opt_to_tree (tree_to_opt t) = t

The actual childTrees definition

With PossiblyInfiniteTreeWithRoot in place, we can now define the actual childTrees function.

def PossiblyInfiniteTree.childTrees {α : Type u_1} (t : PossiblyInfiniteTree α) : PossiblyInfiniteList (PossiblyInfiniteTreeWithRoot α)

The childTrees of a PossiblyInfiniteTree are the PossiblyInfiniteList of all child trees that are not empty, i.e. it only consists of PossiblyInfiniteTreeWithRoot.

Equations

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

theorem PossiblyInfiniteTree.mem_childTrees_iff {α : Type u_1} {t : PossiblyInfiniteTree α} (c : PossiblyInfiniteTreeWithRoot α) : c ∈ t.childTrees ↔ c.val.infinite_tree ∈ t.infinite_tree.childTrees

PossiblyInfiniteTree.childTrees can be expressed through InfiniteTreeSkeleton.childTrees.

theorem PossiblyInfiniteTree.get?_childTrees {α : Type u_1} {t : PossiblyInfiniteTree α} (n : Nat) : t.childTrees.get? n = PossiblyInfiniteTreeWithRoot.tree_to_opt (t.drop [n])

Getting a child tree is the same as dropping the corresponding singleton address.

theorem PossiblyInfiniteTree.get?_get?_childTrees {α : Type u_1} {t : PossiblyInfiniteTree α} (n : Nat) (ns : List Nat) : (PossiblyInfiniteTreeWithRoot.opt_to_tree (t.childTrees.get? n)).get? ns = t.get? (n :: ns)

Getting at an address in a child tree can be combined into a single get call.

theorem PossiblyInfiniteTree.childTrees_empty {α : Type u_1} : empty.childTrees = PossiblyInfiniteList.empty

The childTrees of the empty tree are exactly PossiblyInfiniteList.empty.

Node Constructor

Similar to the InfiniteTreeSkeleton, we can also define a node constructor on the PossiblyInfiniteTree.

def PossiblyInfiniteTree.node {α : Type u_1} (root : α) (childTrees : PossiblyInfiniteList (PossiblyInfiniteTreeWithRoot α)) : PossiblyInfiniteTree α

Construct a PossiblyInfiniteTree from a PossiblyInfiniteList of PossiblyInfiniteTreeWithRoot and a new root element.

Equations

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

theorem PossiblyInfiniteTree.get?_node_nil {α : Type u_1} {root : α} {childTrees : PossiblyInfiniteList (PossiblyInfiniteTreeWithRoot α)} : (node root childTrees).get? [] = some root

Getting the element at address [] on node is the new root.

theorem PossiblyInfiniteTree.get?_node_cons {α : Type u_1} {root : α} {childTrees : PossiblyInfiniteList (PossiblyInfiniteTreeWithRoot α)} (n : Nat) (ns : List Nat) : (node root childTrees).get? (n :: ns) = (PossiblyInfiniteTreeWithRoot.opt_to_tree (childTrees.get? n)).get? ns

Getting any address != [] on node yields the respective element from the previous PossiblyInfiniteTreeWithRoot.

theorem PossiblyInfiniteTree.drop_node_cons {α : Type u_1} {root : α} {childTrees : PossiblyInfiniteList (PossiblyInfiniteTreeWithRoot α)} {n : Nat} {ns : List Nat} : (node root childTrees).drop (n :: ns) = (PossiblyInfiniteTreeWithRoot.opt_to_tree (childTrees.get? n)).drop ns

Dropping from node with an address of the form n::ns is the same as getting the n child from the child trees used in the construction and then dropping ns there.

theorem PossiblyInfiniteTree.root_node {α : Type u_1} {root : α} {childTrees : PossiblyInfiniteList (PossiblyInfiniteTreeWithRoot α)} : (node root childTrees).root = some root

The root of node is the root used in the construction.

theorem PossiblyInfiniteTree.childTrees_node {α : Type u_1} {root : α} {childTrees : PossiblyInfiniteList (PossiblyInfiniteTreeWithRoot α)} : (node root childTrees).childTrees = childTrees

The childTrees of node are the childTrees used in the construction.

theorem PossiblyInfiniteTree.node_root_childTrees {α : Type u_1} {t : PossiblyInfiniteTree α} {root : α} (h : t.root = some root) : t = node root t.childTrees

Any PossiblyInfiniteTree where the root is not none can be written using the node constructor.

ChildNodes

It can be convenient to obtain a list of the immediate child nodes of a given tree. This is equivalent to mapping each child tree to its root.

def PossiblyInfiniteTree.childNodes {α : Type u_1} (t : PossiblyInfiniteTree α) : PossiblyInfiniteList α

The childNodes are InfiniteTreeSkeleton.childNodes.

Equations

• t.childNodes = { infinite_list := t.infinite_tree.childNodes, no_holes := ⋯ }

theorem PossiblyInfiniteTree.get?_childNodes {α : Type u_1} {t : PossiblyInfiniteTree α} {n : Nat} : t.childNodes.get? n = (PossiblyInfiniteTreeWithRoot.opt_to_tree (t.childTrees.get? n)).root

Getting the nth childNodes is the root of the nth childTrees.

theorem PossiblyInfiniteTree.childNodes_eq {α : Type u_1} {t : PossiblyInfiniteTree α} : t.childNodes = t.childTrees.map fun (t : PossiblyInfiniteTreeWithRoot α) => t.val.root.get ⋯

The childNodes are the roots of the childTrees.

theorem PossiblyInfiniteTree.mem_of_mem_childNodes {α : Type u_1} {t : PossiblyInfiniteTree α} (c : α) : c ∈ t.childNodes → c ∈ t

Each child node is a tree member.

theorem PossiblyInfiniteTree.childNodes_empty {α : Type u_1} : empty.childNodes = PossiblyInfiniteList.empty

The childNodes of the empty tree are PossiblyInfiniteList.empty.

Suffixes

Here, we define a suffix relation on PossiblyInfiniteTree inspired by List.IsSuffix. For t1 and t2, t1 <:+ t2 denotes that t1 is a subtree of t2.

The suffix relation is reflexive and transitive but not necesarrily antisymmetric! Note also that InfiniteList.suffix_or_suffix_of_suffix has no equivalent statement here, i.e. just because two trees are subtrees of the same parent tree, we cannot say anything about their relation to one another. They might be totally "disconnected".

def PossiblyInfiniteTree.IsSuffix {α : Type u_1} (t1 t2 : PossiblyInfiniteTree α) : Prop

A suffix relation on infinite trees. This is inspired by List.IsSuffix. Read t1 <:+ t2 as: t1 is a subtree of t2.

Equations

• (t1 <:+ t2) = (t1.infinite_tree <:+ t2.infinite_tree)

def PossiblyInfiniteTree.«term_<:+_» : Lean.TrailingParserDescr

Equations

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

theorem PossiblyInfiniteTree.IsSuffix_iff {α : Type u_1} {t1 t2 : PossiblyInfiniteTree α} : t1 <:+ t2 ↔ ∃ (ns : List Nat), t2.drop ns = t1

t1 is a subtree of t2 if t1 can be obtained from t2 by dropping.

theorem PossiblyInfiniteTree.IsSuffix_refl {α : Type u_1} {t : PossiblyInfiniteTree α} : t <:+ t

The suffix relation is reflexive.

theorem PossiblyInfiniteTree.IsSuffix_trans {α : Type u_1} {t1 t2 t3 : PossiblyInfiniteTree α} : t1 <:+ t2 → t2 <:+ t3 → t1 <:+ t3

The suffix relation is transitive.

theorem PossiblyInfiniteTree.mem_of_mem_suffix {α : Type u_1} {t1 t2 : PossiblyInfiniteTree α} (suffix : t1 <:+ t2) (e : α) : e ∈ t1 → e ∈ t2

A member of a subtree is also a member of the current tree.

theorem PossiblyInfiniteTree.IsSuffix_drop {α : Type u_1} {t : PossiblyInfiniteTree α} (ns : List Nat) : t.drop ns <:+ t

Dropping elements yields a subtree.

theorem PossiblyInfiniteTree.IsSuffix_of_mem_childTrees {α : Type u_1} {t : PossiblyInfiniteTree α} (c : PossiblyInfiniteTreeWithRoot α) : c ∈ t.childTrees → c.val <:+ t

Each child tree is a subtree.

theorem PossiblyInfiniteTree.empty_suffix_of_empty {α : Type u_1} {t : PossiblyInfiniteTree α} : t <:+ empty → t = empty

Every suffix of the empty tree is empty.

theorem PossiblyInfiniteTree.no_orphans' {α : Type u_1} {t : PossiblyInfiniteTree α} (subtree : PossiblyInfiniteTree α) : subtree <:+ t → subtree.root = none → subtree.childNodes = PossiblyInfiniteList.empty

We can express the InfiniteTreeSkeleton.no_orphans condition directly on PossiblyInfiniteTree.

Recursor for Members

We define a recursion (induction) principle for members (Elements) of an PossiblyInfiniteTree called mem_rec. This can be used with the induction tactic to prove a property for each Element of an PossiblyInfiniteTree. Note that for using this coveniently, the goal needs to expressed (rewritten) using an Element.

def PossiblyInfiniteTree.Element {α : Type u_1} (t : PossiblyInfiniteTree α) : Type u_1

A tree Element is a Subtype featuring a proof of being a tree member.

Equations

• t.Element = { e : α // e ∈ t }

theorem PossiblyInfiniteTree.mem_rec {α : Type u_1} {t : PossiblyInfiniteTree α} {motive : t.Element → Prop} (root : ∀ (r : α) (mem : r ∈ t.root), motive ⟨r, ⋯⟩) (step : ∀ (t2 : PossiblyInfiniteTree α) (suffix : t2 <:+ t), (∃ (r : α), ∃ (mem : r ∈ t2.root), motive ⟨r, ⋯⟩) → ∀ {c : α} (mem : c ∈ t2.childNodes), motive ⟨c, ⋯⟩) (a : t.Element) : motive a

A recursor for proving properties about tree members (Elements) via induction.

Branches

Branches are essentially PossiblyInfiniteLists in a PossiblyInfiniteTree and can be characterizes by an infinite "address", i.e. InfiniteList Nat.

def PossiblyInfiniteTree.branchForAddress {α : Type u_1} (t : PossiblyInfiniteTree α) (ns : InfiniteList Nat) : PossiblyInfiniteList α

This function defines the PossiblyInfiniteList of tree elements that corresponds to a given infinite address.

Equations

• t.branchForAddress ns = { infinite_list := t.infinite_tree.branchForAddress ns, no_holes := ⋯ }

def PossiblyInfiniteTree.branchAddressIsMaximal {α : Type u_1} (t : PossiblyInfiniteTree α) (ns : InfiniteList Nat) : Prop

An infinite address is maximal in a PossiblyInfiniteTree if whenever the the tree element is none at the nth step of the address, then all of its siblings are also none (and it is enough to demand that the first sibling is none).

Equations

• t.branchAddressIsMaximal ns = ∀ (n : Nat), (t.branchForAddress ns).get? n.succ = none → (t.drop (ns.take n)).childNodes.head = none

def PossiblyInfiniteTree.branches {α : Type u_1} (t : PossiblyInfiniteTree α) : Set (PossiblyInfiniteList α)

The branches in the PossiblyInfiniteTree are exactly the PossiblyInfiniteLists for which an infinite address exists that is also maximal.

Equations

• t.branches b = ∃ (ns : InfiniteList Nat), b = t.branchForAddress ns ∧ t.branchAddressIsMaximal ns

theorem PossiblyInfiniteTree.get?_branchForAddress {α : Type u_1} {t : PossiblyInfiniteTree α} {ns : InfiniteList Nat} {n : Nat} : (t.branchForAddress ns).get? n = t.get? (ns.take n)

Getting from the branch corresponding to an infinite address corresponds to getting from the tree at the corresponding finite part of the address.

theorem PossiblyInfiniteTree.branches_eq {α : Type u_1} {t : PossiblyInfiniteTree α} : t.branches = fun (b : PossiblyInfiniteList α) => b.head = t.root ∧ (t.childTrees = PossiblyInfiniteList.empty ∧ b.tail = PossiblyInfiniteList.empty ∨ ∃ (c : PossiblyInfiniteTreeWithRoot α), c ∈ t.childTrees ∧ b.tail ∈ c.val.branches)

The set of branches can equivalently be expressed as the set of all PossiblyInfiniteLists where the head equals the root of the tree and the tail occurs in the branches of some childTree. If there are no childTrees, then the tail needs to be empty.

Branch Generation

We can use PossiblyInfiniteList.generate to construct branches in a PossiblyInfiniteTree. First of all, this requires that the mapper function produces a PossiblyInfiniteTreeWithRoot. By that PossiblyInfiniteList.generate gives us an PossiblyInfiniteList of PossiblyInfiniteTreeWithRoot. Intuitively, using all the roots of these trees gives us a branch. But this is only true if the generate trees are always child trees of each other and the generation indeed creates a maximal branch according to branchAddressIsMaximal. This condition is used in the generate_branch_mem_branches theorem to proof that a PossiblyInfiniteList from the generate_branch function is indeed in branches.

def PossiblyInfiniteTree.generate_branch {β : Type u_1} {α : Type u_2} (start : Option β) (generator : β → Option β) (mapper : β → PossiblyInfiniteTreeWithRoot α) : PossiblyInfiniteList α

Given a generator and a mapper that maps generated elements to PossiblyInfiniteTreeWithRoot, construct an PossiblyInfiniteList with the goal of constructing a branch in a tree.

Equations

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

theorem PossiblyInfiniteTree.generate_branch_mem_branches {β : Type u_1} {α : Type u_2} {start : Option β} {generator : β → Option β} {mapper : β → PossiblyInfiniteTreeWithRoot α} (next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).val.childTrees) (maximal : ∀ (b : β), generator b = none → (mapper b).val.childTrees = PossiblyInfiniteList.empty) (isSome_start : start.isSome = true) : generate_branch start generator mapper ∈ (mapper (start.get isSome_start)).val.branches

If the generated trees are childTrees of each other and the generated branch is maximal according to branchAddressIsMaximal, then the generated PossiblyInfiniteList is indeed a branch.

theorem PossiblyInfiniteTree.head_generate_branch {β : Type u_1} {α : Type u_2} {start : Option β} {generator : β → Option β} {mapper : β → PossiblyInfiniteTreeWithRoot α} : (generate_branch start generator mapper).head = Option.map (fun (s : β) => (mapper s).val.root.get ⋯) start

The PossiblyInfiniteList.head of generate_branch is the root of the first tree.

theorem PossiblyInfiniteTree.get?_generate_branch {β : Type u_1} {α : Type u_2} {start : Option β} {generator : β → Option β} {mapper : β → PossiblyInfiniteTreeWithRoot α} (n : Nat) : (generate_branch start generator mapper).get? n = Option.map (fun (t : PossiblyInfiniteTreeWithRoot α) => t.val.root.get ⋯) ((PossiblyInfiniteList.generate start generator mapper).get? n)

Getting the nth element from a generate_branch result is the root of the nth generated tree.

theorem PossiblyInfiniteTree.tail_generate_branch {β : Type u_1} {α : Type u_2} {start : Option β} {generator : β → Option β} {mapper : β → PossiblyInfiniteTreeWithRoot α} : (generate_branch start generator mapper).tail = generate_branch (start.bind generator) generator mapper

The PossiblyInfiniteList.tail of generate_branch is the branch generated when applying the generator function once on the starting element before the actual generation.

Leaves

The leaves of a PossiblyInfiniteTree is the set of elements that occur in a node that has no childNodes.

def PossiblyInfiniteTree.leaves {α : Type u_1} (t : PossiblyInfiniteTree α) : Set α

Equations

• t.leaves a = ∃ (node : List Nat), t.get? node = some a ∧ (t.drop node).childNodes.head = none

Constructing a Tree from a Branch

A PossiblyInfiniteList directly corresponds to the PossiblyInfiniteTree where the list is the "first" branch (with the address that only consists of zeros) and all other nodes are none.

def PossiblyInfiniteTree.from_branch {α : Type u_1} (b : PossiblyInfiniteList α) : PossiblyInfiniteTree α

Equations

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