Rule shapes in the DPDA characteristic grammar

The PDA-to-CFG conversion stores its finite rule set in a Finset, translates it to Langlib's list-based grammar, and then filters that list for fully productive rules. The lemmas here invert those representation layers and recover the five semantic rule forms of the characteristic grammar.

@[reducible, inline]

abbrev DPDA_to_LR.State {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Type

Equations

• DPDA_to_LR.State M = (Q × Bool ⊕ Fin 2)

@[reducible, inline]

abbrev DPDA_to_LR.StackSymbol {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Type

Equations

• DPDA_to_LR.StackSymbol M = Option S

@[reducible, inline]

abbrev DPDA_to_LR.Nonterminal {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : Type

Equations

• DPDA_to_LR.Nonterminal M = PDA_to_CFG.N (DPDA_to_LR.emptyStackPDA M)

def DPDA_to_LR.MathlibRuleShape {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (r : ContextFreeRule T (Nonterminal M)) : Prop

The five possible rule forms before translating Mathlib symbols.

Equations

• One or more equations did not get rendered due to their size.

theorem DPDA_to_LR.mathlibCharacteristicGrammar_rule_shape {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {r : ContextFreeRule T (Nonterminal M)} (hr : r ∈ (mathlibCharacteristicGrammar M).rules) : MathlibRuleShape M r

Invert membership in the finite rule set of Mathlib's characteristic grammar.

theorem DPDA_to_LR.mathlib_rule_of_characteristic_rule {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {r : (characteristicGrammar M).nt × List (symbol T (characteristicGrammar M).nt)} (hr : r ∈ (characteristicGrammar M).rules) : ∃ R ∈ (mathlibCharacteristicGrammar M).rules, r = (R.input, lssymbol_of_lsSymbol R.output)

A retained characteristic rule comes from a rule of Mathlib's characteristic grammar.

theorem DPDA_to_LR.characteristic_rule_fullyProductive {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {r : (characteristicGrammar M).nt × List (symbol T (characteristicGrammar M).nt)} (hr : r ∈ (characteristicGrammar M).rules) : fullyProductiveRule (rawCharacteristicGrammar M) r

Every retained rule is fully productive in the unfiltered characteristic grammar.

def DPDA_to_LR.RuleShape {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (r : (characteristicGrammar M).nt × List (symbol T (characteristicGrammar M).nt)) : Prop

The five possible rule forms after translating to Langlib symbols.

Equations

• One or more equations did not get rendered due to their size.

theorem DPDA_to_LR.characteristicGrammar_rule_shape {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {r : (characteristicGrammar M).nt × List (symbol T (characteristicGrammar M).nt)} (hr : r ∈ (characteristicGrammar M).rules) : RuleShape M r

Inverse rule-shape theorem for the reduced Langlib grammar.