InfiniteTreeSkeleton

This file defines an InfiniteTreeSkeleton as a function from the a list of naturals into the desired type. Note that this is very similar to an InfiniteList only replacing Nat for List Nat. In this way, the InfiniteTreeSkeleton is infinite in both dimensions, i.e. it has infinite depth and each node has infinitely many (direct) children.

Similar to InfiniteList, we offer many convenience functions, some of which have different names. For example, the equivalent to InfiniteList.head would be root and the equivalent to InfiniteList.tail would be childTrees. The functions get and drop behave analogously to their InfiniteList counterparts.

As for the InfiniteList, we also implement a mem_rec recursor that allows showing properties of tree members via induction. We also allow generating branches of a tree using the generate_branch function, which yields an InfiniteList. The convenience of this function lies in the theorem generate_branch_mem_branches that immediately allows us to verify that the generated InfiniteList is indeed a branch in the InfiniteTreeSkeleton.

def InfiniteTreeSkeleton (α : Type u) : Type u

An InfiniteTreeSkeleton is a function from a list of naturals (representing an address in the tree) into the desired type.

Equations

• InfiniteTreeSkeleton α = (List Nat → α)

Basics

The essential functions on infinite trees, mainly get, drop, root, and childTrees.

def InfiniteTreeSkeleton.get {α : Type u_1} (t : InfiniteTreeSkeleton α) (ns : List Nat) : α

Obtains the element of the tree at the given address.

Equations

• t.get ns = t ns

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

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

Equations

• t.drop ns ns' = t.get (ns ++ ns')

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

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

Equations

• t.root = t.get []

def InfiniteTreeSkeleton.childTrees {α : Type u_1} (t : InfiniteTreeSkeleton α) : InfiniteList (InfiniteTreeSkeleton α)

Get the InfiniteList of immediate child trees of the current tree.

Equations

• t.childTrees n ns = t.get (n :: ns)

def InfiniteTreeSkeleton.node {α : Type u_1} (root : α) (childTrees : InfiniteList (InfiniteTreeSkeleton α)) : InfiniteTreeSkeleton α

Construct an InfiniteTreeSkeleton from an InfiniteList of InfiniteTreeSkeletons and a new root element.

Equations

• InfiniteTreeSkeleton.node root childTrees [] = root
• InfiniteTreeSkeleton.node root childTrees (hd :: tl) = childTrees hd tl

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

Equations

• InfiniteTreeSkeleton.instMembership = { mem := fun (t : InfiniteTreeSkeleton α) (a : α) => ∃ (ns : List Nat), t.get ns = a }

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

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

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

theorem InfiniteTreeSkeleton.get_mem {α : Type u_1} {t : InfiniteTreeSkeleton α} {ns : List Nat} : t.get ns ∈ t

Each element we can get is in the tree.

