Euler tour tree

25 fully proved

Euler Tour Tree

InductiveRooted ordered tree#✓fully proved

A rooted ordered tree with vertices in a type \(V\) consists of a root vertex in \(V\) together with an ordered list of child subtrees, each a rooted ordered tree with vertices in \(V\).

Vertex labels need not be distinct.

inductive Tree (V : Type u) where
  | node (root : V) (children : List (Tree V)) : Tree V
deriving Repr

Used by 103

Used byArc sequence of the Euler tour · Arc sequence as the zipped Euler tour · Children of a rooted tree · Induction principle for rooted trees · Cutting the last child subtree · Linking two rooted trees · The Euler tour visits exactly the vertices of the tree · Linking two copies of a single vertex is not valid · Root of a rooted tree · Size of a rooted tree · Euler tour · Euler tour with an accumulator · Accumulator lemma for the Euler tour · Euler tour of a linked tree · Recursive formula for the Euler tour · Valid Euler-tour tree · Valid trees have distinct vertices · Linking valid trees with disjoint vertices gives a valid tree · A single-vertex tree is valid · Preorder vertex list of a rooted tree · Accumulator preorder traversal · Accumulator preorder traversal is append · Preorder vertex list of a node · Access in a link-cut tree · Access preserves validity · Access leaves the represented forest unchanged · After access, the accessed vertex ends its preferred path · Adjacency in a rooted tree · Parent-child edges are edges · Adjacency test · An edge cut keeps every other edge · Edges after grafting · Pruning keeps surviving edges · Rerooting keeps every edge · Connectivity in a link-cut tree state · Connectivity via Euler tours · Linking connects the endpoints · Making a vertex the root keeps its connections · Cutting off the subtree at a vertex · Cutting preserves validity · Cutting an edge of a link-cut tree · Edge cutting preserves validity · Edge cut on an adjacent pair · Edge cut on a non-adjacent pair · Preferred-path decomposition of a tree · Access edges make the root path the downward preferred path · The downward preferred path starts at the root · Decomposition paths are paths of the tree · Preferred paths permute the vertex list · Subtree rooted at a vertex · Tree of a forest containing a vertex · A root path ends at its target · Grafting a tree below a vertex · The root path starts at the root · Consecutive vertices of a root path are adjacent · Preferred paths of a link-cut tree state follow represented edges · Preferred paths of a tree follow tree edges · A root path follows parent-child edges downward · Linking two trees of a link-cut tree state · Linking in a link-cut tree preserves validity · Making a vertex the root in a link-cut tree state · Rerooting a link-cut tree state preserves validity · Making a vertex the root installs a tree rooted there · Vertex of a link-cut tree state · Both sides of a cut remain in the forest · The first endpoint of a tree edge is a vertex · The parent endpoint of a tree edge is a vertex · Preferred paths cover exactly the vertices of the forest · Access keeps off-path preferred edges · Access makes the root path preferred · The second endpoint of a tree edge is a vertex · The child endpoint of a tree edge is a vertex · Root paths stay inside the tree · Vertices after grafting · Vertices of a pruned tree · Pruning keeps the vertices outside the detached subtree · Rerooting preserves the vertex set · Preferred paths cover each vertex at most once · Root paths have distinct vertices · A cut disconnects a vertex from everything outside its subtree · Cutting an edge separates its endpoints · Forest from a vertex list · Parent-child relation in a rooted tree · Preferred-path decomposition of a link-cut tree state · Removing the tree containing a vertex splits the forest's vertices · The preferred paths of a tree rearrange its vertex list · Grafting adds the new subtree's vertices · Pruning a subtree splits the vertex list · Rerooting preserves the vertices · Pruning the subtrees rooted at a vertex · Pruning at an absent vertex changes nothing · Removing the trees that contain a vertex · Rerooting a tree at a vertex · Rerooting fails at an absent vertex · Grafting keeps the root · Root-to-vertex path · Pruning keeps the root · Path tree on a vertex list · Link-cut tree state · Adjacency in a tree is symmetric · Preferred paths of a tree · Valid link-cut tree states · Validity of states with no preferred edges

