Regular languages are LR(0)

Every regular language is generated by an LR(0) grammar, hence is an LR language.

The construction stays entirely inside this development's own grammars. In this repository a regular language is, by definition, one generated by a right-regular grammar (is_RG); the repository proves these coincide with the DFA languages (is_RG_iff_isRegular, built from RG_of_DFA / RG_language = M.accepts). Given a regular language we take the DFA M it equals and use the deterministic right-regular grammar RG_of_DFA M, whose generated language (RG_of_DFA_language) and reachable sentential forms (RG_of_DFA_derives_inv) are already established. We reinterpret that right-regular grammar as a context-free grammar via CF_grammar_of_RG (the rules are unchanged) and show it is LR(0).

Because the DFA is deterministic, every rightmost sentential form is w·q — terminals w followed by the single state-nonterminal reached after reading w — so the prefix already built determines the handle and rule with no lookahead. The reachable-form content is borrowed wholesale from the right-regular development; the only new ingredient is that a rightmost context-free step is a special case of a general one, so a rightmost derivation of the wrapped grammar is in particular a right-regular derivation.

Main results

• is_LRk_zero_of_isRegular — every regular language is LR(0)
• is_LR_of_is_RG — every regular language is an LR language
• RG_subclass_LR — RG ⊆ LR

List helpers

The inclusion

theorem is_LRk_zero_of_is_RG {T : Type} [Fintype T] {L : Language T} (h : is_RG L) : is_LRk 0 L

Every regular (right-regular-generated) language is generated by an LR(0) grammar.

theorem is_LR_of_is_RG {T : Type} [Fintype T] {L : Language T} (h : is_RG L) : is_LR L

Every regular language is an LR language.

theorem RG_subclass_LR {T : Type} [Fintype T] : RG ⊆ LR

The class of regular languages is contained in the class of LR languages.