@cite{kuhlmann-nivre-2006} @cite{kuhlmann-2013} Projection theory for dependency trees: BFS-based projection computation, interval/gap/block analysis, Prop-level Dominance (reflexive-transitive closure), and the bridge theorems connecting BFS membership to dominance.

Also contains the isProjective / isWellFormed predicates, which depend on projection infrastructure.

References: @cite{kuhlmann-nivre-2006}, @cite{kuhlmann-2013}.

def DepGrammar.parentEdge (deps : List Dependency) (v w : ℕ) : Prop

Parent edge predicate: there is a head→dep dependency (v → w) in deps. The atomic relation whose reflexive-transitive closure is Dominates (defined below). Sites that need to express "v is a head with dep w" should use this rather than re-spelling the existential.

Equations

• DepGrammar.parentEdge deps v w = ∃ d ∈ deps, d.headIdx = v ∧ d.depIdx = w

def DepGrammar.projection (deps : List Dependency) (root : ℕ) : List ℕ

Projection π(i): the yield of node i — all nodes it transitively dominates, including itself — sorted in ascending order.

The projection is the central primitive of @cite{kuhlmann-nivre-2006} and @cite{kuhlmann-2013}. Projectivity, gap degree, block-degree, edge degree, and well-nestedness are all defined in terms of projections.

A dependency graph is projective iff every projection is an interval (@cite{kuhlmann-nivre-2006}, Definition 3).

Equations

• DepGrammar.projection deps root = (DepGrammar.projection.go deps [root] [] (deps.length * (deps.length + 1) + 2)).mergeSort fun (x1 x2 : ℕ) => decide (x1 ≤ x2)

def DepGrammar.projection.go (deps : List Dependency) (queue visited : List ℕ) (fuel : ℕ) : List ℕ

Equations

• One or more equations did not get rendered due to their size.
• DepGrammar.projection.go deps queue visited 0 = visited
• DepGrammar.projection.go deps [] visited fuel = visited

def DepGrammar.isInterval (sorted : List ℕ) : Bool

Whether a sorted list of positions forms an interval [min.max] with no internal gaps. A projection is an interval iff its node has gap degree 0.

Equations

• DepGrammar.isInterval [] = true
• DepGrammar.isInterval [head] = true
• DepGrammar.isInterval sorted = (sorted.getLast! - sorted.head! + 1 == sorted.length)

def DepGrammar.gaps (sorted : List ℕ) : List (ℕ × ℕ)

The gaps in a sorted projection: pairs (jₖ, jₖ₊₁) adjacent in the projection where jₖ₊₁ − jₖ > 1. (@cite{kuhlmann-nivre-2006}, Definition 6; @cite{kuhlmann-2013}, §7.1)

Equations

• DepGrammar.gaps sorted = List.filter (fun (x : ℕ × ℕ) => match x with | (a, b) => decide (b - a > 1)) (sorted.zip (List.drop 1 sorted))

def DepGrammar.blocks : List ℕ → List (List ℕ)

The blocks of a sorted projection: maximal contiguous segments.

Example: projection [1, 2, 5, 6, 7] → blocks [[1, 2], [5, 6, 7]]

The number of blocks equals gap degree + 1 and corresponds to the fan-out of the LCFRS rule extracted for that node.

Equations

• One or more equations did not get rendered due to their size.
• DepGrammar.blocks [] = []
• DepGrammar.blocks [a] = [[a]]

def DepGrammar.gapDegreeAt (deps : List Dependency) (root : ℕ) : ℕ

Gap degree of a node: number of gaps in its projection. (@cite{kuhlmann-nivre-2006}, Definition 6)

Equations

• DepGrammar.gapDegreeAt deps root = (DepGrammar.gaps (DepGrammar.projection deps root)).length

def DepGrammar.DepTree.gapDegree (t : DepTree) : ℕ

Gap degree of a tree: max gap degree over all nodes. (@cite{kuhlmann-nivre-2006}, Definition 7) Gap degree 0 ⟺ projective.

Equations

• t.gapDegree = List.foldl max 0 (List.map (DepGrammar.gapDegreeAt t.deps) (List.range t.words.length))

def DepGrammar.blockDegreeAt (deps : List Dependency) (root : ℕ) : ℕ

Block-degree of a node: number of blocks in its projection. Block-degree = gap degree + 1 = fan-out of extracted LCFRS rule.

Equations

• DepGrammar.blockDegreeAt deps root = (DepGrammar.blocks (DepGrammar.projection deps root)).length

def DepGrammar.DepTree.blockDegree (t : DepTree) : ℕ

Block-degree of a tree: max block-degree over all nodes. Block-degree 1 ⟺ projective. Bounded block-degree + well-nestedness ⟺ polynomial parsing (@cite{kuhlmann-2013}, Lemma 10).

