LR(k) grammars compile to deterministic pushdown automata

The concrete parser reads an explicit fresh endmarker. Correctness on marked words is proved at the automaton level, and the endmarker is then removed by deterministic-context-free closure under regular quotient and inverse injective renaming.

theorem CF_grammar.LRk.is_DPDA_CF_language_of_IsLRk {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hLR : G.IsLRk k) : is_DPDA (CF_language G)

Every LR(k) grammar language is deterministic context-free. The construction uses k+1 lookahead slots so it also covers k = 0.

theorem is_DPDA_of_is_LRk {T : Type} [Fintype T] {k : ℕ} {L : Language T} (h : is_LRk k L) : is_DPDA L

Exact language-class inclusion: every LR(k) language is accepted by a DPDA, for every finite k (including zero lookahead).

theorem is_DPDA_of_is_LR {T : Type} [Fintype T] {L : Language T} (h : is_LR L) : is_DPDA L

Consequently, every LR language (LR(k) for some finite k) is accepted by a DPDA.