CSG → LBA (Kuroda): completeness

This file proves the completeness half: a derivation [S] ⇒* w of the grammar is replayed in reverse by an accepting run of kMachine g₀ (kMachine_complete).

The core is applyRule_pass_gen, a single backward rule-application pass that rewrites one output-occurrence on the work track to the rule's input pattern patList, skipping blanks. The Complete section then repositions the head freely (sim_reaches), locates the rewrite window (list_split_filterMap), chains one pass per derivation step (step_back, derive_back) and finishes with the accept check.

applyRule single-pass steps

theorem KurodaConstruction.le_foldr_max (L : List ℕ) (x : ℕ) (hx : x ∈ L) : x ≤ List.foldr max 0 L

Every element of a ℕ-list is ≤ its foldr max 0.

theorem KurodaConstruction.output_length_le_ruleBound {T : Type} (g₀ : grammar T) (ri : Fin g₀.rules.length) : g₀.rules[ri].output_string.length ≤ ruleBound g₀

Each rule's output length is within ruleBound.

theorem KurodaConstruction.kStep_sim_applyRule {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (c : Fin (n + 1) → KCell g₀) (i : Fin (n + 1)) (ri : Fin g₀.rules.length) (l r : Bool) (ws : KWork g₀) (hc : c i = some (Sum.inr (l, r, ws))) : LBA.Step (kMachine g₀) { state := KState.sim, tape := { contents := c, head := i } } { state := KState.applyRule ri 0, tape := { contents := c, head := i } }

From sim, begin applying rule ri at the current cell (echo, stay).

theorem KurodaConstruction.kStep_applyRule_blank {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (c : Fin (n + 1) → KCell g₀) (i : Fin (n + 1)) (ri : Fin g₀.rules.length) (k : Fin (ruleBound g₀ + 1)) (l r : Bool) (hlt : ↑i < n) (hc : c i = some (Sum.inr (l, r, none))) (hr : r = false) : LBA.Step (kMachine g₀) { state := KState.applyRule ri k, tape := { contents := c, head := i } } { state := KState.applyRule ri k, tape := { contents := c, head := ⟨↑i + 1, ⋯⟩ } }

Skip a blank during the rule-application pass (echo, move right, keep the match position).

theorem KurodaConstruction.kStep_applyRule_continue {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (c : Fin (n + 1) → KCell g₀) (i : Fin (n + 1)) (ri : Fin g₀.rules.length) (k : Fin (ruleBound g₀ + 1)) (l r : Bool) (s : symbol T g₀.nt) (hlt : ↑i < n) (hc : c i = some (Sum.inr (l, r, some s))) (hm : g₀.rules[ri].output_string[↑k]? = some s) (hk : ↑k + 1 < g₀.rules[ri].output_string.length) (hr : r = false) : LBA.Step (kMachine g₀) { state := KState.applyRule ri k, tape := { contents := c, head := i } } { state := KState.applyRule ri (k + 1), tape := { contents := Function.update c i (some (Sum.inr (l, r, (patList g₀ g₀.rules[ri])[↑k]?))), head := ⟨↑i + 1, ⋯⟩ } }

Match the k-th output symbol and write the replacement, continuing the pass (k+1 < |out|).

theorem KurodaConstruction.kStep_applyRule_last {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (c : Fin (n + 1) → KCell g₀) (i : Fin (n + 1)) (ri : Fin g₀.rules.length) (k : Fin (ruleBound g₀ + 1)) (l r : Bool) (s : symbol T g₀.nt) (hlt : ↑i < n) (hc : c i = some (Sum.inr (l, r, some s))) (hm : g₀.rules[ri].output_string[↑k]? = some s) (hk : ↑k + 1 = g₀.rules[ri].output_string.length) : LBA.Step (kMachine g₀) { state := KState.applyRule ri k, tape := { contents := c, head := i } } { state := KState.sim, tape := { contents := Function.update c i (some (Sum.inr (l, r, (patList g₀ g₀.rules[ri])[↑k]?))), head := ⟨↑i + 1, ⋯⟩ } }

Match the last output symbol (k+1 = |out|); the replacement is written and the pass ends (return to sim).

theorem KurodaConstruction.kStep_applyRule_last_clamp {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (c : Fin (n + 1) → KCell g₀) (i : Fin (n + 1)) (ri : Fin g₀.rules.length) (k : Fin (ruleBound g₀ + 1)) (l r : Bool) (s : symbol T g₀.nt) (hin : ↑i = n) (hc : c i = some (Sum.inr (l, r, some s))) (hm : g₀.rules[ri].output_string[↑k]? = some s) (hk : ↑k + 1 = g₀.rules[ri].output_string.length) : LBA.Step (kMachine g₀) { state := KState.applyRule ri k, tape := { contents := c, head := i } } { state := KState.sim, tape := { contents := Function.update c i (some (Sum.inr (l, r, (patList g₀ g₀.rules[ri])[↑k]?))), head := i } }

Match the last output symbol when the cell is the rightmost (i.val = n); moving right clamps, so the head stays at n.

theorem KurodaConstruction.applyRule_pass {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (ri : Fin g₀.rules.length) (start : ℕ) (hq : start + g₀.rules[ri].output_string.length ≤ n + 1) (d : ℕ) (W : Fin (n + 1) → KWork g₀) (k : Fin (ruleBound g₀ + 1)) (hk : ↑k < g₀.rules[ri].output_string.length) : g₀.rules[ri].output_string.length - 1 - ↑k = d → (∀ (j : ℕ), ↑k ≤ j → ∀ (hj : j < g₀.rules[ri].output_string.length), W ⟨start + j, ⋯⟩ = some g₀.rules[ri].output_string[j]) → ∃ (h : Fin (n + 1)), LBA.Reaches (kMachine g₀) { state := KState.applyRule ri k, tape := { contents := fun (p : Fin (n + 1)) => mkCell g₀ p (W p), head := ⟨start + ↑k, ⋯⟩ } } { state := KState.sim, tape := { contents := fun (p : Fin (n + 1)) => mkCell g₀ p (if start + ↑k ≤ ↑p ∧ ↑p < start + g₀.rules[ri].output_string.length then (patList g₀ g₀.rules[ri])[↑p - start]? else W p), head := h } }

The rule-application pass (contiguous window). From applyRule ri k at cell start+k, where the window holds output_string[k..], scan to the end writing the replacement, reaching sim with the work function updated on [start+k, start+q) to patList[·]?.

theorem KurodaConstruction.applyRule_pass_gen {T : Type} [Fintype T] [DecidableEq T] (g₀ : grammar T) [Fintype g₀.nt] [DecidableEq g₀.nt] {n : ℕ} (ri : Fin g₀.rules.length) (v : List (symbol T g₀.nt)) (hpat : (patList g₀ g₀.rules[ri]).length ≤ g₀.rules[ri].output_string.length) (d : ℕ) (W : Fin (n + 1) → KWork g₀) (pos : ℕ) (hpn : pos < n + 1) (k : Fin (ruleBound g₀ + 1)) (_hk : ↑k < g₀.rules[ri].output_string.length) : n - pos = d → List.filterMap id (List.drop pos (List.ofFn W)) = List.drop (↑k) g₀.rules[ri].output_string ++ v → ∃ (W' : Fin (n + 1) → KWork g₀) (h : Fin (n + 1)), LBA.Reaches (kMachine g₀) { state := KState.applyRule ri k, tape := { contents := fun (p : Fin (n + 1)) => mkCell g₀ p (W p), head := ⟨pos, hpn⟩ } } { state := KState.sim, tape := { contents := fun (p : Fin (n + 1)) => mkCell g₀ p (W' p), head := h } } ∧ (∀ (p : Fin (n + 1)), ↑p < pos → W' p = W p) ∧ List.filterMap id (List.drop pos (List.ofFn W')) = List.drop (↑k) (patList g₀ g₀.rules[ri]) ++ v

The general rule-application pass (skips interspersed blanks). From applyRule ri k at cell pos, where the non-blank cells from pos begin with output_string[k..] followed by v, scan right (skipping blanks, matching each output symbol and writing the replacement) and reach sim with the work track's non-blank tail now patList[k..] ++ v, leaving cells < pos fixed.

Replaying a derivation backwards (completeness)

theorem KurodaConstruction.kStep_sim_right {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (W : Fin (n + 1) → KWork g₀) (i : Fin (n + 1)) (hlt : ↑i < n) : LBA.Step (kMachine g₀) { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := i } } { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := ⟨↑i + 1, ⋯⟩ } }

In sim, the head may move one cell right (the tape is unchanged).

theorem KurodaConstruction.kStep_sim_left {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (W : Fin (n + 1) → KWork g₀) (i : Fin (n + 1)) (hpos : 0 < ↑i) : LBA.Step (kMachine g₀) { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := i } } { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := ⟨↑i - 1, ⋯⟩ } }

In sim, the head may move one cell left (the tape is unchanged).

theorem KurodaConstruction.sim_reaches_zero {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (W : Fin (n + 1) → KWork g₀) (i : Fin (n + 1)) : LBA.Reaches (kMachine g₀) { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := i } } { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := 0 } }

