Normal forms and uniqueness of list-introducing spine edges

Every occurrence of a characteristic list nonterminal in a rule right side is its final symbol. Consequently an Introduces witness for such a child is one of four exact forms: a reading move, an epsilon move, a stack split, or the grammar start rule. This file turns the history-sensitive parent-head theorem into equality of the complete introducing edges.

inductive DPDA_to_LR.ListIntroduction {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : List (symbol T (Nonterminal M)) → Nonterminal M → List T → List (symbol T (Nonterminal M)) → Nonterminal M → Nonterminal M × List (symbol T (Nonterminal M)) → Prop

Normal form of an introducing edge whose child is a characteristic list nonterminal.

• read {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {t : List T} {q target next : State M} {a : T} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (hparent : ActiveSpine M p (PDA_to_CFG.N.single q Z target) t) (htransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun q a Z) (hrule : (PDA_to_CFG.N.single q Z target, [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) : ListIntroduction M (p ++ [symbol.terminal a]) (PDA_to_CFG.N.list next gamma target) t p (PDA_to_CFG.N.single q Z target) (PDA_to_CFG.N.single q Z target, [symbol.terminal a, symbol.nonterminal (PDA_to_CFG.N.list next gamma target)])
• epsilon {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {t : List T} {q target next : State M} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (hparent : ActiveSpine M p (PDA_to_CFG.N.single q Z target) t) (htransition : (next, gamma) ∈ (emptyStackPDA M).transition_fun' q Z) (hrule : (PDA_to_CFG.N.single q Z target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)]) ∈ (characteristicGrammar M).rules) : ListIntroduction M p (PDA_to_CFG.N.list next gamma target) t p (PDA_to_CFG.N.single q Z target) (PDA_to_CFG.N.single q Z target, [symbol.nonterminal (PDA_to_CFG.N.list next gamma target)])
• split {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {t : List T} {q middle target : State M} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (hparent : ActiveSpine M p (PDA_to_CFG.N.list q (Z :: gamma) target) t) (hlength : ↑(Z :: gamma).length ≤ PDA_to_CFG.max_push (emptyStackPDA M)) (hrule : (PDA_to_CFG.N.list q (Z :: gamma) target, [symbol.nonterminal (PDA_to_CFG.N.single q Z middle), symbol.nonterminal (PDA_to_CFG.N.list middle gamma target)]) ∈ (characteristicGrammar M).rules) : ListIntroduction M (p ++ [symbol.nonterminal (PDA_to_CFG.N.single q Z middle)]) (PDA_to_CFG.N.list middle gamma target) t p (PDA_to_CFG.N.list q (Z :: gamma) target) (PDA_to_CFG.N.list q (Z :: gamma) target, [symbol.nonterminal (PDA_to_CFG.N.single q Z middle), symbol.nonterminal (PDA_to_CFG.N.list middle gamma target)])
• start {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] {M : DPDA Q T S} {p : List (symbol T (Nonterminal M))} {t : List T} {target : State M} (hparent : ActiveSpine M p PDA_to_CFG.N.start t) (hrule : (PDA_to_CFG.N.start, [symbol.nonterminal (PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target)]) ∈ (characteristicGrammar M).rules) : ListIntroduction M p (PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target) t p PDA_to_CFG.N.start (PDA_to_CFG.N.start, [symbol.nonterminal (PDA_to_CFG.N.list (emptyStackPDA M).initial_state [(emptyStackPDA M).start_symbol] target)])

theorem DPDA_to_LR.listIntroduction_of_introduces {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {childPrefix : List (symbol T (Nonterminal M))} {child : Nonterminal M} {childSuffix : List T} {parentPrefix : List (symbol T (Nonterminal M))} {parent : Nonterminal M} {rule : Nonterminal M × List (symbol T (Nonterminal M))} (hlist : IsListSymbol M (symbol.nonterminal child)) (h : Introduces M childPrefix child childSuffix parentPrefix parent rule) : ListIntroduction M childPrefix child childSuffix parentPrefix parent rule

Classification of an arbitrary Introduces witness whose child is a characteristic list nonterminal.

An equality-based view is more convenient when comparing two edges: its indices remain explicit hypotheses instead of being consumed by dependent pattern matching.

From head uniqueness to complete edge uniqueness

theorem DPDA_to_LR.emptyStack_read_epsilon_same_output_false {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {q p : State M} {a : T} {Z : StackSymbol M} {gamma : List (StackSymbol M)} (hread : (p, gamma) ∈ (emptyStackPDA M).transition_fun q a Z) (hepsilon : (p, gamma) ∈ (emptyStackPDA M).transition_fun' q Z) : False

A reading and an epsilon transition of the normalized empty-stack PDA cannot have the same output. In a simulation state this is inherited from the underlying DPDA; the only additional epsilon move enters the drain state, which no reading move can enter.

theorem DPDA_to_LR.introducingEdgesUnique_of_activeHeadUnique {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (hhead : ActiveHeadUnique M) : IntroducingEdgesUnique M

The history-sensitive uniqueness of the parent head determines the whole list-introducing edge.