Semantic conflict freedom for LR(k) grammars

This file packages the two direct consequences of Knuth's handle-uniqueness condition needed by a deterministic bottom-up parser. A reduction candidate is a handle ending at the current prefix. A later-handle candidate witnesses that the handle ending in the same right-sentential form lies strictly to the right of that prefix. CoreIsLRk makes reductions unique and rules out a reduction/later-handle conflict at equal lookahead.

theorem CF_grammar.LRk.lrLookahead_eq_of_observe_eq {T : Type} {k : ℕ} {u v : List T} (h : observe k u = observe k v) : lrLookahead k u = lrLookahead k v

Equality of padded k-observations implies equality of the usual length-at-most-k terminal prefixes.

def CF_grammar.LRk.ReductionCandidate {T : Type} (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.nt)) (u : Lookahead T k) (r : G.nt × List (symbol T G.nt)) : Prop

A production is reducible at gamma with padded lookahead u when a rightmost derivation has reached its left-hand nonterminal and applying the production ends exactly at gamma.

Equations

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

def CF_grammar.LRk.LaterHandleCandidate {T : Type} (G : CF_grammar T) (k : ℕ) (gamma : List (symbol T G.nt)) (u : Lookahead T k) : Prop

A handle lies genuinely later than gamma in a right-sentential form whose terminal suffix has padded lookahead u. The displayed terminal a is the first grammar symbol beyond gamma; retaining it makes strictness structural rather than an inequality on lengths.

Equations

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

theorem CF_grammar.LRk.CoreIsLRk.reductionCandidate_unique {T : Type} {G : CF_grammar T} {k : ℕ} (hLR : G.CoreIsLRk k) {gamma : List (symbol T G.nt)} {u : Lookahead T k} {r₁ r₂ : G.nt × List (symbol T G.nt)} (h₁ : ReductionCandidate G k gamma u r₁) (h₂ : ReductionCandidate G k gamma u r₂) : r₁ = r₂

Two reductions enabled at the same prefix and lookahead use the same production (and, internally, the same handle position).

theorem CF_grammar.LRk.CoreIsLRk.not_reductionCandidate_and_laterHandleCandidate {T : Type} {G : CF_grammar T} {k : ℕ} (hLR : G.CoreIsLRk k) {gamma : List (symbol T G.nt)} {u : Lookahead T k} {r₁ : G.nt × List (symbol T G.nt)} (hred : ReductionCandidate G k gamma u r₁) : ¬LaterHandleCandidate G k gamma u

An LR(k) reduction cannot coexist with a handle ending strictly later in the same right-sentential form at the same lookahead. This is the semantic shift/reduce-conflict theorem; unlike reduce/reduce uniqueness, it uses the full sentential-form equality in CoreIsLRk.