Algebra of the LR lookahead buffer

These lemmas isolate the finite-control arithmetic used by the marked-input machine. They state that a refill implements exactly one logical shift of observe, including the final no-refill phase after the marker has entered the buffer.

@[simp]

theorem CF_grammar.LRk.Buffered.lastBuffer_observe {T : Type} (k : ℕ) (hk : 0 < k) (w : List T) : lastBuffer hk (observe k w) = w[k - 1]?

theorem CF_grammar.LRk.Buffered.shiftBuffer_observe_cons {T : Type} (k : ℕ) (hk : 0 < k) (a : T) (w : List T) : shiftBuffer hk (observe k (a :: w)) w[k - 1]? = observe k w

Appending the next unread physical symbol after shifting the observed head produces the observation of the remaining logical input.

theorem CF_grammar.LRk.Buffered.shiftBuffer_observe_cons_of_last_none {T : Type} (k : ℕ) (hk : 0 < k) (a : T) (w : List T) (hlast : lastBuffer hk (observe k (a :: w)) = none) : shiftBuffer hk (observe k (a :: w)) none = observe k w

If EOF is already visible at the back of the buffer, no physical refill is needed: padding with EOF still implements the same logical shift.

def CF_grammar.LRk.Buffered.unreadAfter {T : Type} (k : ℕ) (w : List T) : List (Option T)

Physical input still unread after preloading a k-symbol observation. If the word is shorter than the buffer, its marker has already been consumed; otherwise the suffix is embedded and followed by the fresh marker.

Equations

• CF_grammar.LRk.Buffered.unreadAfter k w = if k ≤ w.length then List.map some (List.drop k w) ++ [none] else []

theorem CF_grammar.LRk.Buffered.unreadAfter_cons_split {T : Type} (k : ℕ) (hk : 0 < k) (a : T) (w : List T) {b : T} (hlast : lastBuffer hk (observe k (a :: w)) = some b) : ∃ (x : Option T) (xs : List (Option T)), unreadAfter k (a :: w) = x :: xs ∧ xs = unreadAfter k w ∧ shiftBuffer hk (observe k (a :: w)) x = observe k w

While the old buffer still ends in a real terminal, the unread marked input has a head. Reading that head is exactly the refill required by shiftBuffer, and its tail is the unread input for the logical suffix.