Soundness of the canonical LR parser

Every bottom-up parser step reverses either no grammar step (a shift) or one rightmost grammar step (a reduction). Consequently an accepting canonical run reconstructs a derivation of its input word.

theorem CF_grammar.LRk.CanonicalParser.Step.form_derives {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} {c d : Config T G} (h : Step G k c d) : G.augment.DerivesRightmost d.form c.form

A trusted canonical parser step reads the sentential forms backwards.

theorem CF_grammar.LRk.CanonicalParser.Reaches.form_derives {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} {c d : Config T G} (h : Reaches G k c d) : G.augment.DerivesRightmost d.form c.form

Along a canonical run, the current sentential form rightmost-derives the sentential form at the beginning of the run.

theorem CF_grammar.LRk.CanonicalParser.accepts_sound {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) {w : List T} (h : Accepts G k w) : w ∈ CF_language G

Every word accepted by the canonical table belongs to the source context-free language.