Link-cut tree

83 fully proved

Link Cut Tree

DefinitionPath tree on a vertex list#✓fully proved

For a vertex \(r\) and a list of vertices \(c_1, \dots, c_k\), the spine is the rooted tree \(r \to c_1 \to \cdots \to c_k\): its root is \(r\), each vertex has the next one in the list as its only child, and the last vertex (\(c_k\), or \(r\) when \(k = 0\)) is a leaf.

public def spine : V → List V → Tree V
  | r, [] => .node r []
  | r, c :: cs => .node r [spine c cs]

Uses 1 · Used by 1

Statement usesRooted ordered tree

Used byForest from a vertex list

DefinitionForest from a vertex list#✓fully proved

The forest built from the empty list is empty; the forest built from a list \(r, c_1, \dots, c_k\) consists of the single spine \(r \to c_1 \to \cdots \to c_k\), the rooted tree in which each vertex has the next one as its only child.

public def ofVertexList : List V → List (Tree V)
  | [] => []
  | r :: rs => [spine r rs]

Uses 2

Statement usesRooted ordered tree · Path tree on a vertex list

DefinitionTree of a forest containing a vertex#✓fully proved

For a vertex \(x\) and a forest given as a list of trees, the first tree whose vertices contain \(x\), or nothing when no tree contains \(x\).

public def findTree (x : V) : List (Tree V) → Option (Tree V)
  | [] => none
  | t :: ts => if x ∈ Tree.vertices t then some t else findTree x ts

Uses 2 · Used by 20

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

Used byAccess in a link-cut tree · Access preserves validity · Access leaves the represented forest unchanged · After access, the accessed vertex ends its preferred path · An edge cut keeps every other edge · Linking connects the endpoints · Making a vertex the root keeps its connections · Cutting off the subtree at a vertex · Cutting preserves validity · 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 · Both sides of a cut remain in the forest · Access keeps off-path preferred edges · Access makes the root path preferred · 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

DefinitionRemoving the trees that contain a vertex#✓fully proved

Given a vertex \(x\) and a forest, given as a list of rooted ordered trees, removing the trees containing \(x\) deletes from the list every tree that has \(x\) among its vertices and keeps the remaining trees in their original order.

public def removeTree (x : V) : List (Tree V) → List (Tree V)
  | [] => []
  | t :: ts => if x ∈ Tree.vertices t then removeTree x ts else t :: removeTree x ts

Uses 2 · Used by 14

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

Used byAn edge cut keeps every other edge · Linking connects the endpoints · Making a vertex the root keeps its connections · Cutting off the subtree at a vertex · Cutting preserves validity · 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 · Both sides of a cut remain in the forest · 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

TheoremRemoving the tree containing a vertex splits the forest's vertices#✓fully proved

Let \(f\) be a forest of rooted ordered trees whose concatenated vertex lists have no duplicates, let \(x\) be a vertex, and let \(t\) be the first tree of \(f\) containing \(x\). Then the concatenated vertex list of the forest obtained from \(f\) by removing every tree containing \(x\), followed by the vertex list of \(t\), is a permutation of the concatenated vertex list of \(f\).

public theorem perm_flatMap_removeTree {x : V} :
    ∀ {f : List (Tree V)} {t : Tree V},
      (f.flatMap Tree.vertices).Nodup → findTree x f = some t →
      ((removeTree x f).flatMap Tree.vertices ++ Tree.vertices t).Perm
        (f.flatMap Tree.vertices)

Uses 4 · Used by 3

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Tree of a forest containing a vertex · Removing the trees that contain a vertex

Used byCutting preserves validity · Linking in a link-cut tree preserves validity · Rerooting a link-cut tree state preserves validity

DefinitionSubtree rooted at a vertex#✓fully proved

For a vertex \(x\) and a tree \(T\), the subtree of \(T\) rooted at the first occurrence of \(x\) in preorder, or nothing when \(x\) does not occur in \(T\).

public def findSubtree (x : V) : Tree V → Option (Tree V)
  | .node r cs => if r = x then some (.node r cs) else findSubtreeList x cs
where
  findSubtreeList (x : V) : List (Tree V) → Option (Tree V)
    | [] => none
    | c :: cs =>
        match findSubtree x c with
        | some s => some s
        | none => findSubtreeList x cs

Uses 1 · Used by 8

Statement usesRooted ordered tree

Used byAn edge cut keeps every other edge · Cutting off the subtree at a vertex · Cutting preserves validity · Both sides of a cut remain in the forest · Pruning keeps the vertices outside the detached subtree · A cut disconnects a vertex from everything outside its subtree · Cutting an edge separates its endpoints · Pruning a subtree splits the vertex list

DefinitionAdjacency in a rooted tree#✓fully proved

Two vertices \(a\) and \(b\) are adjacent in a rooted tree \(t\) when they are joined by a parent-child edge of \(t\) in either direction: some node of \(t\) labelled \(a\) has a child labelled \(b\), or some node of \(t\) labelled \(b\) has a child labelled \(a\).

This is the undirected edge relation that the structural operations of the link-cut tree are specified against.

public def Adjacent (a b : V) : Tree V → Prop
  | .node r cs =>
      (r = a ∧ ∃ c ∈ cs, c.root = b) ∨ (r = b ∧ ∃ c ∈ cs, c.root = a) ∨
        AdjacentList a b cs
where
  /-- Adjacency inside one of a list of subtrees. -/
  AdjacentList (a b : V) : List (Tree V) → Prop
    | [] => False
    | c :: cs => Adjacent a b c ∨ AdjacentList a b cs

Uses 2 · Used by 15

Statement usesRooted ordered tree · Root of a rooted tree

Used byParent-child edges are edges · An edge cut keeps every other edge · Edges after grafting · Pruning keeps surviving edges · Rerooting keeps every edge · Edge cut on an adjacent pair · Edge cut on a non-adjacent pair · Decomposition paths are paths of the tree · 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 · The first endpoint of a tree edge is a vertex · The second endpoint of a tree edge is a vertex · Cutting an edge separates its endpoints · Adjacency in a tree is symmetric

TheoremThe first endpoint of a tree edge is a vertex#✓fully proved

If \(a\) and \(b\) are adjacent in a tree \(t\), that is, joined by a parent-child edge in either direction, then \(a\) is a vertex of \(t\).

public theorem Adjacent.mem_left {a b : V} :
    ∀ {t : Tree V}, Adjacent a b t → a ∈ Tree.vertices t

Uses 6 · Used by 5

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

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a node

Used byAn edge cut keeps every other edge · Pruning keeps surviving edges · The parent endpoint of a tree edge is a vertex · The second endpoint of a tree edge is a vertex · Cutting an edge separates its endpoints

TheoremAdjacency in a tree is symmetric#✓fully proved

For every rooted ordered tree \(T\) and vertices \(a\) and \(b\), if \(a\) and \(b\) are adjacent in \(T\) (joined by a parent-child edge in either direction), then \(b\) and \(a\) are adjacent in \(T\).

public theorem Adjacent.symm {a b : V} :
    ∀ {t : Tree V}, Adjacent a b t → Adjacent b a t

Uses 4 · Used by 2

Statement usesRooted ordered tree · Adjacency in a rooted tree

Proof usesInduction principle for rooted trees · Root of a rooted tree

Used byAn edge cut keeps every other edge · The second endpoint of a tree edge is a vertex

TheoremThe second endpoint of a tree edge is a vertex#✓fully proved

If \(a\) and \(b\) are adjacent in a tree \(t\), that is, joined by a parent-child edge in either direction, then \(b\) is a vertex of \(t\).

public theorem Adjacent.mem_right {a b : V} {t : Tree V}
    (h : Adjacent a b t) : b ∈ Tree.vertices t

Uses 5 · Used by 4

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

Proof usesThe first endpoint of a tree edge is a vertex · Adjacency in a tree is symmetric

Used byAn edge cut keeps every other edge · Pruning keeps surviving edges · The child endpoint of a tree edge is a vertex · Cutting an edge separates its endpoints

DefinitionAdjacency test#✓fully proved

For vertices \(a\), \(b\) and a rooted tree \(t\) with root \(r\) and child subtrees \(c_1, \dots, c_k\), the adjacency test of \(a\) and \(b\) in \(t\) returns true exactly when \(r = a\) and some \(c_i\) has root \(b\), or \(r = b\) and some \(c_i\) has root \(a\), or the adjacency test of \(a\) and \(b\) returns true in some \(c_i\).

It returns true exactly when \(a\) and \(b\) are adjacent in \(t\), and it is the guard checked by the edge cut before it cuts.

public def adjacentB (a b : V) : Tree V → Bool
  | .node r cs =>
      (decide (r = a) && cs.any (fun c => decide (c.root = b))) ||
        (decide (r = b) && cs.any (fun c => decide (c.root = a))) ||
        adjacentBList a b cs
where
  /-- Adjacency test over a list of subtrees. -/
  adjacentBList (a b : V) : List (Tree V) → Bool
    | [] => false
    | c :: cs => adjacentB a b c || adjacentBList a b cs

Uses 2 · Used by 4

Statement usesRooted ordered tree · Root of a rooted tree

Used byCutting an edge of a link-cut tree · Edge cutting preserves validity · Edge cut on an adjacent pair · Edge cut on a non-adjacent pair

DefinitionGrafting a tree below a vertex#✓fully proved

For a vertex \(y\) and trees \(N\) and \(T\), grafting \(N\) at \(y\) in \(T\) attaches \(N\) as a new last child of the first node of \(T\) labelled \(y\) in preorder, keeping every existing node and edge; it returns nothing when \(y\) does not occur in \(T\). This is the tree surgery behind linking two trees: it adds exactly the edge from \(y\) to the root of \(N\).

public def graftAt (y : V) (newChild : Tree V) : Tree V → Option (Tree V)
  | .node r cs =>
      if r = y then some (.node r (cs ++ [newChild]))
      else (graftAtList y newChild cs).map (.node r)