Tree

TheoremInduction principle for rooted trees#✓fully proved

Let \(P\) be a property of trees. Suppose that for every vertex \(r\) and all trees \(c_1, \dots, c_k\) (with \(k \ge 0\)), if \(P\) holds for each \(c_i\), then \(P\) holds for the tree with root \(r\) and child subtrees \(c_1, \dots, c_k\). Then \(P\) holds for every tree.

theorem children_ind {motive : Tree V → Prop}
    (node : ∀ (r : V) (cs : List (Tree V)), (∀ c ∈ cs, motive c) →
      motive (.node r cs))
    (t : Tree V) : motive t

Uses 1 · Used by 37

Statement usesRooted ordered tree

Used byThe Euler tour visits exactly the vertices of the tree · Accumulator lemma for the Euler tour · Accumulator preorder traversal is append · After access, the accessed vertex ends its preferred path · Parent-child edges are edges · An edge cut keeps every other edge · Edges after grafting · Pruning keeps surviving edges · Rerooting keeps every edge · Linking connects the endpoints · Making a vertex the root keeps its connections · Edge cut on an adjacent pair · Edge cut on a non-adjacent pair · Access edges make the root path the downward preferred path · Decomposition paths are paths of the tree · Preferred paths permute the vertex list · A root path ends at its target · Consecutive vertices of a root path are adjacent · A root path follows parent-child edges downward · Making a vertex the root installs a tree rooted there · Both sides of a cut remain in the forest · The first endpoint of a tree edge is a vertex · Root paths stay inside the tree · Vertices after grafting · Vertices of a pruned tree · Pruning keeps the vertices outside the detached subtree · Rerooting preserves the vertex set · Root paths have distinct vertices · A cut disconnects a vertex from everything outside its subtree · Cutting an edge separates its endpoints · Grafting adds the new subtree's vertices · Pruning a subtree splits the vertex list · Rerooting preserves the vertices · Pruning at an absent vertex changes nothing · Rerooting fails at an absent vertex · Grafting keeps the root · Adjacency in a tree is symmetric

DefinitionRoot of a rooted tree#✓fully proved

The root of the tree with root vertex \(r\) and child subtrees \(c_1, \dots, c_k\) is the vertex \(r\).

def root : Tree V → V
  | .node r _ => r

Uses 1 · Used by 35

Statement usesRooted ordered tree

Used byEuler tour of a linked tree · Adjacency in a rooted tree · Parent-child edges are edges · Adjacency test · An edge cut keeps every other edge · Edges after grafting · Pruning keeps surviving edges · Rerooting keeps every edge · Linking connects the endpoints · Making a vertex the root keeps its connections · Edge cut on an adjacent pair · Edge cut on a non-adjacent pair · Preferred-path decomposition of a tree · Access edges make the root path the downward preferred path · The downward preferred path starts at the root · Decomposition paths are paths of the tree · Preferred paths permute the vertex list · The root path starts at the root · Consecutive vertices of a root path are adjacent · A root path follows parent-child edges downward · Making a vertex the root installs a tree rooted there · Both sides of a cut remain in the forest · The first endpoint of a tree edge is a vertex · Pruning keeps the vertices outside the detached subtree · Rerooting preserves the vertex set · A cut disconnects a vertex from everything outside its subtree · Cutting an edge separates its endpoints · Parent-child relation in a rooted tree · Pruning a subtree splits the vertex list · Rerooting preserves the vertices · Rerooting a tree at a vertex · Rerooting fails at an absent vertex · Grafting keeps the root · Pruning keeps the root · Adjacency in a tree is symmetric

DefinitionChildren of a rooted tree#✓fully proved

The children of a tree are the child subtrees of its root, as a list in their given order.

def children : Tree V → List (Tree V)
  | .node _ cs => cs

Uses 1

Statement usesRooted ordered tree

DefinitionSize of a rooted tree#✓fully proved

The size of a tree is its number of nodes, counting repeated vertex labels with multiplicity: the tree with root \(r\) and child subtrees \(c_1, \dots, c_k\) has size \(1 + \sum_{i=1}^{k} \operatorname{size}(c_i)\).