Equations

• t.blockDegree = List.foldl max 0 (List.map (DepGrammar.blockDegreeAt t.deps) (List.range t.words.length))

theorem DepGrammar.projection_chain' (deps : List Dependency) (root : ℕ) : List.IsChain (fun (x1 x2 : ℕ) => x1 < x2) (projection deps root)

The output of projection is strictly increasing (sorted, no duplicates). Proof: BFS visits each node at most once (visited check), then mergeSort produces a sorted list. Since visited prevents duplicates, the sorted list is strictly increasing.

theorem DepGrammar.root_mem_projection (deps : List Dependency) (root : ℕ) : root ∈ projection deps root

root is always in its own projection.

theorem DepGrammar.projection_nonempty (deps : List Dependency) (root : ℕ) : projection deps root ≠ []

The output of projection is non-empty (root is always included).

theorem DepGrammar.projection_of_no_children (deps : List Dependency) (idx : ℕ) (h : List.filter (fun (d : Dependency) => d.headIdx == idx) deps = []) : projection deps idx = [idx]

Projection of a node with no outgoing edges is just [root].

Key step: BFS from root finds no children, so only root is visited. Used by leaf_no_subtree_members in HarmonicOrder.lean.

theorem DepGrammar.projection_nodup (deps : List Dependency) (root : ℕ) : (projection deps root).Nodup

The output of projection is a list with no duplicates. Follows from BFS visiting each node at most once (go_nodup), composed with the fact that mergeSort preserves the multiset (hence Nodup).

theorem DepGrammar.child_mem_projection (deps : List Dependency) (v w : ℕ) (hedge : parentEdge deps v w) : w ∈ projection deps v

If (v, w) is a dependency edge, then w ∈ projection deps v. Proof: BFS from v processes v first (adding children to queue), w is a child of v (by the edge), so w enters the queue and is processed.

theorem DepGrammar.chain_length_le_range (l : List ℕ) (lo hi : ℕ) (hchain : List.IsChain (fun (x1 x2 : ℕ) => x1 < x2) l) (hbounds : ∀ x ∈ l, lo < x ∧ x < hi) : l.length ≤ hi - lo - 1

A strictly increasing list of Nats with all elements in (lo, hi) has length ≤ hi - lo - 1. Proof: the head ≥ lo + 1, the last ≤ hi - 1, and chain_getLast_ge gives last ≥ head + (length - 1), so lo + 1 + (length - 1) ≤ hi - 1, giving length ≤ hi - lo - 1.

theorem DepGrammar.isInterval_iff_gaps_nil (ls : List ℕ) (h : List.IsChain (fun (x1 x2 : ℕ) => x1 < x2) ls) : isInterval ls = true ↔ gaps ls = []

For IsChain (· < ·) lists, isInterval = true ↔ gaps = [].

theorem DepGrammar.blocks_length_eq_gaps_length_succ (ls : List ℕ) (hne : ls ≠ []) (hc : List.IsChain (fun (x1 x2 : ℕ) => x1 < x2) ls) : (blocks ls).length = (gaps ls).length + 1

For non-empty strictly increasing lists, #blocks = #gaps + 1.

theorem DepGrammar.interval_mem_of_range (l : List ℕ) : l ≠ [] → List.IsChain (fun (x1 x2 : ℕ) => x1 < x2) l → isInterval l = true → ∀ (x : ℕ), l.head! ≤ x → x ≤ l.getLast! → x ∈ l

For a strictly increasing interval list, every integer in [head!, getLast!] is a member. Proof by induction: isInterval + chain forces consecutive elements (b = a + 1), so each integer in the range appears.

theorem DepGrammar.interval_mem_between (l : List ℕ) (hchain : List.IsChain (fun (x1 x2 : ℕ) => x1 < x2) l) (hint : isInterval l = true) (a b c : ℕ) (ha : a ∈ l) (hc : c ∈ l) (hab : a < b) (hbc : b < c) : b ∈ l

If a strictly increasing interval list contains a and c with a < b < c, then it contains b.

def DepGrammar.Dominates (deps : List Dependency) (v x : ℕ) : Prop

Prop-level dominance: Dominates deps v x iff v transitively dominates x via dependency edges (head → dep). Defined as the reflexive-transitive closure of parentEdge.

Equations

• DepGrammar.Dominates deps v x = Relation.ReflTransGen (DepGrammar.parentEdge deps) v x

theorem DepGrammar.Dominates_def {deps : List Dependency} {v x : ℕ} : Dominates deps v x ↔ Relation.ReflTransGen (parentEdge deps) v x

Unfolding bridge to mathlib's Relation.ReflTransGen for ad-hoc access to its lemma corpus (lift, mono, closed, etc.) without manual unfold.