where
  graftAtList (y : V) (newChild : Tree V) :
      List (Tree V) → Option (List (Tree V))
    | [] => none
    | c :: cs =>
        match graftAt y newChild c with
        | some c' => some (c' :: cs)
        | none => (graftAtList y newChild cs).map (c :: ·)

Uses 1 · Used by 16

Statement usesRooted ordered tree

Used byAn edge cut keeps every other edge · Edges after grafting · Rerooting keeps every edge · Linking connects the endpoints · Making a vertex the root keeps its connections · Linking two trees of a link-cut tree state · Linking in a link-cut tree preserves validity · Making a vertex the root installs a tree rooted there · Vertices after grafting · Rerooting preserves the vertex set · Cutting an edge separates its endpoints · Grafting adds the new subtree's vertices · Rerooting preserves the vertices · Rerooting a tree at a vertex · Rerooting fails at an absent vertex · Grafting keeps the root

TheoremVertices after grafting#✓fully proved

Let \(t\) and \(C\) be trees and \(y\) a vertex. If grafting \(C\) at \(y\) in \(t\), that is, attaching \(C\) as a new last child of a node labelled \(y\), produces the tree \(t'\), then for every \(v\), \(v\) is a vertex of \(t'\) if and only if \(v\) is a vertex of \(t\) or a vertex of \(C\).

