Correctness of the canonical LR table

This file gives a small grammar-symbol-stack semantics for the canonical table. It separates the mathematical handle-pruning proof from the later finite-control/buffer simulation by the concrete DPDA.

structure CF_grammar.LRk.CanonicalParser.Config (T : Type) (G : CF_grammar T) : Type

• stack : List (symbol T G.augment.nt)
• input : List T

def CF_grammar.LRk.CanonicalParser.Config.form {T : Type} {G : CF_grammar T} (c : Config T G) : List (symbol T G.augment.nt)

Equations

• c.form = c.stack ++ List.map symbol.terminal c.input

def CF_grammar.LRk.CanonicalParser.initialConfig {T : Type} (G : CF_grammar T) (w : List T) : Config T G

Equations

• CF_grammar.LRk.CanonicalParser.initialConfig G w = { stack := [], input := w }

inductive CF_grammar.LRk.CanonicalParser.Step {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) : Config T G → Config T G → Prop

One trusted table step. The suffix equation in the reduction constructor is not an extra parser test: on reachable kernels it follows from semantic item validity. Recording it here makes the handle-pruning invariant explicit.

• shift {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} {gamma : List (symbol T G.augment.nt)} {a : T} {w : List T} (haction : tableAction G k (scanKernel G k gamma) (observe k (a :: w)) = TableAction.shift) : Step G k { stack := gamma, input := a :: w } { stack := gamma ++ [symbol.terminal a], input := w }
• reduce {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} {gamma p : List (symbol T G.augment.nt)} {w : List T} {r : RuleIndex G.augment} (haction : tableAction G k (scanKernel G k gamma) (observe k w) = TableAction.reduce r) (hgamma : gamma = p ++ (ruleAt G.augment r).2) : Step G k { stack := gamma, input := w } { stack := p ++ [symbol.nonterminal (ruleAt G.augment r).1], input := w }

@[reducible, inline]

abbrev CF_grammar.LRk.CanonicalParser.Reaches {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) : Config T G → Config T G → Prop

Equations

• CF_grammar.LRk.CanonicalParser.Reaches G k = Relation.ReflTransGen (CF_grammar.LRk.CanonicalParser.Step G k)