def size : Tree V → Nat
  | .node _ cs => 1 + (cs.map size).sum

Uses 1

Statement usesRooted ordered tree

DefinitionAccumulator preorder traversal#✓fully proved

For a rooted ordered tree \(t\) with root \(r\) and child subtrees \(c_1, \dots, c_k\) (in order) and a list \(a\), the accumulator traversal \(T(t, a)\) is the list whose first entry is \(r\) and whose remaining entries are \(T(c_1, T(c_2, \dots, T(c_k, a) \dots))\); when \(k = 0\) the remaining entries are \(a\).

The list \(T(t, a)\) equals the preorder vertex list of \(t\) followed by \(a\), so the preorder list is computed in linear time rather than by repeatedly appending child lists.

def verticesAux : Tree V → List V → List V
  | .node r cs, acc => r :: cs.foldr (fun c acc => verticesAux c acc) acc

Uses 1 · Used by 3

Statement usesRooted ordered tree

Used byPreorder vertex list of a rooted tree · Accumulator preorder traversal is append · Preorder vertex list of a node

DefinitionPreorder vertex list of a rooted tree#✓fully proved

The preorder vertex list of a rooted ordered tree \(t\) is the accumulator preorder traversal of \(t\) started from the empty list.

Equivalently, it is the root of \(t\) followed by the preorder vertex lists of its child subtrees in order; repeated vertex labels appear with multiplicity.

def vertices (t : Tree V) : List V :=
  verticesAux t []

Uses 2 · Used by 52

Statement usesRooted ordered tree · Accumulator preorder traversal

Used byThe Euler tour visits exactly the vertices of the tree · Linking two copies of a single vertex is not valid · Valid Euler-tour tree · Valid trees have distinct vertices · Linking valid trees with disjoint vertices gives a valid tree · A single-vertex tree is valid · Accumulator preorder traversal is append · Preorder vertex list of a node · Access preserves validity · After access, the accessed vertex ends its preferred path · An edge cut keeps every other edge · Pruning keeps surviving edges · Rerooting keeps every edge · Connectivity in a link-cut tree state · Connectivity via Euler tours · Linking connects the endpoints · Making a vertex the root keeps its connections · Cutting preserves validity · Edge cutting preserves validity · Access edges make the root path the downward preferred path · Preferred paths permute the vertex list · Tree of a forest containing a vertex · Linking two trees of a link-cut tree state · Linking in a link-cut tree preserves validity · Rerooting a link-cut tree state preserves validity · Making a vertex the root installs a tree rooted there · Vertex of a link-cut tree state · Both sides of a cut remain in the forest · The first endpoint of a tree edge is a vertex · The parent endpoint of a tree edge is a vertex · Preferred paths cover exactly the vertices of the forest · The second endpoint of a tree edge is a vertex · The child endpoint of a tree edge is a vertex · Root paths stay inside the tree · Vertices after grafting · Vertices of a pruned tree · Pruning keeps the vertices outside the detached subtree · Rerooting preserves the vertex set · Preferred paths cover each vertex at most once · Root paths have distinct vertices · A cut disconnects a vertex from everything outside its subtree · Cutting an edge separates its endpoints · Removing the tree containing a vertex splits the forest's vertices · The preferred paths of a tree rearrange its vertex list · Grafting adds the new subtree's vertices · Pruning a subtree splits the vertex list · Rerooting preserves the vertices · Pruning at an absent vertex changes nothing · Removing the trees that contain a vertex · Rerooting fails at an absent vertex · Valid link-cut tree states · Validity of states with no preferred edges

TheoremAccumulator preorder traversal is append#✓fully proved

For every rooted ordered tree \(t\) and every list \(a\), the accumulator preorder traversal of \(t\) started from \(a\) equals the preorder vertex list of \(t\) followed by \(a\).

theorem verticesAux_eq (t : Tree V) (acc : List V) :
    verticesAux t acc = vertices t ++ acc

Uses 4 · Used by 1

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Accumulator preorder traversal

Proof usesInduction principle for rooted trees

Used byPreorder vertex list of a node