public theorem mem_vertices_graftAt {y v : V} {newChild : Tree V} :
    ∀ {t t' : Tree V}, graftAt y newChild t = some t' →
      (v ∈ Tree.vertices t' ↔ v ∈ Tree.vertices t ∨ v ∈ Tree.vertices newChild)

Uses 5 · Used by 6

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

Proof usesInduction principle for rooted trees · Preorder vertex list of a node

Used byAn edge cut keeps every other edge · Linking connects the endpoints · Making a vertex the root keeps its connections · Making a vertex the root installs a tree rooted there · Rerooting preserves the vertex set · Cutting an edge separates its endpoints

TheoremGrafting keeps the root#✓fully proved

Let \(T\) and \(N\) be rooted ordered trees and \(y\) a vertex. If grafting \(N\) into \(T\) at \(y\) is defined and yields the tree \(T'\), then the root of \(T'\) equals the root of \(T\).

public theorem root_graftAt {y : V} {newChild : Tree V} :
    ∀ {t t' : Tree V}, graftAt y newChild t = some t' → t'.root = t.root

Uses 4 · Used by 7

Statement usesRooted ordered tree · Root of a rooted tree · Grafting a tree below a vertex

Proof usesInduction principle for rooted trees

Used byAn edge cut keeps every other edge · Edges after grafting · Linking connects the endpoints · Making a vertex the root keeps its connections · Making a vertex the root installs a tree rooted there · Rerooting preserves the vertex set · Cutting an edge separates its endpoints

TheoremEdges after grafting#✓fully proved

Let \(t\) and \(u\) be rooted trees and \(y\) a vertex, and suppose that grafting \(u\) as a new child under \(y\) in \(t\) succeeds and yields the tree \(t'\). Then for all vertices \(a\) and \(b\), the vertices \(a\) and \(b\) are adjacent in \(t'\) if and only if they are adjacent in \(t\), or adjacent in \(u\), or \(a = y\) and \(b\) is the root of \(u\), or \(a\) is the root of \(u\) and \(b = y\).

public theorem adjacent_graftAt {y a b : V} {newChild : Tree V} :
    ∀ {t t' : Tree V}, graftAt y newChild t = some t' →
      (Adjacent a b t' ↔ Adjacent a b t ∨ Adjacent a b newChild ∨
        (a = y ∧ b = newChild.root) ∨ (a = newChild.root ∧ b = y))

Uses 6 · Used by 1

Statement usesRooted ordered tree · Root of a rooted tree · Adjacency in a rooted tree · Grafting a tree below a vertex

Proof usesInduction principle for rooted trees · Grafting keeps the root

Used byRerooting keeps every edge

TheoremGrafting adds the new subtree's vertices#✓fully proved

Let \(t\) and \(s\) be rooted ordered trees and \(y\) a vertex. If grafting \(s\) as a new child at \(y\) in \(t\) succeeds and yields the tree \(t'\), then the vertex list of \(t'\) is a permutation of the vertex list of \(t\) followed by the vertex list of \(s\).

public theorem perm_vertices_graftAt {y : V} {newChild : Tree V} :
    ∀ {t t' : Tree V}, graftAt y newChild t = some t' →
      (Tree.vertices t').Perm (Tree.vertices t ++ Tree.vertices newChild)

Uses 5 · Used by 2

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

Proof usesInduction principle for rooted trees · Preorder vertex list of a node

Used byLinking in a link-cut tree preserves validity · Rerooting preserves the vertices

DefinitionRerooting a tree at a vertex#✓fully proved

For a vertex \(x\) and a rooted ordered tree \(T\) with root \(r\), rerooting \(T\) at \(x\) is defined recursively. If \(r = x\), the result is \(T\) itself. Otherwise let \(C\) be the first child subtree of \(r\) that contains \(x\), let \(p\) be the root of \(C\), and let \(C'\) be \(C\) rerooted at \(x\). The result is \(C'\) with the tree formed by \(r\) and its remaining children (in their original order) attached as a new last child of the first node of \(C'\), in preorder, labelled \(p\). If no child subtree of \(r\) contains \(x\), rerooting is undefined; thus rerooting is defined exactly when \(x\) is a vertex of \(T\).

When the vertices of \(T\) are distinct, this reverses the edges on the path from \(r\) to \(x\) and keeps every other edge, so the undirected tree is unchanged and only the root moves to \(x\). This is the tree surgery behind making \(x\) the root in a link-cut tree.

Cslib.Algorithms.Lean.LinkCutTree.rerootAt · 19 lines

public def rerootAt (x : V) : Tree V → Option (Tree V)
  | .node r cs =>
      if r = x then some (.node r cs)
      else
        match rerootAtList x cs with
        | some (c', rest, p) => graftAt p (.node r rest) c'
        | none => none
where
  /-- Reroot the first child subtree containing `x`; returns the rerooted
  child, the remaining sibling subtrees in order, and the root of the
  original child (the next vertex on the root-to-`x` path, under which the
  caller reattaches the remainder). -/
  rerootAtList (x : V) : List (Tree V) → Option (Tree V × List (Tree V) × V)
    | [] => none
    | c :: cs =>
        match rerootAt x c with
        | some c' => some (c', cs, c.root)
        | none =>
            (rerootAtList x cs).map (fun (c', rest, p) => (c', c :: rest, p))

Uses 3 · Used by 13

Statement usesRooted ordered tree · Root of a rooted tree · Grafting a tree below a vertex

Used byAn edge cut keeps every other edge · Rerooting keeps every edge · Linking connects the endpoints · Making a vertex the root keeps its connections · 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 · Rerooting preserves the vertex set · Cutting an edge separates its endpoints · Rerooting preserves the vertices · Rerooting fails at an absent vertex

TheoremRerooting fails at an absent vertex#✓fully proved

For every rooted ordered tree \(T\) and every vertex \(x\) that is not a vertex of \(T\), rerooting \(T\) at \(x\) is undefined (it returns no tree).

public theorem rerootAt_eq_none_of_not_mem {x : V} :
    ∀ {t : Tree V}, x ∉ Tree.vertices t → rerootAt x t = none

Uses 7 · Used by 6

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

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a node · Grafting a tree below a vertex

Used byAn edge cut keeps every other edge · Linking connects the endpoints · Making a vertex the root keeps its connections · Making a vertex the root installs a tree rooted there · Rerooting preserves the vertex set · Cutting an edge separates its endpoints

TheoremRerooting preserves the vertex set#✓fully proved

Let \(t\) be a rooted tree and \(x\) a vertex. If rerooting \(t\) at \(x\) yields the tree \(t'\), then a vertex lies in \(t'\) if and only if it lies in \(t\).

public theorem mem_vertices_rerootAt {x v : V} :
    ∀ {t t' : Tree V}, rerootAt x t = some t' →
      (v ∈ Tree.vertices t' ↔ v ∈ Tree.vertices t)

Uses 10 · Used by 5

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

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a node · Grafting a tree below a vertex · Vertices after grafting · Rerooting fails at an absent vertex · Grafting keeps the root

Used byAn edge cut keeps every other edge · Linking connects the endpoints · Making a vertex the root keeps its connections · Making a vertex the root installs a tree rooted there · Cutting an edge separates its endpoints

TheoremRerooting keeps every edge#✓fully proved

Let \(t\) be a rooted tree with no repeated vertex, and suppose that rerooting \(t\) at a vertex \(x\) yields the tree \(t'\). Then for all vertices \(a\) and \(b\), the vertices \(a\) and \(b\) are adjacent in \(t'\) if and only if they are adjacent in \(t\).

public theorem adjacent_rerootAt {x a b : V} :
    ∀ {t t' : Tree V}, (Tree.vertices t).Nodup → rerootAt x t = some t' →
      (Adjacent a b t' ↔ Adjacent a b t)

Uses 9 · Used by 2

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Adjacency in a rooted tree · Rerooting a tree at a vertex

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a node · Edges after grafting · Grafting a tree below a vertex

Used byAn edge cut keeps every other edge · Cutting an edge separates its endpoints

TheoremRerooting preserves the vertices#✓fully proved

Let \(t\) be a rooted ordered tree and \(x\) a vertex. If rerooting \(t\) at \(x\) yields the tree \(t'\), then the vertex list of \(t'\) is a permutation of the vertex list of \(t\).

public theorem perm_vertices_rerootAt {x : V} :
    ∀ {t t' : Tree V}, rerootAt x t = some t' →
      (Tree.vertices t').Perm (Tree.vertices t)

Uses 8 · Used by 4

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

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a node · Grafting a tree below a vertex · Grafting adds the new subtree's vertices

Used byAn edge cut keeps every other edge · Linking in a link-cut tree preserves validity · Rerooting a link-cut tree state preserves validity · Cutting an edge separates its endpoints

DefinitionPruning the subtrees rooted at a vertex#✓fully proved

For a vertex \(x\) and a rooted ordered tree \(T\), pruning \(T\) at \(x\) removes every subtree of \(T\) whose root is labelled \(x\), keeping every other node and edge and the order of children. If the root of \(T\) is \(x\), nothing remains and pruning is undefined. Otherwise the result is the tree with the same root whose children are, in their original order, the pruned children of the root, with the children labelled \(x\) dropped.

This is the tree surgery behind the remainder side of the cut operation of a link-cut tree.

public def pruneAt (x : V) : Tree V → Option (Tree V)
  | .node r cs => if r = x then none else some (.node r (pruneList x cs))
where
  pruneList (x : V) : List (Tree V) → List (Tree V)
    | [] => []
    | c :: cs =>
        match pruneAt x c with
        | some c' => c' :: pruneList x cs
        | none => pruneList x cs

Uses 1 · Used by 11

Statement usesRooted ordered tree

Used byAn edge cut keeps every other edge · Pruning keeps surviving edges · Cutting off the subtree at a vertex · Cutting preserves validity · Both sides of a cut remain in the forest · Vertices of a pruned tree · Pruning keeps the vertices outside the detached subtree · A cut disconnects a vertex from everything outside its subtree · Pruning a subtree splits the vertex list · Pruning at an absent vertex changes nothing · Pruning keeps the root

TheoremPruning at an absent vertex changes nothing#✓fully proved

Let \(t\) be a rooted ordered tree and \(x\) a vertex that does not occur in \(t\). Then pruning the subtrees rooted at \(x\) from \(t\) succeeds and returns \(t\) itself.

public theorem pruneAt_eq_self_of_not_mem {x : V} :
    ∀ {t : Tree V}, x ∉ Tree.vertices t → pruneAt x t = some t

Uses 5 · Used by 2

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Pruning the subtrees rooted at a vertex

Proof usesInduction principle for rooted trees · Preorder vertex list of a node

Used byPruning keeps the vertices outside the detached subtree · Pruning a subtree splits the vertex list

TheoremVertices of a pruned tree#✓fully proved

Let \(t\) be a rooted tree and \(x\) a vertex. If pruning \(t\) at \(x\) leaves the tree \(t'\), then every vertex of \(t'\) is a vertex of \(t\) and is different from \(x\).

public theorem mem_vertices_pruneAt {x v : V} :
    ∀ {t t' : Tree V}, pruneAt x t = some t' → v ∈ Tree.vertices t' →
      v ∈ Tree.vertices t ∧ v ≠ x

Uses 5 · Used by 2

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Pruning the subtrees rooted at a vertex

Proof usesInduction principle for rooted trees · Preorder vertex list of a node

Used byPruning keeps surviving edges · A cut disconnects a vertex from everything outside its subtree

TheoremPruning keeps the vertices outside the detached subtree#✓fully proved

Let \(t\) be a rooted tree whose preorder vertex list has no repeated vertex, and let \(x\) be a vertex. Suppose the subtree search finds the subtree \(s\) of \(t\) rooted at \(x\), and pruning \(t\) at \(x\) leaves the tree \(t'\). Then every vertex of \(t\) that is not a vertex of \(s\) is a vertex of \(t'\).

public theorem mem_vertices_pruneAt_of_mem_not_mem {x v : V} :
    ∀ {t sub t' : Tree V}, (Tree.vertices t).Nodup →
      findSubtree x t = some sub → pruneAt x t = some t' →
      v ∈ Tree.vertices t → v ∉ Tree.vertices sub →
      v ∈ Tree.vertices t'

Uses 8 · Used by 1

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Subtree rooted at a vertex · Pruning the subtrees rooted at a vertex

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a node · Pruning at an absent vertex changes nothing

Used byBoth sides of a cut remain in the forest

TheoremPruning a subtree splits the vertex list#✓fully proved

Let \(t\) be a rooted ordered tree whose vertex list has no duplicates and let \(x\) be a vertex. If \(x\) occurs in \(t\), with \(s\) the subtree of \(t\) rooted at \(x\), and pruning at \(x\) leaves a tree \(t'\) (that is, \(x\) is not the root of \(t\)), then the vertex list of \(t\) is a permutation of the vertex list of \(t'\) followed by the vertex list of \(s\).

public theorem perm_vertices_pruneAt {x : V} :
    ∀ {t sub t' : Tree V}, (Tree.vertices t).Nodup →
      findSubtree x t = some sub → pruneAt x t = some t' →
      (Tree.vertices t).Perm (Tree.vertices t' ++ Tree.vertices sub)

Uses 8 · Used by 2

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Subtree rooted at a vertex · Pruning the subtrees rooted at a vertex

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a node · Pruning at an absent vertex changes nothing

Used byAn edge cut keeps every other edge · Cutting preserves validity

TheoremPruning keeps the root#✓fully proved

Let \(T\) be a rooted ordered tree and \(x\) a vertex. If pruning \(T\) at \(x\) yields a tree \(T'\) (that is, the root of \(T\) is not \(x\)), then the root of \(T'\) equals the root of \(T\).

public theorem root_pruneAt {x : V} {t t' : Tree V}
    (h : pruneAt x t = some t') : t'.root = t.root

Uses 3 · Used by 1

Statement usesRooted ordered tree · Root of a rooted tree · Pruning the subtrees rooted at a vertex

Used byPruning keeps surviving edges

TheoremPruning keeps surviving edges#✓fully proved

Let \(t\) be a rooted tree with no repeated vertex and \(x\) a vertex, and suppose that removing every subtree rooted at \(x\) from \(t\) leaves the tree \(t'\) (that is, the root of \(t\) is not \(x\)). If \(a\) and \(b\) are adjacent in \(t\) and both are vertices of \(t'\), then \(a\) and \(b\) are adjacent in \(t'\).

Together with the fact that every vertex of \(t'\) is a vertex of \(t\) other than \(x\), this specifies pruning at the level of edges on the surviving vertices.

public theorem adjacent_pruneAt_of_mem_mem {a b x : V} :
    ∀ {t t' : Tree V}, (Tree.vertices t).Nodup →
      pruneAt x t = some t' → Adjacent a b t →
      a ∈ Tree.vertices t' → b ∈ Tree.vertices t' →
      Adjacent a b t'

Uses 11 · Used by 1

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Adjacency in a rooted tree · Pruning the subtrees rooted at a vertex

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a node · The first endpoint of a tree edge is a vertex · The second endpoint of a tree edge is a vertex · Vertices of a pruned tree · Pruning keeps the root

Used byAn edge cut keeps every other edge

DefinitionRoot-to-vertex path#✓fully proved

For a vertex \(x\) and a rooted ordered tree \(T\), the root path of \(x\) is defined exactly when \(x\) is a vertex of \(T\). It is then the list of vertices on the path from the root of \(T\) down to \(x\), root first and ending with \(x\); if \(x\) occurs more than once, the path leads to its first occurrence in preorder.

This is the preferred path installed by the access operation of a link-cut tree.

public def rootPath (x : V) : Tree V → Option (List V)
  | .node r cs =>
      if r = x then some [r] else (rootPathList x cs).map (fun p => r :: p)
where
  rootPathList (x : V) : List (Tree V) → Option (List V)
    | [] => none
    | c :: cs =>
        match rootPath x c with
        | some p => some p
        | none => rootPathList x cs

Uses 1 · Used by 13

Statement usesRooted ordered tree

Used byAccess in a link-cut tree · Access preserves validity · Access leaves the represented forest unchanged · After access, the accessed vertex ends its preferred path · Access edges make the root path the downward preferred path · A root path ends at its target · The root path starts at the root · Consecutive vertices of a root path are adjacent · A root path follows parent-child edges downward · Access keeps off-path preferred edges · Access makes the root path preferred · Root paths stay inside the tree · Root paths have distinct vertices

TheoremA root path ends at its target#✓fully proved

If \(p\) is the path from the root of a tree \(T\) down to a vertex \(x\) of \(T\), then \(p\) is nonempty and its last (deepest) vertex is \(x\).

public theorem getLast?_rootPath {x : V} {t : Tree V} {p : List V}
    (h : rootPath x t = some p) : p.getLast? = some x

Uses 3 · Used by 2

Statement usesRooted ordered tree · Root-to-vertex path

Proof usesInduction principle for rooted trees

Used byAfter access, the accessed vertex ends its preferred path · Access edges make the root path the downward preferred path

TheoremThe root path starts at the root#✓fully proved

Let \(t\) be a tree and \(x\) a vertex. If the root path of \(x\) in \(t\) (the path from the root of \(t\) down to \(x\)) is defined and equals \(p\), then \(p\) is nonempty and its first vertex is the root of \(t\).

public theorem head?_rootPath {x : V} {t : Tree V} {p : List V}
    (h : rootPath x t = some p) : p.head? = some t.root

Uses 3 · Used by 3

Statement usesRooted ordered tree · Root of a rooted tree · Root-to-vertex path

Used byAccess edges make the root path the downward preferred path · Consecutive vertices of a root path are adjacent · A root path follows parent-child edges downward

TheoremRoot paths stay inside the tree#✓fully proved

If \(p\) is the path in a tree \(t\) from the root down to a vertex \(x\), then every vertex of \(p\) is a vertex of \(t\).

public theorem mem_rootPath {x v : V} {t : Tree V} {p : List V}
    (h : rootPath x t = some p) (hv : v ∈ p) : v ∈ Tree.vertices t

Uses 5 · Used by 1

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Root-to-vertex path

Proof usesInduction principle for rooted trees · Preorder vertex list of a node

Used byRoot paths have distinct vertices

TheoremRoot paths have distinct vertices#✓fully proved

If the preorder vertex list of a rooted tree \(t\) has no repeated vertex and \(p\) is the path from the root of \(t\) down to a vertex \(x\), then \(p\) has no repeated vertex.

public theorem nodup_rootPath {x : V} :
    ∀ {t : Tree V} {p : List V}, (Tree.vertices t).Nodup →
      rootPath x t = some p → p.Nodup

Uses 6 · Used by 2

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Root-to-vertex path

Proof usesInduction principle for rooted trees · Preorder vertex list of a node · Root paths stay inside the tree

Used byAccess preserves validity · Access edges make the root path the downward preferred path

TheoremConsecutive vertices of a root path are adjacent#✓fully proved

Let \(t\) be a tree and \(x\) a vertex. If the root path of \(x\) in \(t\) is defined and equals \(p = (p_0, \dots, p_k)\), then for every \(i < k\) the vertices \(p_i\) and \(p_{i+1}\) are adjacent in \(t\), that is, joined by a parent-child edge of \(t\) in one direction or the other.

public theorem isChain_adjacent_rootPath {x : V} :
    ∀ {t : Tree V} {p : List V}, rootPath x t = some p →
      p.IsChain (fun a b => Adjacent a b t)

Uses 6

Statement usesRooted ordered tree · Adjacency in a rooted tree · Root-to-vertex path

Proof usesInduction principle for rooted trees · Root of a rooted tree · The root path starts at the root

DefinitionParent-child relation in a rooted tree#✓fully proved

For vertices \(a\) and \(b\) and a rooted ordered tree \(t\), \(a\) is a parent of \(b\) in \(t\) when some node of \(t\) labelled \(a\) has a child subtree whose root is \(b\). Preferred edges of a link-cut tree are directed this way, from a node to its preferred child.

public def ParentChild (a b : V) : Tree V → Prop
  | .node r cs => (r = a ∧ ∃ c ∈ cs, c.root = b) ∨ ParentChildList a b cs
where
  /-- Directed parent-child adjacency inside one of a list of subtrees. -/
  ParentChildList (a b : V) : List (Tree V) → Prop
    | [] => False
    | c :: cs => ParentChild a b c ∨ ParentChildList a b cs

Uses 2 · Used by 16

Statement usesRooted ordered tree · Root of a rooted tree

Used byAccess preserves validity · After access, the accessed vertex ends its preferred path · Parent-child edges are edges · An edge cut keeps every other edge · Making a vertex the root keeps its connections · Cutting preserves validity · Edge cutting preserves validity · A root path follows parent-child edges downward · Linking in a link-cut tree preserves validity · Rerooting a link-cut tree state preserves validity · The parent endpoint of a tree edge is a vertex · The child endpoint of a tree edge is a vertex · Preferred paths cover each vertex at most once · Cutting an edge separates its endpoints · Valid link-cut tree states · Validity of states with no preferred edges

TheoremParent-child edges are edges#✓fully proved

For every rooted tree \(t\) and all vertices \(a\) and \(b\), if \(a\) is the parent of \(b\) somewhere in \(t\), then \(a\) and \(b\) are adjacent in \(t\).

public theorem ParentChild.adjacent {a b : V} :
    ∀ {t : Tree V}, ParentChild a b t → Adjacent a b t

Uses 5 · Used by 2

Statement usesRooted ordered tree · Adjacency in a rooted tree · Parent-child relation in a rooted tree

Proof usesInduction principle for rooted trees · Root of a rooted tree

Used byThe parent endpoint of a tree edge is a vertex · The child endpoint of a tree edge is a vertex

TheoremThe parent endpoint of a tree edge is a vertex#✓fully proved

If \(a\) is the parent of \(b\) somewhere in a tree \(t\), then \(a\) is a vertex of \(t\).

public theorem ParentChild.mem_left {a b : V} {t : Tree V}
    (h : ParentChild a b t) : a ∈ Tree.vertices t

Uses 5

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Parent-child relation in a rooted tree

Proof usesThe first endpoint of a tree edge is a vertex · Parent-child edges are edges

TheoremThe child endpoint of a tree edge is a vertex#✓fully proved

If \(a\) is the parent of \(b\) somewhere in a tree \(t\), then \(b\) is a vertex of \(t\).

public theorem ParentChild.mem_right {a b : V} {t : Tree V}
    (h : ParentChild a b t) : b ∈ Tree.vertices t

Uses 5

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Parent-child relation in a rooted tree

Proof usesThe second endpoint of a tree edge is a vertex · Parent-child edges are edges

TheoremA root path follows parent-child edges downward#✓fully proved

Let \(t\) be a tree and \(x\) a vertex. If the root path of \(x\) in \(t\) is defined and equals \(p = (p_0, \dots, p_k)\), then for every \(i < k\) the vertex \(p_i\) is the parent of \(p_{i+1}\) somewhere in \(t\).

public theorem isChain_parentChild_rootPath {x : V} :
    ∀ {t : Tree V} {p : List V}, rootPath x t = some p →
      p.IsChain (fun a b => ParentChild a b t)

Uses 6 · Used by 1

Statement usesRooted ordered tree · Parent-child relation in a rooted tree · Root-to-vertex path

Proof usesInduction principle for rooted trees · Root of a rooted tree · The root path starts at the root

Used byAccess preserves validity

DefinitionConsecutive edges of a vertex path#✓fully proved

For a list of vertices \(v_0, v_1, \dots, v_n\), its path edges are the ordered pairs \((v_0, v_1), (v_1, v_2), \dots, (v_{n-1}, v_n)\) of consecutive vertices, in this order; a list with at most one vertex has no path edges. For a path listed from the root downward each pair is (parent, child), and the preferred edges installed by an access to a vertex \(x\) are the path edges of the root-to-\(x\) path.

public def pathEdges : List V → List (V × V)
  | [] => []
  | [_] => []
  | a :: b :: rest => (a, b) :: pathEdges (b :: rest)

Used by 7

Used byAccess in a link-cut tree · Access preserves validity · Access leaves the represented forest unchanged · After access, the accessed vertex ends its preferred path · Access edges make the root path the downward preferred path · Access keeps off-path preferred edges · Access makes the root path preferred

DefinitionPreferred-path decomposition of a tree#✓fully proved

Given a list \(E\) of preferred edges, each a pair (parent, preferred child), the decomposition of a tree \(T\) is a pair (down, rest): down is the preferred path that starts at the root of \(T\) and follows edges of \(E\) downward, and rest is the list of all other preferred paths of \(T\). When a node has several children joined to it by edges of \(E\) (excluded in valid states, where each vertex has at most one preferred child), the first one in child order continues the path through that node and each of the others starts its own path in rest.

Cslib.Algorithms.Lean.LinkCutTree.decomp · 18 lines

public def decomp (edges : List (V × V)) : Tree V → List V × List (List V)
  | .node r cs =>
      match decompList edges r cs with
      | (ext, rest) => (r :: ext, rest)
where
  /-- Combine the decompositions of the children of `r`: returns the
  downward continuation below `r` (the root path of the preferred child, or
  `[]` when no child is preferred) and every other path below `r`. -/
  decompList (edges : List (V × V)) (r : V) :
      List (Tree V) → List V × List (List V)
    | [] => ([], [])
    | c :: cs =>
        match decomp edges c, decompList edges r cs with
        | (cdown, crest), (ext, rest) =>
            if (r, c.root) ∈ edges then
              (cdown, crest ++ if ext = [] then rest else ext :: rest)
            else
              (ext, (cdown :: crest) ++ rest)

Uses 2 · Used by 8

Statement usesRooted ordered tree · Root of a rooted tree

Used byAfter access, the accessed vertex ends its preferred path · 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 · Preferred paths of a tree follow tree edges · The preferred paths of a tree rearrange its vertex list · Preferred paths of a tree

DefinitionPreferred paths of a tree#✓fully proved

Let \(t\) be a rooted ordered tree and let \(E\) be a list of preferred edges, each a pair (parent, child). The preferred paths of \(t\) under \(E\) are listed as follows: first the downward path of the preferred-path decomposition of \(t\) under \(E\), which starts at the root of \(t\) and follows preferred edges downward, and then all other paths of that decomposition, in the order the decomposition returns them.

public def treePaths (edges : List (V × V)) (t : Tree V) : List (List V) :=
  (decomp edges t).1 :: (decomp edges t).2

Uses 2 · Used by 8

Statement usesRooted ordered tree · Preferred-path decomposition of a tree

Used byAfter access, the accessed vertex ends its preferred path · Decomposition paths are paths of the tree · Preferred paths of a link-cut tree state follow represented edges · Preferred paths of a tree follow tree edges · Preferred paths cover exactly the vertices of the forest · Preferred paths cover each vertex at most once · Preferred-path decomposition of a link-cut tree state · The preferred paths of a tree rearrange its vertex list

TheoremThe downward preferred path starts at the root#✓fully proved

For every list of preferred edges, the downward preferred path in the preferred-path decomposition of a tree is nonempty and its first vertex is the root of the tree.

public theorem decomp_fst_head? (edges : List (V × V)) (t : Tree V) :
    (decomp edges t).1.head? = some t.root

Uses 3 · Used by 1

Statement usesRooted ordered tree · Root of a rooted tree · Preferred-path decomposition of a tree

Used byDecomposition paths are paths of the tree

TheoremPreferred paths permute the vertex list#✓fully proved

For every list of preferred edges, the downward preferred path of a tree followed by the concatenation of the other paths of its preferred-path decomposition is a permutation of the vertex list of the tree.

public theorem decomp_perm (edges : List (V × V)) (t : Tree V) :
    ((decomp edges t).1 ++ (decomp edges t).2.flatMap id).Perm
      (Tree.vertices t)

Uses 6 · Used by 1

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Preferred-path decomposition of a tree

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a node

Used byThe preferred paths of a tree rearrange its vertex list

TheoremThe preferred paths of a tree rearrange its vertex list#✓fully proved

For every list \(E\) of directed edges and every rooted ordered tree \(t\), the concatenation of the preferred paths of \(t\) under \(E\) is a permutation of the preorder vertex list of \(t\).

public theorem perm_treePaths_flatMap (edges : List (V × V)) (t : Tree V) :
    ((treePaths edges t).flatMap id).Perm (Tree.vertices t)

Uses 5 · Used by 2

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

Proof usesPreferred-path decomposition of a tree · Preferred paths permute the vertex list

Used byPreferred paths cover exactly the vertices of the forest · Preferred paths cover each vertex at most once

TheoremDecomposition paths are paths of the tree#✓fully proved

For every list of preferred edges, in the preferred-path decomposition of a tree \(T\), the downward preferred path and every other path are paths of \(T\): any two consecutive vertices are joined by a parent-child edge of \(T\), in either direction.

public theorem decomp_isChain (edges : List (V × V)) (t : Tree V) :
    (decomp edges t).1.IsChain (fun a b => Adjacent a b t) ∧
      ∀ p ∈ (decomp edges t).2, p.IsChain (fun a b => Adjacent a b t)

Uses 7 · Used by 1

Statement usesRooted ordered tree · Adjacency in a rooted tree · Preferred-path decomposition of a tree

Proof usesInduction principle for rooted trees · Root of a rooted tree · The downward preferred path starts at the root · Preferred paths of a tree

Used byPreferred paths of a tree follow tree edges

TheoremPreferred paths of a tree follow tree edges#✓fully proved

Let \(t\) be a tree and \(E\) any list of pairs of vertices, read as preferred (parent, child) edges. For every path \(p = (p_0, \dots, p_k)\) in the preferred-path decomposition of \(t\) under \(E\) and every \(i < k\), the vertices \(p_i\) and \(p_{i+1}\) are adjacent in \(t\), that is, joined by a parent-child edge of \(t\) in one direction or the other.

public theorem isChain_of_mem_treePaths {edges : List (V × V)} {t : Tree V}
    {p : List V} (hp : p ∈ treePaths edges t) :
    p.IsChain (fun a b => Adjacent a b t)

Uses 5 · Used by 1

Statement usesRooted ordered tree · Adjacency in a rooted tree · Preferred paths of a tree

Proof usesPreferred-path decomposition of a tree · Decomposition paths are paths of the tree

Used byPreferred paths of a link-cut tree state follow represented edges

TheoremAccess edges make the root path the downward preferred path#✓fully proved

Let \(T\) be a tree whose vertex list is duplicate-free, let \(x\) be a vertex of \(T\) with root path \(p\) (the path from the root of \(T\) down to \(x\)), and let \(E\) be a list of directed edges such that every consecutive pair of \(p\), parent first, lies in \(E\), and every edge of \(E\) whose first vertex lies on \(p\) is such a consecutive pair. Then the downward preferred path of the preferred-path decomposition of \(T\) under \(E\) is \(p\).

public theorem decomp_fst_eq_rootPath {x : V} {E : List (V × V)} :
    ∀ {t : Tree V} {p : List V}, (Tree.vertices t).Nodup →
      rootPath x t = some p →
      (∀ e ∈ pathEdges p, e ∈ E) →
      (∀ e ∈ E, e.1 ∈ p → e ∈ pathEdges p) →
      (decomp E t).1 = p

Uses 11 · Used by 1

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Preferred-path decomposition of a tree · Consecutive edges of a vertex path · Root-to-vertex path

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a node · A root path ends at its target · The root path starts at the root · Root paths have distinct vertices

Used byAfter access, the accessed vertex ends its preferred path

StructureLink-cut tree state#✓fully proved

A state of a link-cut tree over a vertex type \(V\) consists of the represented forest, a list of rooted ordered trees with vertices in \(V\), and a list of preferred (solid) edges, each a pair \((u, v)\) of vertices meant as the edge from a node \(u\) to its preferred child \(v\) in the represented forest; the structure itself does not require these pairs to be edges of the forest. The preferred-path decomposition is derived from the preferred edges as the maximal solid chains in each represented tree. With no preferred edges, every edge is dashed and every vertex is its own singleton path.

public structure State (V : Type u) where
  /-- The represented forest. -/
  forest : List (Tree V)
  /-- The preferred edges, as `(parent, child)` pairs. -/
  preferred : List (V × V)

Uses 1 · Used by 34

Statement usesRooted ordered tree

Used byAccess in a link-cut tree · Access preserves validity · Access leaves the represented forest unchanged · After access, the accessed vertex ends its preferred path · An edge cut keeps every other 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 paths of a link-cut tree state follow represented edges · 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 · Preferred paths cover exactly the vertices of the forest · Access keeps off-path preferred edges · Access makes the root path preferred · Preferred paths have distinct vertices · Preferred paths cover each vertex at most once · A cut disconnects a vertex from everything outside its subtree · Cutting an edge separates its endpoints · Preferred paths are pairwise vertex-disjoint · Preferred-path decomposition of a link-cut tree state · Valid link-cut tree states · Validity of states with no preferred edges

State

DefinitionVertex of a link-cut tree state#✓fully proved

A vertex \(x\) belongs to a link-cut tree state \(s\) when \(x\) is a vertex of some tree of the represented forest of \(s\).

public def Mem (s : State V) (x : V) : Prop :=
  ∃ t ∈ s.forest, x ∈ Tree.vertices t

Uses 3 · Used by 7

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Link-cut tree state

Used byAfter access, the accessed vertex ends its preferred path · An edge cut keeps every other edge · Linking connects the endpoints · Making a vertex the root keeps its connections · Making a vertex the root installs a tree rooted there · Both sides of a cut remain in the forest · Cutting an edge separates its endpoints

DefinitionConnectivity in a link-cut tree state#✓fully proved

Two vertices \(x\) and \(y\) are connected in a link-cut tree state \(s\) when some tree of the represented forest of \(s\) has both \(x\) and \(y\) among its vertices.

Connectivity is the abstraction against which the link-cut tree operations are specified.

public def Connected (s : State V) (x y : V) : Prop :=
  ∃ t ∈ s.forest, x ∈ Tree.vertices t ∧ y ∈ Tree.vertices t

Uses 3 · Used by 5

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Link-cut tree state

Used byConnectivity via Euler tours · Linking connects the endpoints · Making a vertex the root keeps its connections · A cut disconnects a vertex from everything outside its subtree · Cutting an edge separates its endpoints

TheoremConnectivity via Euler tours#✓fully proved

For a link-cut tree state \(s\) and vertices \(x\) and \(y\), \(x\) and \(y\) are connected in \(s\) if and only if some tree of the represented forest of \(s\) contains both \(x\) and \(y\) in its Euler tour.

public theorem connected_iff_tour {x y : V} :
    s.Connected x y ↔ ∃ t ∈ s.forest, x ∈ Tree.tour t ∧ y ∈ Tree.tour t

Uses 6

Statement usesRooted ordered tree · Euler tour · Link-cut tree state · Connectivity in a link-cut tree state

Proof usesThe Euler tour visits exactly the vertices of the tree · Preorder vertex list of a rooted tree

DefinitionValid link-cut tree states#✓fully proved

A link-cut tree state \(s\) is valid when four conditions hold: the concatenation of the vertex lists of the trees of its represented forest has no duplicates (so the trees are vertex-disjoint); its list of preferred edges has no duplicates; every preferred edge \((a, b)\) is a parent-child edge of some tree of the represented forest, with \(a\) the parent of \(b\); and any two preferred edges with the same parent are equal, so each vertex has at most one preferred child.

The duplicate-free vertex condition also pins down the parent of each vertex, so the maximal chains of preferred edges in each tree are genuine disjoint paths.

public def Valid (s : State V) : Prop :=
  (s.forest.flatMap Tree.vertices).Nodup ∧
    s.preferred.Nodup ∧
    (∀ e ∈ s.preferred, ∃ t ∈ s.forest, ParentChild e.1 e.2 t) ∧
    (∀ e₁ ∈ s.preferred, ∀ e₂ ∈ s.preferred, e₁.1 = e₂.1 → e₁ = e₂)

Uses 4 · Used by 13

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Parent-child relation in a rooted tree · Link-cut tree state

Used byAccess preserves validity · After access, the accessed vertex ends its preferred path · An edge cut keeps every other edge · Making a vertex the root keeps its connections · Cutting preserves validity · Edge cutting preserves validity · Linking in a link-cut tree preserves validity · Rerooting a link-cut tree state preserves validity · Preferred paths have distinct vertices · Preferred paths cover each vertex at most once · Cutting an edge separates its endpoints · Preferred paths are pairwise vertex-disjoint · Validity of states with no preferred edges

TheoremValidity of states with no preferred edges#✓fully proved

Let \(s\) be a link-cut tree state whose list of preferred edges is empty. If the concatenation of the vertex lists of the trees of the represented forest of \(s\) has no duplicates, then \(s\) is valid.

This is the situation after every structural operation, which resets all edges to dashed.

public theorem valid_of_preferred_nil (hpre : s.preferred = [])
    (h : (s.forest.flatMap Tree.vertices).Nodup) : s.Valid

Uses 5 · Used by 4

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Link-cut tree state · Valid link-cut tree states

Proof usesParent-child relation in a rooted tree

Used byCutting preserves validity · Edge cutting preserves validity · Linking in a link-cut tree preserves validity · Rerooting a link-cut tree state preserves validity

DefinitionPreferred-path decomposition of a link-cut tree state#✓fully proved

For a link-cut tree state \(s\), its preferred paths are obtained by taking, for each represented tree of \(s\) in forest order, the preferred paths of that tree under the preferred edges of \(s\), and concatenating these lists. Within a tree these are its maximal chains of preferred edges when each vertex has at most one preferred child, each listed from its shallowest to its deepest vertex; a vertex incident to no preferred edge forms a singleton path.

The decomposition keeps the preferred paths of every subtree, not one distinguished path, so an access changes only the preferred edges leaving vertices of the accessed root path.

public def paths (s : State V) : List (List V) :=
  s.forest.flatMap (treePaths s.preferred)

Uses 3 · Used by 6

Statement usesRooted ordered tree · Link-cut tree state · Preferred paths of a tree

Used byAfter access, the accessed vertex ends its preferred path · Preferred paths of a link-cut tree state follow represented edges · Preferred paths cover exactly the vertices of the forest · Preferred paths have distinct vertices · Preferred paths cover each vertex at most once · Preferred paths are pairwise vertex-disjoint

TheoremPreferred paths cover exactly the vertices of the forest#✓fully proved

For every link-cut tree state \(s\) and every vertex \(v\), \(v\) lies on some path of the preferred-path decomposition of \(s\) if and only if \(v\) is a vertex of some tree of the represented forest of \(s\). No validity hypothesis on \(s\) is needed.

public theorem mem_paths_flatMap {v : V} :
    v ∈ (paths s).flatMap id ↔ v ∈ s.forest.flatMap Tree.vertices

Uses 6

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Link-cut tree state · Preferred-path decomposition of a link-cut tree state

Proof usesThe preferred paths of a tree rearrange its vertex list · Preferred paths of a tree

TheoremPreferred paths cover each vertex at most once#✓fully proved

In a valid link-cut tree state, the concatenation of all preferred paths of the decomposition has no repeated vertex: no vertex occurs twice on one path or on two different paths.

Together with the fact that every vertex of the represented forest lies on some preferred path, the preferred paths partition the vertex set.

public theorem nodup_paths_flatMap (hs : s.Valid) :
    ((paths s).flatMap id).Nodup

Uses 8 · Used by 2

Statement usesLink-cut tree state · Valid link-cut tree states · Preferred-path decomposition of a link-cut tree state

Proof usesRooted ordered tree · Preorder vertex list of a rooted tree · Parent-child relation in a rooted tree · The preferred paths of a tree rearrange its vertex list · Preferred paths of a tree

Used byPreferred paths have distinct vertices · Preferred paths are pairwise vertex-disjoint

TheoremPreferred paths are pairwise vertex-disjoint#✓fully proved

In a valid link-cut tree state, any two preferred paths at different positions of the preferred-path decomposition have no vertex in common.

public theorem pairwise_disjoint_paths (hs : s.Valid) :
    (paths s).Pairwise List.Disjoint

Uses 4

Statement usesLink-cut tree state · Valid link-cut tree states · Preferred-path decomposition of a link-cut tree state

Proof usesPreferred paths cover each vertex at most once

TheoremPreferred paths have distinct vertices#✓fully proved

Every preferred path of a valid state has distinct vertices.

public theorem nodup_of_mem_paths {p : List V} (hs : s.Valid)
    (hp : p ∈ paths s) : p.Nodup

Uses 4

Statement usesLink-cut tree state · Valid link-cut tree states · Preferred-path decomposition of a link-cut tree state

Proof usesPreferred paths cover each vertex at most once

TheoremPreferred paths of a link-cut tree state follow represented edges#✓fully proved

Let \(s\) be a link-cut tree state. For every path \(p = (p_0, \dots, p_k)\) in the preferred-path decomposition of \(s\) and every \(i < k\), some represented tree of \(s\) has \(p_i\) and \(p_{i+1}\) adjacent, that is, joined by a parent-child edge in one direction or the other.

This holds for every state, with no validity hypothesis.

public theorem isChain_of_mem_paths {p : List V} (hp : p ∈ paths s) :
    p.IsChain (fun a b => ∃ t ∈ s.forest, Adjacent a b t)

Uses 6

Statement usesRooted ordered tree · Adjacency in a rooted tree · Link-cut tree state · Preferred-path decomposition of a link-cut tree state

Proof usesPreferred paths of a tree follow tree edges · Preferred paths of a tree

DefinitionAccess in a link-cut tree#✓fully proved

Let \(s\) be a link-cut tree state and \(x\) a vertex. If \(x\) is a vertex of some tree of the represented forest of \(s\), let \(T\) be the first such tree and let \(p\) be the path in \(T\) from its root down to \(x\). Accessing \(x\) keeps the represented forest and replaces the preferred edges by those preferred edges of \(s\) whose parent endpoint is not on \(p\), followed by the edges of \(p\), each directed from parent to child. If \(x\) is not a vertex of the represented forest, accessing \(x\) leaves \(s\) unchanged.

Thus every edge of the root-to-\(x\) path becomes preferred, the previously preferred child edges of the vertices on that path are dropped, and preferred edges hanging off the path survive: in the tree with root \(1\), whose children are \(2\) and \(3\), where \(4\) is a child of \(2\) and \(5\) a child of \(3\), accessing \(5\) after accessing \(4\) keeps the preferred path \([2, 4]\), since the edge from \(2\) to \(4\) has its parent endpoint off the path \(1, 3, 5\).

public def access (x : V) (s : State V) : State V :=
  match findTree x s.forest with
  | some t =>
      match rootPath x t with
      | some p =>
          ⟨s.forest,
            (s.preferred.filter (fun e => e.1 ∉ p)) ++ pathEdges p⟩
      | none => s
  | none => s

Uses 5 · Used by 5

Statement usesRooted ordered tree · Link-cut tree state · Tree of a forest containing a vertex · Consecutive edges of a vertex path · Root-to-vertex path

Used byAccess preserves validity · Access leaves the represented forest unchanged · After access, the accessed vertex ends its preferred path · Access keeps off-path preferred edges · Access makes the root path preferred

TheoremAccess keeps off-path preferred edges#✓fully proved

Let \(s\) be a link-cut tree state, \(x\) a vertex, and \((u, w)\) a preferred edge of \(s\), directed from the parent \(u\) to the child \(w\). Suppose that, if some tree of the represented forest of \(s\) contains \(x\), then \(u\) does not lie on the path in the first such tree from its root down to the first occurrence of \(x\) in preorder. Then \((u, w)\) is still a preferred edge after accessing \(x\).

This is the edge-level fact behind the persistence of off-path preferred paths across accesses.

public theorem mem_preferred_access {x : V} {e : V × V}
    (he : e ∈ s.preferred)
    (h : ∀ t p, findTree x s.forest = some t → rootPath x t = some p →
      e.1 ∉ p) :
    e ∈ (access x s).preferred

Uses 6

Statement usesRooted ordered tree · Link-cut tree state · Access in a link-cut tree · Tree of a forest containing a vertex · Root-to-vertex path

Proof usesConsecutive edges of a vertex path

TheoremAccess makes the root path preferred#✓fully proved

Let \(s\) be a link-cut tree state and \(x\) a vertex, let \(t\) be the first tree of the represented forest of \(s\) that contains \(x\), and let \(p\) be the path in \(t\) from the root down to the first occurrence of \(x\) in preorder. Then every edge of \(p\), taken as the pair (parent, child) of consecutive vertices of \(p\), is a preferred edge of the state obtained from \(s\) by accessing \(x\).

public theorem mem_preferred_access_of_mem_pathEdges {x : V} {t : Tree V}
    {p : List V} {e : V × V} (hft : findTree x s.forest = some t)
    (hrp : rootPath x t = some p) (he : e ∈ pathEdges p) :
    e ∈ (access x s).preferred

Uses 6

Statement usesRooted ordered tree · Link-cut tree state · Access in a link-cut tree · Tree of a forest containing a vertex · Consecutive edges of a vertex path · Root-to-vertex path

TheoremAccess leaves the represented forest unchanged#✓fully proved

For every link-cut tree state \(s\) and every vertex \(x\), accessing \(x\) changes only the preferred edges: the represented forest of the resulting state equals the represented forest of \(s\).

public theorem access_forest (x : V) : (access x s).forest = s.forest

Uses 6

Statement usesRooted ordered tree · Link-cut tree state · Access in a link-cut tree

Proof usesTree of a forest containing a vertex · Consecutive edges of a vertex path · Root-to-vertex path

TheoremAfter access, the accessed vertex ends its preferred path#✓fully proved

Let \(s\) be a valid link-cut tree state and let \(x\) be a vertex of its represented forest. Then, after accessing \(x\), the preferred-path decomposition of the new state contains a path \(p\) whose last vertex is \(x\), and \(p\) is the path from the root down to \(x\) in some tree of the represented forest of \(s\).

Paths are listed from the root downward, so \(x\) is the deepest vertex of \(p\). No auxiliary splay tree is modeled, so this is only the endpoint property of the accessed preferred path.

public theorem access_last {x : V} (hs : s.Valid) (hx : s.Mem x) :
    ∃ p ∈ paths (access x s), p.getLast? = some x ∧
      ∃ t ∈ s.forest, rootPath x t = some p

Uses 17

Statement usesRooted ordered tree · Link-cut tree state · Vertex of a link-cut tree state · Valid link-cut tree states · Access in a link-cut tree · Preferred-path decomposition of a link-cut tree state · Root-to-vertex path

Proof usesInduction principle for rooted trees · Preorder vertex list of a rooted tree · Preorder vertex list of a node · Parent-child relation in a rooted tree · Preferred-path decomposition of a tree · Access edges make the root path the downward preferred path · Tree of a forest containing a vertex · A root path ends at its target · Consecutive edges of a vertex path · Preferred paths of a tree

TheoremAccess preserves validity#✓fully proved

If a link-cut tree state \(s\) is valid, then for every vertex \(x\) the state obtained from \(s\) by accessing \(x\) is again valid.

The new preferred edges are the retained off-path edges together with the edges of the accessed root path; the two groups have disjoint parent endpoints (off versus on the path), so duplicate-freeness and the at-most-one-preferred-child condition carry over.

public theorem Valid.access {x : V} (hs : s.Valid) : (State.access x s).Valid

Uses 11

Statement usesLink-cut tree state · Valid link-cut tree states · Access in a link-cut tree

Proof usesRooted ordered tree · Preorder vertex list of a rooted tree · Parent-child relation in a rooted tree · Tree of a forest containing a vertex · A root path follows parent-child edges downward · Root paths have distinct vertices · Consecutive edges of a vertex path · Root-to-vertex path

DefinitionMaking a vertex the root in a link-cut tree state#✓fully proved

Given a vertex \(x\) and a state \(s\), the state \(\operatorname{makeRoot}(x, s)\) has no preferred edges (all edges dashed), and its forest is defined as follows. If \(x\) is not a vertex of the forest, the forest is unchanged. Otherwise the first represented tree containing \(x\) is rerooted at \(x\): the edges on the path from its old root to \(x\) are reversed, and when the tree has distinct vertices every undirected edge is kept. The rerooted tree replaces every tree containing \(x\) and is placed at the end of the forest.

public def makeRoot (x : V) (s : State V) : State V :=
  { s with
    preferred := []
    forest :=
      match findTree x s.forest with
      | some t =>
          match rerootAt x t with
          | some t' => removeTree x s.forest ++ [t']
          | none => s.forest
      | none => s.forest }

Uses 5 · Used by 9

Statement usesRooted ordered tree · Link-cut tree state · Tree of a forest containing a vertex · Removing the trees that contain a vertex · Rerooting a tree at a vertex

Used byAn edge cut keeps every other edge · Making a vertex the root keeps its connections · 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 · Rerooting a link-cut tree state preserves validity · Making a vertex the root installs a tree rooted there · Cutting an edge separates its endpoints

TheoremMaking a vertex the root installs a tree rooted there#✓fully proved

Let \(s\) be a link-cut tree state and \(x\) a vertex of its represented forest. After making \(x\) the root, some represented tree has root \(x\) and contains \(x\) as a vertex.

That tree is the rerooted old tree of \(x\).

public theorem makeRoot_root {x : V} (hx : s.Mem x) :
    ∃ t ∈ (makeRoot x s).forest, t.root = x ∧ x ∈ Tree.vertices t

Uses 16

Statement usesRooted ordered tree · Root of a rooted tree · Preorder vertex list of a rooted tree · Link-cut tree state · Vertex of a link-cut tree state · Making a vertex the root in a link-cut tree state

Proof usesInduction principle for rooted trees · Preorder vertex list of a node · Tree of a forest containing a vertex · Grafting a tree below a vertex · Vertices after grafting · Rerooting preserves the vertex set · Removing the trees that contain a vertex · Rerooting a tree at a vertex · Rerooting fails at an absent vertex · Grafting keeps the root

TheoremMaking a vertex the root keeps its connections#✓fully proved

Let \(s\) be a valid link-cut tree state and let \(x\) and \(y\) be connected in \(s\). Then \(x\) and \(y\) are still connected in the state obtained from \(s\) by making \(x\) the root of its represented tree.

Rerooting spans the same vertex set as the old tree and keeps every undirected edge; vertex disjointness of the represented trees pins down which tree contains \(x\).

public theorem connected_makeRoot {x y : V} (hs : s.Valid)
    (h : s.Connected x y) : (makeRoot x s).Connected x y

Uses 19

Statement usesLink-cut tree state · Connectivity in a link-cut tree state · Valid link-cut tree states · Making a vertex the root in a link-cut tree state

Proof usesRooted ordered tree · Induction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a rooted tree · Preorder vertex list of a node · Parent-child relation in a rooted tree · Vertex of a link-cut tree state · Tree of a forest containing a vertex · Grafting a tree below a vertex · Vertices after grafting · Rerooting preserves the vertex set · Removing the trees that contain a vertex · Rerooting a tree at a vertex · Rerooting fails at an absent vertex · Grafting keeps the root

TheoremRerooting a link-cut tree state preserves validity#✓fully proved

For every valid link-cut tree state \(s\) and every vertex \(x\), the state obtained from \(s\) by making \(x\) the root of its represented tree is valid.

The new forest has the same flat vertex list as the old one up to permutation (the rerooted tree replaces its original), and the preferred edges are reset.

public theorem Valid.makeRoot {x : V} (hs : s.Valid) :
    (State.makeRoot x s).Valid

Uses 12 · Used by 3

Statement usesLink-cut tree state · Valid link-cut tree states · Making a vertex the root in a link-cut tree state

Proof usesRooted ordered tree · Preorder vertex list of a rooted tree · Parent-child relation in a rooted tree · Validity of states with no preferred edges · Tree of a forest containing a vertex · Removing the tree containing a vertex splits the forest's vertices · Rerooting preserves the vertices · Removing the trees that contain a vertex · Rerooting a tree at a vertex

Used byAn edge cut keeps every other edge · Edge cutting preserves validity · Cutting an edge separates its endpoints

DefinitionLinking two trees of a link-cut tree state#✓fully proved

Given vertices \(x\) and \(y\) and a state \(s\), the state \(\operatorname{link}(x, y, s)\) has no preferred edges (all edges dashed), and its forest is defined as follows. If \(x\) or \(y\) is not a vertex of the forest, the forest is unchanged. Otherwise let \(t_x\) and \(t_y\) be the first represented trees containing \(x\) and \(y\). If \(x\) is a vertex of \(t_y\), the forest is unchanged. Otherwise \(t_x\) is rerooted at \(x\) (the edges on its old root-to-\(x\) path are reversed, so \(x\) becomes its root), the result is attached as a new last child subtree of the first node labelled \(y\) in \(t_y\), which adds the edge from \(y\) to \(x\), and this joined tree replaces every tree containing \(x\) or \(y\), placed at the end of the forest.

Cslib.Algorithms.Lean.LinkCutTree.State.link · 15 lines

public def link (x y : V) (s : State V) : State V :=
  { s with
    preferred := []
    forest :=
      match findTree x s.forest, findTree y s.forest with
      | some tx, some ty =>
          if x ∈ Tree.vertices ty then s.forest
          else
            match rerootAt x tx with
            | some tx' =>
                match graftAt y tx' ty with
                | some tj => removeTree x (removeTree y s.forest) ++ [tj]
                | none => s.forest
            | none => s.forest
      | _, _ => s.forest }

Uses 7 · Used by 2

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Link-cut tree state · Tree of a forest containing a vertex · Grafting a tree below a vertex · Removing the trees that contain a vertex · Rerooting a tree at a vertex

Used byLinking connects the endpoints · Linking in a link-cut tree preserves validity

TheoremLinking connects the endpoints#✓fully proved

Let \(s\) be a link-cut tree state and let \(x\) and \(y\) be vertices of its represented forest. Then in the state obtained from \(s\) by linking \(x\) to \(y\), the vertices \(x\) and \(y\) are connected, that is, some represented tree contains both. No invariant on the state is needed.

public theorem connected_link {x y : V} (hx : s.Mem x) (hy : s.Mem y) :
    (link x y s).Connected x y

Uses 17

Statement usesLink-cut tree state · Connectivity in a link-cut tree state · Vertex of a link-cut tree state · Linking two trees of a link-cut tree state

Proof usesRooted ordered tree · Induction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a rooted tree · Preorder vertex list of a node · Tree of a forest containing a vertex · Grafting a tree below a vertex · Vertices after grafting · Rerooting preserves the vertex set · Removing the trees that contain a vertex · Rerooting a tree at a vertex · Rerooting fails at an absent vertex · Grafting keeps the root

TheoremLinking in a link-cut tree preserves validity#✓fully proved

For every valid link-cut tree state \(s\) and all vertices \(x\) and \(y\), the state obtained from \(s\) by linking \(x\) and \(y\) is valid.

The joined tree has the union of the two old vertex lists up to permutation (rerooting and grafting both permute), the rest of the forest is untouched, and the preferred edges are reset.

public theorem Valid.link {x y : V} (hs : s.Valid) :
    (State.link x y s).Valid

Uses 14

Statement usesLink-cut tree state · Valid link-cut tree states · Linking two trees of a link-cut tree state

Proof usesRooted ordered tree · Preorder vertex list of a rooted tree · Parent-child relation in a rooted tree · Validity of states with no preferred edges · Tree of a forest containing a vertex · Grafting a tree below a vertex · Removing the tree containing a vertex splits the forest's vertices · Grafting adds the new subtree's vertices · Rerooting preserves the vertices · Removing the trees that contain a vertex · Rerooting a tree at a vertex

DefinitionCutting off the subtree at a vertex#✓fully proved

Cutting at a vertex \(x\) resets the preferred edges of the state to the empty list and changes its forest as follows. If no tree of the forest contains \(x\), the forest is unchanged. Otherwise let \(T\) be the first tree containing \(x\) and \(S\) the first subtree of \(T\) rooted at \(x\) in preorder. Every tree containing \(x\) is removed from the forest, and two trees are appended at the end: first the remainder of \(T\) with every subtree rooted at \(x\) pruned off, then \(S\). When \(x\) is the root of \(T\) nothing remains, and only \(S\) is appended.

public def cut (x : V) (s : State V) : State V :=
  { s with
    preferred := []
    forest :=
      match findTree x s.forest with
      | some t =>
          match findSubtree x t with
          | some sub =>
              match pruneAt x t with
              | some rem => removeTree x s.forest ++ [rem, sub]
              | none => removeTree x s.forest ++ [sub]
          | none => s.forest
      | none => s.forest }

Uses 6 · Used by 9

Statement usesRooted ordered tree · Link-cut tree state · Subtree rooted at a vertex · Tree of a forest containing a vertex · Pruning the subtrees rooted at a vertex · Removing the trees that contain a vertex

Used byAn edge cut keeps every other edge · 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 · Both sides of a cut remain in the forest · A cut disconnects a vertex from everything outside its subtree · Cutting an edge separates its endpoints

TheoremA cut disconnects a vertex from everything outside its subtree#✓fully proved

Let \(s\) be a link-cut tree state, let \(t\) be the first tree of its represented forest containing the vertex \(x\), and let \(u\) be the first subtree of \(t\) in preorder whose root is \(x\). After cutting \(s\) at \(x\), the vertex \(x\) is not connected to any vertex \(y\) that is not a vertex of \(u\).

No invariant on the state is needed.

public theorem not_connected_cut {x y : V} {t sub : Tree V}
    (hft : findTree x s.forest = some t) (hsub : findSubtree x t = some sub)
    (hy : y ∉ Tree.vertices sub) :
    ¬ (cut x s).Connected x y

Uses 13 · Used by 1

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Link-cut tree state · Connectivity in a link-cut tree state · Cutting off the subtree at a vertex · Subtree rooted at a vertex · Tree of a forest containing a vertex

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a node · Vertices of a pruned tree · Pruning the subtrees rooted at a vertex · Removing the trees that contain a vertex

Used byCutting an edge separates its endpoints

TheoremBoth sides of a cut remain in the forest#✓fully proved

Let \(s\) be a link-cut tree state, let \(x\) and \(y\) be vertices, and let \(t\) be the first tree of the represented forest of \(s\) that contains \(x\). Suppose no vertex occurs twice in \(t\), and let \(T_x\) be the subtree of \(t\) rooted at \(x\). If \(y\) is a vertex of \(t\) but not of \(T_x\), then after cutting \(s\) at \(x\) both \(x\) and \(y\) are vertices of the represented forest.

public theorem mem_cut {x y : V} {t sub : Tree V}
    (hnodup : (Tree.vertices t).Nodup)
    (hft : findTree x s.forest = some t) (hsub : findSubtree x t = some sub)
    (hy : y ∈ Tree.vertices t) (hy' : y ∉ Tree.vertices sub) :
    (cut x s).Mem x ∧ (cut x s).Mem y

Uses 13

Statement usesRooted ordered tree · Preorder vertex list of a rooted tree · Link-cut tree state · Vertex of a link-cut tree state · Cutting off the subtree at a vertex · Subtree rooted at a vertex · Tree of a forest containing a vertex

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a node · Pruning keeps the vertices outside the detached subtree · Pruning the subtrees rooted at a vertex · Removing the trees that contain a vertex

TheoremCutting preserves validity#✓fully proved

If \(s\) is a valid link-cut tree state, then for every vertex \(x\) the state obtained from \(s\) by cutting off the subtree rooted at \(x\) is again valid.

Pruning splits the vertices of the cut tree into those of the remainder and those of the detached subtree, the rest of the forest is untouched, and the preferred edges are reset.

public theorem Valid.cut {x : V} (hs : s.Valid) : (State.cut x s).Valid

Uses 13 · Used by 1

Statement usesLink-cut tree state · Valid link-cut tree states · Cutting off the subtree at a vertex

Proof usesRooted ordered tree · Preorder vertex list of a rooted tree · Parent-child relation in a rooted tree · Validity of states with no preferred edges · Subtree rooted at a vertex · Tree of a forest containing a vertex · Removing the tree containing a vertex splits the forest's vertices · Pruning a subtree splits the vertex list · Pruning the subtrees rooted at a vertex · Removing the trees that contain a vertex

Used byEdge cutting preserves validity

DefinitionCutting an edge of a link-cut tree#✓fully proved

For vertices \(x\) and \(y\) and a link-cut tree state \(s\), cutting the edge between \(x\) and \(y\) works as follows. If \(x\) and \(y\) are adjacent in some tree of the represented forest of \(s\), the result is obtained from \(s\) by first making \(x\) the root of its represented tree and then cutting off the subtree rooted at \(y\). Otherwise the represented forest is left unchanged. In both cases the list of preferred edges becomes empty.

When \(x\) and \(y\) are joined by an edge of a valid state, making \(x\) the root turns \(y\) into the root of a child subtree of \(x\), so the cut separates the two sides of the edge between \(x\) and \(y\) and keeps every other edge.

The adjacency test is necessary: without it the composite would cut at \(y\) regardless of \(x\). For instance, on the chain \(1 \to 2\) it would detach \(2\) when asked to cut the edge between \(99\) and \(2\), although there is no such edge.

public def cutEdge (x y : V) (s : State V) : State V :=
  if s.forest.any (adjacentB x y) then cut y (makeRoot x s)
  else { s with preferred := [] }

Uses 5 · Used by 5

Statement usesRooted ordered tree · Link-cut tree state · Cutting off the subtree at a vertex · Making a vertex the root in a link-cut tree state · Adjacency test

Used byAn edge cut keeps every other edge · Edge cutting preserves validity · Edge cut on an adjacent pair · Edge cut on a non-adjacent pair · Cutting an edge separates its endpoints

TheoremEdge cut on an adjacent pair#✓fully proved

Let \(s\) be a link-cut tree state and let \(x\) and \(y\) be adjacent in some tree of the represented forest of \(s\). Then cutting the edge between \(x\) and \(y\) in \(s\) gives the same state as first making \(x\) the root of its represented tree and then cutting off the subtree rooted at \(y\).

public theorem cutEdge_eq_cut_makeRoot_of_adjacent {x y : V}
    (hadj : ∃ t ∈ s.forest, Adjacent x y t) :
    cutEdge x y s = cut y (makeRoot x s)

Uses 9 · Used by 2

Statement usesRooted ordered tree · Adjacency in a rooted tree · Link-cut tree state · Cutting off the subtree at a vertex · Cutting an edge of a link-cut tree · Making a vertex the root in a link-cut tree state

Proof usesInduction principle for rooted trees · Root of a rooted tree · Adjacency test

Used byAn edge cut keeps every other edge · Cutting an edge separates its endpoints

TheoremEdge cut on a non-adjacent pair#✓fully proved

Let \(s\) be a link-cut tree state and let \(x\) and \(y\) be adjacent in no tree of the represented forest of \(s\). Then cutting the edge between \(x\) and \(y\) in \(s\) leaves the represented forest unchanged and makes the list of preferred edges empty.

In particular, no other edge at \(y\) is cut.

public theorem cutEdge_eq_of_not_adjacent {x y : V}
    (hadj : ¬ ∃ t ∈ s.forest, Adjacent x y t) :
    cutEdge x y s = { s with preferred := [] }

Uses 9

Statement usesRooted ordered tree · Adjacency in a rooted tree · Link-cut tree state · Cutting an edge of a link-cut tree

Proof usesInduction principle for rooted trees · Root of a rooted tree · Cutting off the subtree at a vertex · Making a vertex the root in a link-cut tree state · Adjacency test

TheoremEdge cutting preserves validity#✓fully proved

If \(s\) is a valid link-cut tree state, then for all vertices \(x\) and \(y\) the state obtained from \(s\) by cutting the edge between \(x\) and \(y\) is again valid.

On an adjacent pair the edge cut makes \(x\) the root of its tree and then cuts off the subtree rooted at \(y\); otherwise it only resets the preferred edges.

public theorem Valid.cutEdge {x y : V} (hs : s.Valid) :
    (State.cutEdge x y s).Valid

Uses 12

Statement usesLink-cut tree state · Valid link-cut tree states · Cutting an edge of a link-cut tree

Proof usesRooted ordered tree · Preorder vertex list of a rooted tree · Parent-child relation in a rooted tree · Cutting preserves validity · Rerooting a link-cut tree state preserves validity · Cutting off the subtree at a vertex · Making a vertex the root in a link-cut tree state · Validity of states with no preferred edges · Adjacency test

TheoremCutting an edge separates its endpoints#✓fully proved

Let \(s\) be a valid link-cut tree state and let \(x\) and \(y\) be adjacent in some tree of the represented forest of \(s\). After the edge cut of \(x\) and \(y\) in \(s\), the vertices \(x\) and \(y\) are not connected: no represented tree contains both.

public theorem not_connected_cutEdge {x y : V} (hs : s.Valid)
    (hadj : ∃ t ∈ s.forest, Adjacent x y t) :
    ¬ (cutEdge x y s).Connected x y

Uses 30

Statement usesRooted ordered tree · Adjacency in a rooted tree · Link-cut tree state · Connectivity in a link-cut tree state · Valid link-cut tree states · Cutting an edge of a link-cut tree

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a rooted tree · Preorder vertex list of a node · The first endpoint of a tree edge is a vertex · The second endpoint of a tree edge is a vertex · Parent-child relation in a rooted tree · Vertex of a link-cut tree state · Rerooting a link-cut tree state preserves validity · Cutting off the subtree at a vertex · Edge cut on an adjacent pair · Making a vertex the root in a link-cut tree state · A cut disconnects a vertex from everything outside its subtree · Rerooting keeps every edge · Subtree rooted at a vertex · Tree of a forest containing a vertex · Grafting a tree below a vertex · Vertices after grafting · Rerooting preserves the vertex set · Rerooting preserves the vertices · Removing the trees that contain a vertex · Rerooting a tree at a vertex · Rerooting fails at an absent vertex · Grafting keeps the root

TheoremAn edge cut keeps every other edge#✓fully proved

Let \(s\) be a valid link-cut tree state and let \(x\) and \(y\) be adjacent in some tree of its represented forest. If \(a\) and \(b\) are adjacent in some tree of the represented forest of \(s\), and neither \(a = x\) and \(b = y\) nor \(a = y\) and \(b = x\), then \(a\) and \(b\) are adjacent in some tree of the represented forest obtained from \(s\) by cutting the edge between \(x\) and \(y\).

Edges of other trees pass through untouched; edges of the cut tree survive the rerooting at \(x\) and then lie on one side of the prune at \(y\), and the only edge crossing the prune is the edge between \(x\) and \(y\).

public theorem adjacent_cutEdge {x y a b : V} (hs : s.Valid)
    (hadj : ∃ t ∈ s.forest, Adjacent x y t)
    (hab : ∃ t ∈ s.forest, Adjacent a b t)
    (hxy : ¬ ((a = x ∧ b = y) ∨ (a = y ∧ b = x))) :
    ∃ t ∈ (cutEdge x y s).forest, Adjacent a b t

Uses 32

Statement usesRooted ordered tree · Adjacency in a rooted tree · Link-cut tree state · Valid link-cut tree states · Cutting an edge of a link-cut tree

Proof usesInduction principle for rooted trees · Root of a rooted tree · Preorder vertex list of a rooted tree · Preorder vertex list of a node · The first endpoint of a tree edge is a vertex · The second endpoint of a tree edge is a vertex · Adjacency in a tree is symmetric · Parent-child relation in a rooted tree · Vertex of a link-cut tree state · Rerooting a link-cut tree state preserves validity · Cutting off the subtree at a vertex · Edge cut on an adjacent pair · Making a vertex the root in a link-cut tree state · Pruning keeps surviving edges · Rerooting keeps every edge · Subtree rooted at a vertex · Tree of a forest containing a vertex · Grafting a tree below a vertex · Vertices after grafting · Rerooting preserves the vertex set · Pruning a subtree splits the vertex list · Rerooting preserves the vertices · Pruning the subtrees rooted at a vertex · Removing the trees that contain a vertex · Rerooting a tree at a vertex · Rerooting fails at an absent vertex · Grafting keeps the root

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.