Ancestors and graph distance on finite plane trees

The common ancestor of two addresses is their longest common prefix. The distance is the sum of their depths minus twice that ancestor's depth. The definitions are total on addresses; prefix closure ensures that the common ancestor of present vertices is present too.

Vertex t is only a name for the subtype of present addresses of t. Its metric is the real cast of the natural distance. No metric or topology instance is introduced on all addresses, and no separate graph representation is needed.

def BGW.PlaneTree.lca : List ℕ → List ℕ → List ℕ

The longest common address prefix, with the root represented by the empty list.

Equations

• BGW.PlaneTree.lca [] x✝ = []
• BGW.PlaneTree.lca x✝ [] = []
• BGW.PlaneTree.lca (a :: u) (b :: v) = if a = b then a :: BGW.PlaneTree.lca u v else []

@[simp]

theorem BGW.PlaneTree.lca_nil_left (u : List ℕ) : lca [] u = []

@[simp]

theorem BGW.PlaneTree.lca_nil_right (u : List ℕ) : lca u [] = []

theorem BGW.PlaneTree.prefix_lca_iff (w u v : List ℕ) : w <+: lca u v ↔ w <+: u ∧ w <+: v

An address is a prefix of the LCA exactly when it is a common prefix.

theorem BGW.PlaneTree.lca_prefix_left (u v : List ℕ) : lca u v <+: u

theorem BGW.PlaneTree.lca_prefix_right (u v : List ℕ) : lca u v <+: v

@[simp]

theorem BGW.PlaneTree.lca_self (u : List ℕ) : lca u u = u

theorem BGW.PlaneTree.lca_comm (u v : List ℕ) : lca u v = lca v u

theorem BGW.PlaneTree.lca_eq_left_iff (u v : List ℕ) : lca u v = u ↔ u <+: v

theorem BGW.PlaneTree.isVertex_lca {t : PlaneTree} {u v : List ℕ} (hu : t.IsVertex u) (_hv : t.IsVertex v) : t.IsVertex (lca u v)

The LCA of two present vertices remains a present vertex.

def BGW.PlaneTree.graphDist (u v : List ℕ) : ℕ

The natural parent-child distance between two addresses.

Equations

• BGW.PlaneTree.graphDist u v = u.length + v.length - 2 * (BGW.PlaneTree.lca u v).length

theorem BGW.PlaneTree.graphDist_add_two_lca (u v : List ℕ) : graphDist u v + 2 * (lca u v).length = u.length + v.length

The subtraction in graphDist never truncates a negative quantity.

theorem BGW.PlaneTree.graphDist_nonneg (u v : List ℕ) : 0 ≤ graphDist u v

@[simp]

theorem BGW.PlaneTree.graphDist_self (u : List ℕ) : graphDist u u = 0

theorem BGW.PlaneTree.graphDist_comm (u v : List ℕ) : graphDist u v = graphDist v u

@[simp]

theorem BGW.PlaneTree.graphDist_eq_zero_iff (u v : List ℕ) : graphDist u v = 0 ↔ u = v

theorem BGW.PlaneTree.graphDist_triangle (u v w : List ℕ) : graphDist u w ≤ graphDist u v + graphDist v w

@[simp]

theorem BGW.PlaneTree.graphDist_root (u : List ℕ) : graphDist [] u = u.length

@[simp]

theorem BGW.PlaneTree.graphDist_append_singleton (u : List ℕ) (j : ℕ) : graphDist u (u ++ [j]) = 1

Every parent-child edge has unit length.

theorem BGW.PlaneTree.isVertex_dropLast {t : PlaneTree} {u : List ℕ} (hu : t.IsVertex u) : t.IsVertex u.dropLast

Removing the last address entry gives a present parent, with the root fixed.

theorem BGW.PlaneTree.graphDist_dropLast (u : List ℕ) (hu : u ≠ []) : graphDist u.dropLast u = 1

def BGW.PlaneTree.Vertex (t : PlaneTree) : Type

Present addresses of a fixed tree; this is a subtype, not a second tree representation.

Equations

• t.Vertex = { u : List ℕ // t.IsVertex u }

@[instance_reducible]

noncomputable instance BGW.PlaneTree.vertexMetricSpace (t : PlaneTree) : MetricSpace t.Vertex

The metric on vertices is the real cast of their natural parent-child distance.

Equations

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

@[simp]

theorem BGW.PlaneTree.dist_vertex_eq_graphDist {t : PlaneTree} (u v : t.Vertex) : dist u v = ↑(graphDist ↑u ↑v)