TheoremPreorder vertex list of a node#✓fully proved

For a vertex \(r\) and rooted ordered trees \(c_1, \dots, c_k\), the preorder vertex list of the tree with root \(r\) and child subtrees \(c_1, \dots, c_k\) (in order) is \(r\) followed by the concatenation of the preorder vertex lists of \(c_1, \dots, c_k\), in this order.

theorem vertices_node (r : V) (cs : List (Tree V)) :
    vertices (.node r cs) = r :: cs.flatMap vertices

Uses 4 · Used by 28

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree

Proof usesAccumulator preorder traversal · Accumulator preorder traversal is append

Used byThe Euler tour visits exactly the vertices of the tree · Linking two copies of a single vertex is not valid · Linking valid trees with disjoint vertices gives a valid tree · A single-vertex tree is valid · After access, the accessed vertex ends its preferred path · An edge cut keeps every other edge · Pruning keeps surviving edges · Rerooting keeps every edge · Linking connects the endpoints · Making a vertex the root keeps its connections · Access edges make the root path the downward preferred path · Preferred paths permute the vertex list · Making a vertex the root installs a tree rooted there · Both sides of a cut remain in the forest · The first endpoint of a tree edge is a vertex · Root paths stay inside the tree · Vertices after grafting · Vertices of a pruned tree · Pruning keeps the vertices outside the detached subtree · Rerooting preserves the vertex set · Root paths have distinct vertices · A cut disconnects a vertex from everything outside its subtree · Cutting an edge separates its endpoints · Grafting adds the new subtree's vertices · Pruning a subtree splits the vertex list · Rerooting preserves the vertices · Pruning at an absent vertex changes nothing · Rerooting fails at an absent vertex

DefinitionEuler tour with an accumulator#✓fully proved

Let \(t\) be a tree with root \(r\) and child subtrees \(c_1, \dots, c_k\) in order, and let \(a\) be a list of vertices. For a list \(L\) of vertices, write \(r \cdot L\) for the list \(L\) with \(r\) put in front. The Euler tour of \(t\) with accumulator \(a\), written \(T(t, a)\), is \(r \cdot L_1\), where \(L_{k+1} = a\) and \(L_i = T(c_i, r \cdot L_{i+1})\) for \(i = k, \dots, 1\).

It equals the Euler tour of \(t\) followed by \(a\), and computes the Euler tour without repeatedly concatenating the tours of the child subtrees.

def tourAux : Tree V → List V → List V
  | .node r cs, acc =>
      r :: cs.foldr (fun c acc => tourAux c (r :: acc)) acc

Uses 1 · Used by 3

Statement usesRooted ordered tree

Used byEuler tour · Accumulator lemma for the Euler tour · Recursive formula for the Euler tour

DefinitionEuler tour#✓fully proved

The Euler tour of a tree \(t\) with root \(r\) and child subtrees \(c_1, \dots, c_k\) in order is the list of vertices consisting of \(r\), followed, for each \(i = 1, \dots, k\) in turn, by the Euler tour of \(c_i\) and then \(r\). It is the vertex sequence of the depth-first walk that returns to the parent vertex after each child subtree.

def tour (t : Tree V) : List V :=
  tourAux t []

Uses 2 · Used by 7

Statement usesRooted ordered tree · Euler tour with an accumulator

Used byArc sequence of the Euler tour · Arc sequence as the zipped Euler tour · The Euler tour visits exactly the vertices of the tree · Accumulator lemma for the Euler tour · Euler tour of a linked tree · Recursive formula for the Euler tour · Connectivity via Euler tours

TheoremAccumulator lemma for the Euler tour#✓fully proved

For every tree \(t\) and every list \(a\) of vertices, the Euler tour of \(t\) with accumulator \(a\) equals the Euler tour of \(t\) followed by \(a\).

theorem tourAux_eq (t : Tree V) (acc : List V) :
    tourAux t acc = tour t ++ acc

Uses 4 · Used by 1

Statement usesRooted ordered tree · Euler tour · Euler tour with an accumulator

Proof usesInduction principle for rooted trees

