Deterministic pushdown automata have LR(1) grammars

The productive characteristic grammar of a normalized DPDA is LR(1). The normalization separates the first final-state visit from the remainder of a computation; exact active-spine synchronization then makes both visible introducing edges and empty returns unique with one symbol of lookahead.

theorem DPDA_to_LR.characteristicGrammar_isLR1 {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : (characteristicGrammar M).IsLRk 1

The productive characteristic grammar constructed from a DPDA is LR(1).

theorem is_LRk_one_of_is_DPDA {T : Type} [Fintype T] {L : Language T} (h : is_DPDA L) : is_LRk 1 L

Every language accepted by a DPDA is generated by an LR(1) grammar.

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

Consequently every DPDA language belongs to the existential finite-lookahead LR class.