From sim at any cell, reach sim at the left end (cell 0).

theorem KurodaConstruction.sim_zero_reaches {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (W : Fin (n + 1) → KWork g₀) (j : Fin (n + 1)) : LBA.Reaches (kMachine g₀) { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := 0 } } { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := j } }

From sim at the left end, reach sim at any cell j (sweep right).

theorem KurodaConstruction.sim_reaches {T : Type} [DecidableEq T] (g₀ : grammar T) [DecidableEq g₀.nt] {n : ℕ} (W : Fin (n + 1) → KWork g₀) (i j : Fin (n + 1)) : LBA.Reaches (kMachine g₀) { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := i } } { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := j } }

From sim, the head may be repositioned to any cell.

theorem KurodaConstruction.list_split_filterMap {α : Type u_1} (L : List (Option α)) (u z : List α) (h : List.filterMap id L = u ++ z) (hz : z ≠ []) : ∃ p < L.length, List.filterMap id (List.take p L) = u ∧ List.filterMap id (List.drop p L) = z

Locate a tape split point realizing a given prefix of the decoded form: if a list of work cells filters to u ++ z with z non-empty, some position p (a valid cell index) splits the tape with u to the left and z to the right.

theorem KurodaConstruction.step_back {T : Type} [Fintype T] [DecidableEq T] (g₀ : grammar T) [Fintype g₀.nt] [DecidableEq g₀.nt] {n : ℕ} (hnc : grammar_noncontracting g₀) (W : Fin (n + 1) → KWork g₀) (i : Fin (n + 1)) (r : grule T g₀.nt) (hr : r ∈ g₀.rules) (u v : List (symbol T g₀.nt)) (hform : formW g₀ W = u ++ r.output_string ++ v) : ∃ (W' : Fin (n + 1) → KWork g₀) (h : Fin (n + 1)), LBA.Reaches (kMachine g₀) { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := i } } { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W' k), head := h } } ∧ formW g₀ W' = u ++ patList g₀ r ++ v