Used byRecursive formula for the Euler tour

TheoremRecursive formula for the Euler tour#✓fully proved

For a vertex \(r\) and a list of trees \(c_1, \dots, c_k\), the Euler tour of the tree with root \(r\) and child subtrees \(c_1, \dots, c_k\) in order is \(r\), followed, for each \(i = 1, \dots, k\) in turn, by the Euler tour of \(c_i\) and then \(r\).

theorem tour_node (r : V) (cs : List (Tree V)) :
    tour (.node r cs) = r :: cs.flatMap (fun c => tour c ++ [r])

Uses 4 · Used by 2

Statement usesRooted ordered tree · Euler tour

Proof usesEuler tour with an accumulator · Accumulator lemma for the Euler tour

Used byThe Euler tour visits exactly the vertices of the tree · Euler tour of a linked tree

DefinitionArc sequence of the Euler tour#✓fully proved

The arc sequence of a tree \(t\) is the list of consecutive pairs of its Euler tour: if the Euler tour of \(t\) is \(v_0, v_1, \dots, v_k\), then the arc sequence of \(t\) is \((v_0, v_1), (v_1, v_2), \dots, (v_{k-1}, v_k)\).

Each tree edge occurs once in each direction.

def arcTour (t : Tree V) : List (V × V) :=
  let tourList := tour t
  tourList.zip tourList.tail

Uses 2 · Used by 1

Statement usesRooted ordered tree · Euler tour

Used byArc sequence as the zipped Euler tour

TheoremArc sequence as the zipped Euler tour#✓fully proved

For every tree \(t\), the arc sequence of \(t\) is the Euler tour of \(t\) zipped with its own tail: if the Euler tour of \(t\) is \(v_0, v_1, \dots, v_k\), then the arc sequence of \(t\) is \((v_0, v_1), (v_1, v_2), \dots, (v_{k-1}, v_k)\).

theorem arcTour_eq_zip (t : Tree V) :
    arcTour t = (tour t).zip (tour t).tail

Uses 3

Statement usesRooted ordered tree · Arc sequence of the Euler tour · Euler tour

TheoremThe Euler tour visits exactly the vertices of the tree#✓fully proved

For every tree \(t\) and every \(v\), \(v\) occurs in the Euler tour of \(t\) if and only if \(v\) is a vertex of \(t\).

theorem mem_tour_iff (t : Tree V) (v : V) : v ∈ tour t ↔ v ∈ vertices t

Uses 6 · Used by 1

Statement usesRooted ordered tree · Euler tour · Preorder vertex list of a rooted tree

Proof usesInduction principle for rooted trees · Recursive formula for the Euler tour · Preorder vertex list of a node

Used byConnectivity via Euler tours

DefinitionValid Euler-tour tree#✓fully proved

A rooted ordered tree is valid when its list of vertices in preorder has no duplicates, that is, every vertex label occurs at most once in the tree.

Raw trees may repeat vertex labels; reading the linking of two trees as a link in a dynamic forest requires valid trees with disjoint vertex sets.

def Valid (t : Tree V) : Prop :=
  (vertices t).Nodup

Uses 2 · Used by 4

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree

Used byLinking two copies of a single vertex is not valid · Valid trees have distinct vertices · Linking valid trees with disjoint vertices gives a valid tree · A single-vertex tree is valid

TheoremValid trees have distinct vertices#✓fully proved

A tree \(t\) is valid if and only if its list of vertices in preorder has no repeated entries.

theorem valid_iff (t : Tree V) : Valid t ↔ (vertices t).Nodup

Uses 3

Statement usesRooted ordered tree · Valid Euler-tour tree · Preorder vertex list of a rooted tree

TheoremA single-vertex tree is valid#✓fully proved

For every vertex \(r\), the tree with root \(r\) and no child subtrees is valid.

theorem valid_singleton (r : V) : Valid (.node r [])

Uses 4

Statement usesRooted ordered tree · Valid Euler-tour tree

Proof usesPreorder vertex list of a rooted tree · Preorder vertex list of a node

DefinitionLinking two rooted trees#✓fully proved

