Reverse viable-prefix lemmas

The soundness development follows item edges forward. Completeness needs the converse structural fact. The first such fact is proved here: a valid item at dot position zero is either the untouched start configuration, or is obtained by one closure edge from a valid parent item. It is a direct item-level form of CF_grammar.derivesRightmost_nonterminal_ancestry.

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

Semantic item validity with an exact count of the rightmost derivation steps reaching the item's prehandle.

Equations

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

theorem CF_grammar.LRk.ValidIn.valid {T : Type} {G : CF_grammar T} {k n : ℕ} {gamma : List (symbol T G.nt)} {i : Item G k} (h : ValidIn G k n gamma i) : Valid G k gamma i

theorem CF_grammar.LRk.Valid.exists_validIn {T : Type} {G : CF_grammar T} {k : ℕ} {gamma : List (symbol T G.nt)} {i : Item G k} (h : Valid G k gamma i) : ∃ (n : ℕ), ValidIn G k n gamma i

theorem CF_grammar.LRk.Item.ext_of_rule_position_lookahead {T : Type} {G : CF_grammar T} {k : ℕ} {i j : Item G k} (hrule : i.rule = j.rule) (hposition : ↑i.position = ↑j.position) (hlookahead : i.lookahead = j.lookahead) : i = j

Extensionality for dependent canonical items, stated through their public projections.

theorem CF_grammar.LRk.augment_ruleIndex_eq_start_of_fst_eq_none {T : Type} (G : CF_grammar T) (i : RuleIndex G.augment) (h : (ruleAt G.augment i).1 = none) : i = startRuleIndex G

The distinguished start rule is the only augmented rule headed by the fresh nonterminal.

theorem CF_grammar.LRk.Item.eq_startItem_of_root {T : Type} (G : CF_grammar T) (k : ℕ) {i : Item G.augment k} (hposition : ↑i.position = 0) (hhead : (ruleAt G.augment i.rule).1 = none) (hlook : i.lookahead = eofLookahead T k) : i = startItem G k

An augmented item at the untouched fresh-start configuration is exactly the distinguished start item.

theorem CF_grammar.LRk.Valid.positive_position_predecessor {T : Type} {G : CF_grammar T} {k : ℕ} {gamma : List (symbol T G.nt)} {j : Item G k} (hj : Valid G k gamma j) (hpositive : 0 < ↑j.position) : ∃ (delta : List (symbol T G.nt)) (X : symbol T G.nt) (i : Item G k), gamma = delta ++ [X] ∧ Valid G k delta i ∧ Advances i X j

A valid item with a positive dot position is obtained by one goto advancement from a valid item at the prefix with its final symbol removed.

theorem CF_grammar.LRk.ValidIn.positive_position_predecessor {T : Type} {G : CF_grammar T} {k n : ℕ} {gamma : List (symbol T G.nt)} {j : Item G k} (hj : ValidIn G k n gamma j) (hpositive : 0 < ↑j.position) : ∃ (delta : List (symbol T G.nt)) (X : symbol T G.nt) (i : Item G k), gamma = delta ++ [X] ∧ ValidIn G k n delta i ∧ Advances i X j

Counted form of Valid.positive_position_predecessor; reversing a goto keeps the derivation count unchanged and shortens the scanned prefix.

theorem CF_grammar.LRk.Valid.zero_position_ancestry {T : Type} {G : CF_grammar T} {k : ℕ} {gamma : List (symbol T G.nt)} {j : Item G k} (hj : Valid G k gamma j) (hzero : ↑j.position = 0) : gamma = [] ∧ (ruleAt G j.rule).1 = G.initial ∧ j.lookahead = eofLookahead T k ∨ ∃ (i : Item G k), Valid G k gamma i ∧ ClosureStep G k i j

A valid zero-dot item is either rooted at the untouched initial nonterminal, or has a valid parent connected by one canonical closure edge.

theorem CF_grammar.LRk.ValidIn.zero_position_ancestry {T : Type} {G : CF_grammar T} {k n : ℕ} {gamma : List (symbol T G.nt)} {j : Item G k} (hj : ValidIn G k n gamma j) (hzero : ↑j.position = 0) : gamma = [] ∧ (ruleAt G j.rule).1 = G.initial ∧ j.lookahead = eofLookahead T k ∨ ∃ (m : ℕ) (i : Item G k), m < n ∧ ValidIn G k m gamma i ∧ ClosureStep G k i j

Counted zero-dot ancestry. In the non-root case the valid parent is reached in strictly fewer rightmost steps.

theorem CF_grammar.LRk.validIn_mem_itemState {T : Type} [Fintype T] (G : CF_grammar T) (k : ℕ) {n : ℕ} {gamma : List (symbol T G.augment.nt)} {i : Item G.augment k} (hi : ValidIn G.augment k n gamma i) : i ∈ itemState G k gamma

Full viable-prefix completeness for the augmented canonical item automaton, with an exact derivation witness.

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

Semantic validity and membership in the finite canonical state coincide.