theorem DepGrammar.Dominates.refl {deps : List Dependency} {v : ℕ} : Dominates deps v v

Reflexive case: v dominates itself.

theorem DepGrammar.Dominates.step {deps : List Dependency} {v w x : ℕ} (hedge : parentEdge deps v w) (h : Dominates deps w x) : Dominates deps v x

Head-style step: edge (v → w) plus dominance from w gives dominance from v.

theorem DepGrammar.Dominates.trans {deps : List Dependency} {u v w : ℕ} (huv : Dominates deps u v) (hvw : Dominates deps v w) : Dominates deps u w

Dominance is transitive.

theorem DepGrammar.Dominates.edge {deps : List Dependency} {v w : ℕ} (h : parentEdge deps v w) : Dominates deps v w

If there is a direct edge (v, w), then v dominates w.

theorem DepGrammar.Dominates.head_induction_on {deps : List Dependency} {x : ℕ} {motive : (v : ℕ) → Dominates deps v x → Prop} {v : ℕ} (h : Dominates deps v x) (refl : motive x ⋯) (step : ∀ {v w : ℕ} (hedge : parentEdge deps v w) (h_tail : Dominates deps w x), motive w h_tail → motive v ⋯) : motive v h

Head-style induction principle for Dominates: prove a property of Dominates deps v x (target x fixed) by handling the reflexive case motive x Dominates.refl and the head-step case parentEdge v w → Dominates w x → motive w → motive v.

Case binders are named refl and step to mirror the prior inductive's constructor names. The v and w arguments of step are implicit (use | @step v w hedge h_tail ih to bind, or obtain ⟨..⟩ := hedge).

theorem DepGrammar.dominates_of_mem_projection {deps : List Dependency} {v x : ℕ} (h : x ∈ projection deps v) : Dominates deps v x

Backward bridge: BFS membership implies dominance.

theorem DepGrammar.projection_closed_under_children (deps : List Dependency) (r w c : ℕ) (hw : w ∈ projection deps r) (hedge : parentEdge deps w c) : c ∈ projection deps r

Projection is closed under children: if w ∈ projection deps r and (w, c) is a dependency edge, then c ∈ projection deps r.

theorem DepGrammar.mem_projection_of_dominates {deps : List Dependency} {v x : ℕ} (h : Dominates deps v x) : x ∈ projection deps v

Forward bridge: dominance implies BFS membership.

theorem DepGrammar.dominates_iff_mem_projection (deps : List Dependency) (v x : ℕ) : Dominates deps v x ↔ x ∈ projection deps v

Bridge theorem: BFS projection membership ↔ Prop-level dominance.

theorem DepGrammar.foldl_max_ge_init (ls : List ℕ) (init : ℕ) : List.foldl max init ls ≥ init

foldl max init ls ≥ init.

theorem DepGrammar.foldl_max_ge_mem (ls : List ℕ) (init x : ℕ) (hx : x ∈ ls) : List.foldl max init ls ≥ x

foldl max init ls ≥ x for any x ∈ ls.

theorem DepGrammar.foldl_max_zero_iff (ls : List ℕ) : List.foldl max 0 ls = 0 ↔ ∀ x ∈ ls, x = 0

List.foldl max 0 ls = 0 iff every element of ls is 0.

theorem DepGrammar.foldl_max_pos_of_mem_pos (ls : List ℕ) (x : ℕ) (hx : x ∈ ls) (hpos : x > 0) : List.foldl max 0 ls > 0

If some element of ls is positive, then List.foldl max 0 ls > 0.

theorem DepGrammar.foldl_max_le_bound (ls : List ℕ) (init bound : ℕ) (hinit : init ≤ bound) (hall : ∀ x ∈ ls, x ≤ bound) : List.foldl max init ls ≤ bound

foldl max init ls ≤ bound when init ≤ bound and all elements ≤ bound.

theorem DepGrammar.foldl_max_const (ls : List ℕ) (k : ℕ) (hne : ls ≠ []) (hall : ∀ x ∈ ls, x = k) : List.foldl max 0 ls = k

foldl max 0 ls = k when all elements are k and the list is non-empty.

def DepGrammar.isProjective (t : DepTree) : Bool

Check projectivity: every node's projection is an interval. (@cite{kuhlmann-nivre-2006}, Definition 3)

Equivalent to: no two dependency arcs cross. Equivalent to: gap degree = 0. Equivalent to: block-degree = 1.

Equations

• DepGrammar.isProjective t = (List.range t.words.length).all fun (i : ℕ) => DepGrammar.isInterval (DepGrammar.projection t.deps i)

def DepGrammar.isWellFormed (t : DepTree) : Bool

A dependency tree is well-formed if it satisfies all constraints.

Equations

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