Let \(t_1\) be a tree with root \(r\) and child subtrees \(c_1, \dots, c_k\), and let \(t_2\) be a tree. The link of \(t_1\) and \(t_2\) is the tree with root \(r\) and child subtrees \(c_1, \dots, c_k, t_2\), so \(t_2\) becomes the new last child subtree of the root of \(t_1\).

def link : Tree V → Tree V → Tree V
  | .node r cs, t₂ => .node r (cs ++ [t₂])

Uses 1 · Used by 3

Statement usesRooted ordered tree

Used byLinking two copies of a single vertex is not valid · Euler tour of a linked tree · Linking valid trees with disjoint vertices gives a valid tree

TheoremLinking valid trees with disjoint vertices gives a valid tree#✓fully proved

Let \(t_1\) and \(t_2\) be valid trees such that no vertex of \(t_1\) is a vertex of \(t_2\). Then the link of \(t_1\) and \(t_2\), that is, \(t_1\) with \(t_2\) added as the last child subtree of its root, is valid.

This is the forest precondition for reading the link as a link of two trees in a dynamic forest.

theorem valid_link {t₁ t₂ : Tree V} (h₁ : Valid t₁) (h₂ : Valid t₂)
    (hd : List.Disjoint (vertices t₁) (vertices t₂)) :
    Valid (link t₁ t₂)

Uses 5

Statement usesRooted ordered tree · Valid Euler-tour tree · Linking two rooted trees · Preorder vertex list of a rooted tree

Proof usesPreorder vertex list of a node

TheoremLinking two copies of a single vertex is not valid#✓fully proved

For every vertex \(r\), the link of the single-vertex tree with root \(r\) and another single-vertex tree with root \(r\) is not valid, since the vertex \(r\) occurs twice in it. Hence the link of two valid trees need not be valid when their vertex sets are not disjoint.

theorem not_valid_link_same_root (r : V) :
    ¬ Valid (link (.node r []) (.node r []))

Uses 5

Statement usesRooted ordered tree · Valid Euler-tour tree · Linking two rooted trees

Proof usesPreorder vertex list of a rooted tree · Preorder vertex list of a node

DefinitionSplicing two Euler tours#✓fully proved

For lists \(\tau_1\) and \(\tau_2\) of vertices and a vertex \(r\), the splice of \(\tau_1\) and \(\tau_2\) at \(r\) is the list consisting of the entries of \(\tau_1\), followed by the entries of \(\tau_2\), followed by \(r\).

It is used with \(\tau_1\) and \(\tau_2\) the Euler tours of two trees and \(r\) the root of the first tree: walk the first tour, then the second tour, then return to \(r\).

def spliceLink (tour₁ tour₂ : List V) (r : V) : List V :=
  tour₁ ++ tour₂ ++ [r]

TheoremEuler tour of a linked tree#✓fully proved

For trees \(t_1\) and \(t_2\), let \(t\) be the link of \(t_1\) and \(t_2\), that is, \(t_1\) with \(t_2\) added as the last child subtree of its root. The Euler tour of \(t\) is the Euler tour of \(t_1\), followed by the Euler tour of \(t_2\), followed by the root of \(t_1\).

theorem tour_link (t₁ t₂ : Tree V) :
    tour (link t₁ t₂) = tour t₁ ++ (tour t₂ ++ [t₁.root])

Uses 5

Statement usesRooted ordered tree · Linking two rooted trees · Root of a rooted tree · Euler tour

Proof usesRecursive formula for the Euler tour

DefinitionCutting the last child subtree#✓fully proved

Let \(t\) be a tree with root \(r\) and child subtrees \(c_1, \dots, c_k\). Cutting the last child subtree of \(t\) gives no result when \(k = 0\); when \(k \ge 1\) it gives the pair consisting of the tree with root \(r\) and child subtrees \(c_1, \dots, c_{k-1}\), together with the removed subtree \(c_k\).

def cutLast : Tree V → Option (Tree V × Tree V)
  | .node r cs => cs.getLast?.map (fun last => (.node r cs.dropLast, last))

Uses 1

Statement usesRooted ordered tree

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.