Semantic validity of canonical LR(k) items

An item [A → alpha · beta, u] is valid for a prefix gamma when a rightmost derivation reaches p A s, gamma = p alpha, and u is the EOF-padded k-lookahead of s. This file establishes the easy (soundness) half of the canonical viable-prefix theorem: item closure and goto preserve that semantic invariant.

Context closure of rightmost derivations

theorem CF_grammar.LRk.rewritesRightmost_append_left {T N : Type} {r : N × List (symbol T N)} {u v : List (symbol T N)} (h : RewritesRightmost r u v) (pre : List (symbol T N)) : RewritesRightmost r (pre ++ u) (pre ++ v)

theorem CF_grammar.LRk.producesRightmost_append_left {T : Type} (G : CF_grammar T) {u v : List (symbol T G.nt)} (h : G.ProducesRightmost u v) (pre : List (symbol T G.nt)) : G.ProducesRightmost (pre ++ u) (pre ++ v)

theorem CF_grammar.LRk.derivesRightmost_append_left {T : Type} (G : CF_grammar T) {u v : List (symbol T G.nt)} (h : G.DerivesRightmost u v) (pre : List (symbol T G.nt)) : G.DerivesRightmost (pre ++ u) (pre ++ v)

theorem CF_grammar.LRk.rewritesRightmost_append_terminals_right {T N : Type} {r : N × List (symbol T N)} {u v : List (symbol T N)} (h : RewritesRightmost r u v) (suffix : List T) : RewritesRightmost r (u ++ List.map symbol.terminal suffix) (v ++ List.map symbol.terminal suffix)

theorem CF_grammar.LRk.producesRightmost_append_terminals_right {T : Type} (G : CF_grammar T) {u v : List (symbol T G.nt)} (h : G.ProducesRightmost u v) (suffix : List T) : G.ProducesRightmost (u ++ List.map symbol.terminal suffix) (v ++ List.map symbol.terminal suffix)

theorem CF_grammar.LRk.derivesRightmost_append_terminals_right {T : Type} (G : CF_grammar T) {u v : List (symbol T G.nt)} (h : G.DerivesRightmost u v) (suffix : List T) : G.DerivesRightmost (u ++ List.map symbol.terminal suffix) (v ++ List.map symbol.terminal suffix)

Item decomposition

theorem CF_grammar.LRk.Item.rule_eq_before_next_afterNext {T : Type} {G : CF_grammar T} {k : ℕ} (i : Item G k) {X : symbol T G.nt} (hnext : i.next? = some X) : (ruleAt G i.rule).2 = i.before ++ [X] ++ i.afterNext

If the dot is followed by X, the production splits into the prefix before the dot, X, and the suffix after X.

theorem CF_grammar.LRk.before_eq_of_advances {T : Type} {G : CF_grammar T} {k : ℕ} {i j : Item G k} {X : symbol T G.nt} (h : Advances i X j) : j.before = i.before ++ [X]

Advancing an item appends exactly the traversed symbol to its before-dot prefix.

Semantic validity

def CF_grammar.LRk.Valid {T : Type} (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.nt)) (i : Item G k) : Prop

Semantic validity of an LR item for an already scanned grammar-symbol prefix.

Equations

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

noncomputable def CF_grammar.LRk.validItems {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.nt)) : Finset (Item G k)

The finite set of all semantically valid items at a prefix.

Equations

• CF_grammar.LRk.validItems G k gamma = Finset.filter (CF_grammar.LRk.Valid G k gamma) Finset.univ

@[simp]

theorem CF_grammar.LRk.mem_validItems {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.nt)) (i : Item G k) : i ∈ validItems G k gamma ↔ Valid G k gamma i

theorem CF_grammar.LRk.Valid.apply_rule {T : Type} {G : CF_grammar T} {k : ℕ} {gamma : List (symbol T G.nt)} {i : Item G k} (hi : Valid G k gamma i) : ∃ (p : List (symbol T G.nt)) (s : List T), gamma = p ++ i.before ∧ observe k s = i.lookahead ∧ G.DerivesRightmost [symbol.nonterminal G.initial] (p ++ (ruleAt G i.rule).2 ++ List.map symbol.terminal s)

Applying the production named by a valid item reaches its complete right-sentential form.

theorem CF_grammar.LRk.Valid.closureStep {T : Type} {G : CF_grammar T} {k : ℕ} {gamma : List (symbol T G.nt)} {i j : Item G k} (hi : Valid G k gamma i) (hij : ClosureStep G k i j) : Valid G k gamma j

One item-closure edge preserves semantic validity at the same prefix.

theorem CF_grammar.LRk.Valid.of_mem_closure {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} {gamma : List (symbol T G.nt)} {I : Finset (Item G k)} (hI : ∀ i ∈ I, Valid G k gamma i) {j : Item G k} (hj : j ∈ closure G k I) : Valid G k gamma j

The whole finite epsilon closure preserves semantic validity.

theorem CF_grammar.LRk.Valid.goto {T : Type} [Fintype T] {G : CF_grammar T} {k : ℕ} {gamma : List (symbol T G.nt)} {I : Finset (Item G k)} (hI : ∀ i ∈ I, Valid G k gamma i) {X : symbol T G.nt} {j : Item G k} (hj : j ∈ LRk.goto G k I X) : Valid G k (gamma ++ [X]) j

A goto edge advances semantic validity by the traversed grammar symbol.