theorem InfiniteTreeSkeleton.get_drop {α : Type u_1} {t : InfiniteTreeSkeleton α} {ns ns' : List Nat} : (t.drop ns).get ns' = t.get (ns ++ ns')

Get after drop can be rewritten into get.

theorem InfiniteTreeSkeleton.drop_eq {α : Type u_1} {t : InfiniteTreeSkeleton α} {ns : List Nat} : t.drop ns = fun (ns' : List Nat) => t.get (ns ++ ns')

Helper theorem stating the definition of drop.

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

Dropping the empty address changes nothing.

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

Two calls to drop can be combined.

theorem InfiniteTreeSkeleton.root_mem {α : Type u_1} {t : InfiniteTreeSkeleton α} : t.root ∈ t

The root is in the tree.

theorem InfiniteTreeSkeleton.root_drop {α : Type u_1} {t : InfiniteTreeSkeleton α} {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.

theorem InfiniteTreeSkeleton.get_childTrees {α : Type u_1} {t : InfiniteTreeSkeleton α} (n : Nat) : t.childTrees.get n = t.drop [n]

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

theorem InfiniteTreeSkeleton.get_get_childTrees {α : Type u_1} {t : InfiniteTreeSkeleton α} (n : Nat) (ns : List Nat) : (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 InfiniteTreeSkeleton.get_node_nil {α : Type u_1} {root : α} {childTrees : InfiniteList (InfiniteTreeSkeleton α)} : (node root childTrees).get [] = root

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

theorem InfiniteTreeSkeleton.get_node_cons {α : Type u_1} {root : α} {childTrees : InfiniteList (InfiniteTreeSkeleton α)} (n : Nat) (ns : List Nat) : (node root childTrees).get (n :: ns) = (childTrees.get n).get ns

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

theorem InfiniteTreeSkeleton.drop_node_cons {α : Type u_1} {root : α} {childTrees : InfiniteList (InfiniteTreeSkeleton α)} {n : Nat} {ns : List Nat} : (node root childTrees).drop (n :: ns) = (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 InfiniteTreeSkeleton.root_node {α : Type u_1} {root : α} {childTrees : InfiniteList (InfiniteTreeSkeleton α)} : (node root childTrees).root = root

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

theorem InfiniteTreeSkeleton.childTrees_node {α : Type u_1} {root : α} {childTrees : InfiniteList (InfiniteTreeSkeleton α)} : (node root childTrees).childTrees = childTrees

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

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

Any InfiniteTreeSkeleton 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 and actually just defined via mapping each child tree to its root.

def InfiniteTreeSkeleton.childNodes {α : Type u_1} (t : InfiniteTreeSkeleton α) : InfiniteList α

The childNodes are the roots of the childTrees.

Equations

• t.childNodes = t.childTrees.map InfiniteTreeSkeleton.root

theorem InfiniteTreeSkeleton.get_childNodes {α : Type u_1} {t : InfiniteTreeSkeleton α} {n : Nat} : t.childNodes.get n = t.get [n]

When getting the nth child node, we can instead get the tree element at the singleton address [n].

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

Each child node is a tree member.

Suffixes

Here, we define a suffix relation on InfiniteTreeSkeleton 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 InfiniteTreeSkeleton.IsSuffix {α : Type u_1} (t1 t2 : InfiniteTreeSkeleton α) : 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) = ∃ (ns : List Nat), t2.drop ns = t1

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

Equations

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

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

The suffix relation is reflexive.

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

The suffix relation is transitive.

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

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

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

Dropping elements yields a subtree.

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

Each child tree is a subtree.

Recursor for Members

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

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

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

Equations

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

theorem InfiniteTreeSkeleton.mem_rec {α : Type u_1} {t : InfiniteTreeSkeleton α} {motive : t.Element → Prop} (root : motive ⟨t.root, ⋯⟩) (step : ∀ (t2 : InfiniteTreeSkeleton α) (suffix : t2 <:+ t), motive ⟨t2.root, ⋯⟩ → ∀ {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 InfiniteLists in an InfiniteTreeSkeleton and can be characterizes by an infinite "address", i.e. InfiniteList Nat.

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

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

Equations

• t.branchForAddress ns n = t.get (ns.take n)

def InfiniteTreeSkeleton.branches {α : Type u_1} (t : InfiniteTreeSkeleton α) : Set (InfiniteList α)

The branches in the InfiniteTreeSkeleton are exactly the InfiniteLists for which an infinite address exists.

Equations

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

theorem InfiniteTreeSkeleton.get_branchForAddress {α : Type u_1} {t : InfiniteTreeSkeleton α} {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. This essentially unfold the definition of branchForAddress.

theorem InfiniteTreeSkeleton.head_branchForAddress {α : Type u_1} {t : InfiniteTreeSkeleton α} {ns : InfiniteList Nat} : (t.branchForAddress ns).head = t.root

The InfiniteList.head of branchForAddress is the tree's root.

theorem InfiniteTreeSkeleton.tail_branchForAddress {α : Type u_1} {t : InfiniteTreeSkeleton α} {ns : InfiniteList Nat} : (t.branchForAddress ns).tail = (t.childTrees.get ns.head).branchForAddress ns.tail

The InfiniteList.tail of branchForAddress corresponds to a branch in a child tree.

theorem InfiniteTreeSkeleton.branchForAddress_cons {α : Type u_1} {t : InfiniteTreeSkeleton α} {n : Nat} {ns : InfiniteList Nat} : t.branchForAddress (InfiniteList.cons n ns) = InfiniteList.cons t.root ((t.childTrees.get n).branchForAddress ns)

The branchForAddress for an InfiniteList.cons address can be decomposed accordingly.

theorem InfiniteTreeSkeleton.branches_node {α : Type u_1} {root : α} {childTrees : InfiniteList (InfiniteTreeSkeleton α)} : (node root childTrees).branches = fun (b : InfiniteList α) => b.head = root ∧ ∃ (n : Nat), b.tail ∈ (childTrees.get n).branches

The branches of a tree constructed through node are exactly the ones who's head is the root from the construction and who's tail occurs in the branches of one of the child trees.

Branch Generation

We can use InfiniteList.generate to construct branches in a InfiniteTreeSkeleton. First of all, this requires that the mapper function produces an InfiniteTreeSkeleton. By that InfiniteList.generate gives us an InfiniteList of InfiniteTreeSkeletons. 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. This condition is used in the generate_branch_mem_branches theorem to proof that an InfiniteList from the generate_branch function is indeed in branches.

def InfiniteTreeSkeleton.generate_branch {β : Type u_1} {α : Type u_2} (start : β) (generator : β → β) (mapper : β → InfiniteTreeSkeleton α) : InfiniteList α

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

Equations

• InfiniteTreeSkeleton.generate_branch start generator mapper = (InfiniteList.generate start generator mapper).map InfiniteTreeSkeleton.root

theorem InfiniteTreeSkeleton.generate_branch_mem_branches {β : Type u_1} {α : Type u_2} {start : β} {generator : β → β} {mapper : β → InfiniteTreeSkeleton α} (next_is_child : ∀ (b : β), mapper (generator b) ∈ (mapper b).childTrees) : generate_branch start generator mapper ∈ (mapper start).branches

If the generated trees are childTrees of each other, then the generated InfiniteList is indeed a branch.

theorem InfiniteTreeSkeleton.head_generate_branch {β : Type u_1} {α : Type u_2} {start : β} {generator : β → β} {mapper : β → InfiniteTreeSkeleton α} : (generate_branch start generator mapper).head = (mapper start).root

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

theorem InfiniteTreeSkeleton.get_generate_branch {β : Type u_1} {α : Type u_2} {start : β} {generator : β → β} {mapper : β → InfiniteTreeSkeleton α} (n : Nat) : (generate_branch start generator mapper).get n = ((InfiniteList.generate start generator mapper).get n).root

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

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

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