Computation semantics of productive characteristic nonterminals

The PDA-to-CFG correctness theorem is stated for Mathlib's grammar and for leftmost derivations. The reduced LR grammar, however, records productivity using Langlib's grammar representation. This file bridges those interfaces and turns productivity of a characteristic nonterminal into an actual net-pop computation of the normalized empty-stack PDA.

theorem DPDA_to_LR.mathlib_derives_of_CF_derives {T : Type} [Fintype T] (g : CF_grammar T) {u v : List (symbol T g.nt)} (h : CF_derives g u v) : (mathlib_cfg_of_cfg g).Derives (lsSymbol_of_lssymbol u) (lsSymbol_of_lssymbol v)

Translate an arbitrary Langlib CFG derivation to the corresponding Mathlib CFG derivation. The library's language-equivalence theorem only exposes the special case starting at the initial nonterminal, so the general form is recorded here.

theorem DPDA_to_LR.characteristic_mathlib_derives_of_raw {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {u v : List (symbol T (rawCharacteristicGrammar M).nt)} (h : CF_derives (rawCharacteristicGrammar M) u v) : (mathlibCharacteristicGrammar M).Derives (lsSymbol_of_lssymbol u) (lsSymbol_of_lssymbol v)

A raw characteristic derivation is a derivation in the original Mathlib characteristic grammar.

theorem DPDA_to_LR.reaches_of_mathlib_derives_list {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q p : State M} {γ : List (StackSymbol M)} {w : List T} (hγ : ↑γ.length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (hderive : (mathlibCharacteristicGrammar M).Derives [Symbol.nonterminal (PDA_to_CFG.N.list q γ p)] (List.map Symbol.terminal w)) : PDA.Reaches { state := q, input := w, stack := γ } { state := p, input := [], stack := [] }

A terminal derivation of a characteristic list nonterminal realizes the net-pop computation encoded by that nonterminal.

theorem DPDA_to_LR.reaches_of_productive_list {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q p : State M} {γ : List (StackSymbol M)} (hγ : ↑γ.length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (hprod : productive (rawCharacteristicGrammar M) (PDA_to_CFG.N.list q γ p)) : ∃ (w : List T), PDA.Reaches { state := q, input := w, stack := γ } { state := p, input := [], stack := [] }

Productivity of a list nonterminal gives a concrete net-pop computation.

theorem DPDA_to_LR.reaches_of_productive_single {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q p : State M} {Z : StackSymbol M} (hprod : productive (rawCharacteristicGrammar M) (PDA_to_CFG.N.single q Z p)) : ∃ (w : List T), PDA.Reaches { state := q, input := w, stack := [Z] } { state := p, input := [], stack := [] }

Productivity of a single-symbol nonterminal gives its concrete net-pop computation. We reduce this to the existing correctness theorem for list nonterminals by adjoining the split rule and the empty-list rule.

theorem DPDA_to_LR.characteristic_rule_lhs_productive {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) : productive (rawCharacteristicGrammar M) r.1

Both sides of every retained characteristic rule are productive in the raw grammar.

theorem DPDA_to_LR.characteristic_rule_rhs_productive {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) {A : (characteristicGrammar M).nt} (hA : symbol.nonterminal A ∈ r.2) : productive (rawCharacteristicGrammar M) A