Syntactic cancellation at characteristic handles

Every nonempty right side of the characteristic grammar ends in a list nonterminal. A rightmost-reachable prefix, on the other hand, contains only terminals and single nonterminals. Thus that final list is a genuine marker: equality of two post-handle forms determines the text on both sides of it.

def DPDA_to_LR.IsListSymbol {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) : symbol T (Nonterminal M) → Prop

A grammar symbol is one of the characteristic list nonterminals.

Equations

• DPDA_to_LR.IsListSymbol M (symbol.nonterminal (PDA_to_CFG.N.list a a_1 a_2)) = True
• DPDA_to_LR.IsListSymbol M x✝ = False

theorem DPDA_to_LR.cancel_unique_marker {X : Type} {P : X → Prop} {left₁ left₂ right₁ right₂ : List X} {marker₁ marker₂ : X} (hleft₁ : ∀ x ∈ left₁, ¬P x) (hleft₂ : ∀ x ∈ left₂, ¬P x) (hmarker₁ : P marker₁) (hmarker₂ : P marker₂) (heq : left₂ ++ marker₂ :: right₂ = left₁ ++ marker₁ :: right₁) : left₂ = left₁ ∧ marker₂ = marker₁ ∧ right₂ = right₁

Cancellation around a marker which cannot occur in either surrounding list. This elementary list lemma is kept independent of grammar syntax.

theorem DPDA_to_LR.no_marker_ne_append_marker {X : Type} {P : X → Prop} {plain left right : List X} {marker : X} (hplain : ∀ x ∈ plain, ¬P x) (hmarker : P marker) : plain ≠ left ++ marker :: right

A marker cannot occur in a list all of whose elements are nonmarkers.

theorem DPDA_to_LR.append_singleton_injective {X : Type} {left₁ left₂ : List X} {x₁ x₂ : X} (heq : left₂ ++ [x₂] = left₁ ++ [x₁]) : left₂ = left₁ ∧ x₂ = x₁

Equality of two lists with one final element cancels both final elements.

theorem DPDA_to_LR.PendingPrefix.noList {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} (hp : PendingPrefix M p) (X : symbol T (Nonterminal M)) : X ∈ p → ¬IsListSymbol M X

Pending rightmost prefixes contain no characteristic list symbol.

theorem DPDA_to_LR.terminals_noList {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (w : List T) (X : symbol T (Nonterminal M)) : X ∈ List.map symbol.terminal w → ¬IsListSymbol M X

Terminal words contain no characteristic list symbol.

theorem DPDA_to_LR.PendingPrefix.noList_append_terminal {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} (hp : PendingPrefix M p) (a : T) (X : symbol T (Nonterminal M)) : X ∈ p ++ [symbol.terminal a] → ¬IsListSymbol M X

Appending a terminal preserves absence of characteristic list symbols.

theorem DPDA_to_LR.PendingPrefix.noList_append_single {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} (hp : PendingPrefix M p) (q target : State M) (Z : StackSymbol M) (X : symbol T (Nonterminal M)) : X ∈ p ++ [symbol.nonterminal (PDA_to_CFG.N.single q Z target)] → ¬IsListSymbol M X

Appending a single preserves absence of characteristic list symbols.

theorem DPDA_to_LR.PendingPrefix.noList_append_terminals {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {p : List (symbol T (Nonterminal M))} (hp : PendingPrefix M p) (w : List T) (X : symbol T (Nonterminal M)) : X ∈ p ++ List.map symbol.terminal w → ¬IsListSymbol M X

Appending a terminal word preserves absence of list symbols.

@[simp]

theorem DPDA_to_LR.isListSymbol_list {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) (q target : State M) (gamma : List (StackSymbol M)) : IsListSymbol M (symbol.nonterminal (PDA_to_CFG.N.list q gamma target))

theorem DPDA_to_LR.cancel_characteristic_list_marker {Q T S : Type} [Fintype Q] [Fintype T] [Fintype S] (M : DPDA Q T S) {left₁ left₂ : List (symbol T (Nonterminal M))} {q₁ q₂ target₁ target₂ : State M} {gamma₁ gamma₂ : List (StackSymbol M)} {suffix₁ suffix₂ : List T} (hleft₁ : ∀ X ∈ left₁, ¬IsListSymbol M X) (hleft₂ : ∀ X ∈ left₂, ¬IsListSymbol M X) (heq : left₂ ++ [symbol.nonterminal (PDA_to_CFG.N.list q₂ gamma₂ target₂)] ++ List.map symbol.terminal suffix₂ = left₁ ++ [symbol.nonterminal (PDA_to_CFG.N.list q₁ gamma₁ target₁)] ++ List.map symbol.terminal suffix₁) : left₂ = left₁ ∧ q₂ = q₁ ∧ gamma₂ = gamma₁ ∧ target₂ = target₁ ∧ suffix₂ = suffix₁

Specialized cancellation for the final list nonterminal of two characteristic right sides.