One backward derivation step. If the work track decodes to u ++ output ++ v for some rule r (output non-empty by non-contraction), the simulator can reposition, run one backward applyRule pass, and arrive in sim with the track decoding to u ++ patList r ++ v — i.e. it undoes the forward step u ++ patList r ++ v ⇒ u ++ output ++ v.

theorem KurodaConstruction.derive_back {T : Type} [Fintype T] [DecidableEq T] (g₀ : grammar T) [Fintype g₀.nt] [DecidableEq g₀.nt] {n : ℕ} (hnc : grammar_noncontracting g₀) {β γ : List (symbol T g₀.nt)} (hd : grammar_derives g₀ β γ) (W : Fin (n + 1) → KWork g₀) (i : Fin (n + 1)) (hform : formW g₀ W = γ) : ∃ (W' : Fin (n + 1) → KWork g₀) (h : Fin (n + 1)), LBA.Reaches (kMachine g₀) { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W k), head := i } } { state := KState.sim, tape := { contents := fun (k : Fin (n + 1)) => mkCell g₀ k (W' k), head := h } } ∧ formW g₀ W' = β

Replaying a whole derivation backwards. If β ⇒* γ and the work track decodes to γ, the simulator reaches sim with the track decoding to β.

theorem KurodaConstruction.filterMap_ofFn_singleton {α : Type u_1} {n : ℕ} (W : Fin (n + 1) → Option α) (s : α) (h : List.filterMap id (List.ofFn W) = [s]) : ∃ (j : Fin (n + 1)), W j = some s ∧ ∀ (k : Fin (n + 1)), k ≠ j → W k = none

If the work track decodes to a single symbol s, exactly one cell holds it (the rest blank).

theorem KurodaConstruction.kMachine_complete {T : Type} [Fintype T] [DecidableEq T] (g₀ : grammar T) [Fintype g₀.nt] [DecidableEq g₀.nt] (hnc : grammar_noncontracting g₀) (w : List T) : grammar_language g₀ w → LBA.LanguageViaEmbed (kMachine g₀) (fun (t : T) => some (Sum.inl t)) w

Completeness of the simulator. A derivation [S] ⇒* w is replayed in reverse on the tape (convert input, repeatedly bubble blanks and apply rules backward, then verify [S]), yielding an accepting run. Non-contraction keeps every sentential form within |w| cells.