def CF_grammar.LRk.CanonicalParser.Accepting {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (c : Config T G) : Prop

Equations

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

def CF_grammar.LRk.CanonicalParser.Accepts {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (w : List T) : Prop

Equations

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

@[simp]

theorem CF_grammar.LRk.CanonicalParser.lookaheadHead_observe_cons {T : Type} [Fintype T] (k : ℕ) (hk : 0 < k) (a : T) (w : List T) : lookaheadHead k (observe k (a :: w)) = some a

def CF_grammar.LRk.CanonicalParser.completedItem {T : Type} (G : CF_grammar T) (k : ℕ) (r : RuleIndex G.augment) (u : Lookahead T k) : Item G.augment k

A convenient completed item naming a rule occurrence.

Equations

• CF_grammar.LRk.CanonicalParser.completedItem G k r u = ⟨r, (⟨(CF_grammar.LRk.ruleAt G.augment r).2.length, ⋯⟩, u)⟩

@[simp]

theorem CF_grammar.LRk.CanonicalParser.completedItem_complete {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (r : RuleIndex G.augment) (u : Lookahead T k) : (completedItem G k r u).Complete

@[simp]

theorem CF_grammar.LRk.CanonicalParser.completedItem_before {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (r : RuleIndex G.augment) (u : Lookahead T k) : (completedItem G k r u).before = (ruleAt G.augment r).2

@[simp]

theorem CF_grammar.LRk.CanonicalParser.completedItem_lookahead {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (r : RuleIndex G.augment) (u : Lookahead T k) : (completedItem G k r u).lookahead = u

theorem CF_grammar.LRk.CanonicalParser.fresh_not_mem_augmentString {T : Type} [Fintype T] (G : CF_grammar T) (w : List (symbol T G.nt)) : symbol.nonterminal none ∉ augmentString w

Fresh augmentation never inserts the fresh start symbol into an embedded right-hand side.

theorem CF_grammar.LRk.CanonicalParser.fresh_not_mem_rule_rhs {T : Type} [Fintype T] (G : CF_grammar T) {r : G.augment.nt × List (symbol T G.augment.nt)} (hr : r ∈ G.augment.rules) : symbol.nonterminal none ∉ r.2

No augmented production has the fresh start nonterminal in its right-hand side.

theorem CF_grammar.LRk.CanonicalParser.fresh_prehandle_eq_root {T : Type} [Fintype T] (G : CF_grammar T) {p : List (symbol T G.augment.nt)} {s : List T} (h : G.augment.DerivesRightmost [symbol.nonterminal G.augment.initial] (p ++ [symbol.nonterminal none] ++ List.map symbol.terminal s)) : p = [] ∧ s = []

A surviving occurrence of the fresh initial nonterminal can only be the untouched root configuration.

theorem CF_grammar.LRk.CanonicalParser.stateReduction_of_prehandle {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) {r : RuleIndex G.augment} {p : List (symbol T G.augment.nt)} {s : List T} (hpre : G.augment.DerivesRightmost [symbol.nonterminal G.augment.initial] (p ++ [symbol.nonterminal (ruleAt G.augment r).1] ++ List.map symbol.terminal s)) : StateReduction G k (p ++ (ruleAt G.augment r).2) (observe k s) (ruleAt G.augment r)

A displayed rightmost prehandle exposes its production as a reduction in the canonical state at the completed handle boundary.

theorem CF_grammar.LRk.CanonicalParser.tableAction_shift_before_handle {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) (hLR : G.IsLRk k) {r : RuleIndex G.augment} {p gamma : List (symbol T G.augment.nt)} {s x : List T} {a : T} (hpre : G.augment.DerivesRightmost [symbol.nonterminal G.augment.initial] (p ++ [symbol.nonterminal (ruleAt G.augment r).1] ++ List.map symbol.terminal s)) (hboundary : p ++ (ruleAt G.augment r).2 = gamma ++ symbol.terminal a :: List.map symbol.terminal x) : tableAction G k (scanKernel G k gamma) (observe k (a :: x ++ s)) = TableAction.shift

Before a later displayed handle boundary, LR(k) conflict freedom forces the total table's default shift.

theorem CF_grammar.LRk.CanonicalParser.shifts_to_handle {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) (hLR : G.IsLRk k) {r : RuleIndex G.augment} {p gamma : List (symbol T G.augment.nt)} {s x : List T} (hpre : G.augment.DerivesRightmost [symbol.nonterminal G.augment.initial] (p ++ [symbol.nonterminal (ruleAt G.augment r).1] ++ List.map symbol.terminal s)) (hboundary : p ++ (ruleAt G.augment r).2 = gamma ++ List.map symbol.terminal x) : Reaches G k { stack := gamma, input := x ++ s } { stack := p ++ (ruleAt G.augment r).2, input := s }

A block of terminals before a displayed handle can be shifted without the table skipping an earlier reduction.

theorem CF_grammar.LRk.CanonicalParser.split_at_handle_boundary {T : Type} [Fintype T] {N : Type} {gamma B : List (symbol T N)} {input s : List T} (hend : gamma = [] ∨ ∃ (p : List (symbol T N)) (A : N), gamma = p ++ [symbol.nonterminal A]) (heq : gamma ++ List.map symbol.terminal input = B ++ List.map symbol.terminal s) : ∃ (x : List T), B = gamma ++ List.map symbol.terminal x ∧ input = x ++ s

Prefix/terminal-suffix comparison at a rightmost handle boundary.

theorem CF_grammar.LRk.CanonicalParser.split_fresh_root {T : Type} [Fintype T] (G : CF_grammar T) {gamma : List (symbol T (Option G.nt))} {input : List T} (hend : gamma = [] ∨ ∃ (p : List (symbol T (Option G.nt))) (A : Option G.nt), gamma = p ++ [symbol.nonterminal A]) (heq : gamma ++ List.map symbol.terminal input = [symbol.nonterminal none]) : gamma = [symbol.nonterminal none] ∧ input = []

The only terminal-suffix split of the one-symbol fresh root whose prefix is empty or ends in a nonterminal is the root itself with empty suffix.

def CF_grammar.LRk.CanonicalParser.BackOutcome {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (c : Config T G) : Prop

Result of pruning a counted rightmost derivation: either the table has accepted, or the degenerate zero-step derivation has reached the fresh root.

Equations

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

theorem CF_grammar.LRk.CanonicalParser.parses_back_of_derivesRightmostIn {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) (hLR : G.IsLRk k) {n : ℕ} {gamma : List (symbol T G.augment.nt)} {input : List T} (h : G.augment.DerivesRightmostIn n [symbol.nonterminal G.augment.initial] (gamma ++ List.map symbol.terminal input)) (hend : gamma = [] ∨ ∃ (p : List (symbol T G.augment.nt)) (A : G.augment.nt), gamma = p ++ [symbol.nonterminal A]) : BackOutcome G k { stack := gamma, input := input }

Reverse a counted rightmost derivation by shifting up to each displayed handle and then taking the unique LR(k) reduction.

def CF_grammar.LRk.CanonicalParser.FreshFree {T : Type} {G : CF_grammar T} (c : Config T G) : Prop

The parser stack never contains the fresh augmented start nonterminal. That symbol is recognized by the accept action rather than pushed by a reduction.

Equations

• CF_grammar.LRk.CanonicalParser.FreshFree c = (symbol.nonterminal none ∉ c.stack)

theorem CF_grammar.LRk.CanonicalParser.Step.freshFree {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} {c d : Config T G} (h : Step G k c d) (hc : FreshFree c) : FreshFree d

theorem CF_grammar.LRk.CanonicalParser.Reaches.freshFree {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} {c d : Config T G} (h : Reaches G k c d) (hc : FreshFree c) : FreshFree d

theorem CF_grammar.LRk.CanonicalParser.accepts_complete {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (hk : 0 < k) (hLR : G.IsLRk k) {w : List T} (hw : w ∈ CF_language G) : Accepts G k w

Every word generated by an LR(k) grammar is accepted by its canonical table (for positive lookahead).