ε-Free Indexed Grammars

This file develops the stack-sensitive nullability infrastructure used by the normal-form pipeline. Nullability for indexed grammars depends on the current stack, so ε-elimination is organized around right-hand-side sublists whose deleted symbols are nullable at the stack they receive during expansion.

References

• A. V. Aho, "Indexed grammars — an extension of context-free grammars", JACM 15(4), 1968.

def IndexedGrammar.IsNullable {T : Type} (g : IndexedGrammar T) (A : g.nt) (σ : List g.flag) : Prop

A nonterminal A with stack σ is nullable if g can derive [] from [indexed A σ].

Equations

• g.IsNullable A σ = g.Derives [IndexedGrammar.ISym.indexed A σ] []

theorem IndexedGrammar.generates_nil_iff_initial_nullable {T : Type} (g : IndexedGrammar T) : g.Generates [] ↔ g.IsNullable g.initial []

Generating the empty word is exactly nullability of the initial nonterminal with the empty stack.

theorem IndexedGrammar.isNullable_appendStackSuffix {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} (h : g.IsNullable A σ) (suffix : List g.flag) : g.IsNullable A (σ ++ suffix)

theorem IndexedGrammar.not_isNullable_of_noEpsilon {T : Type} {g : IndexedGrammar T} (hne : g.NoEpsilon') (A : g.nt) (σ : List g.flag) : ¬g.IsNullable A σ

In a no-ε indexed grammar, no single stacked nonterminal can derive the empty sentential form.

theorem IndexedGrammar.derives_erase_nullable {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} (hnullable : g.IsNullable A σ) (u v : List g.ISym) : g.Derives (u ++ [ISym.indexed A σ] ++ v) (u ++ v)

A nullable stacked nonterminal can be erased in any sentential context.

theorem IndexedGrammar.transforms_append_cases {T : Type} {g : IndexedGrammar T} {u v w : List g.ISym} (hstep : g.Transforms (u ++ v) w) : (∃ (u' : List g.ISym), g.Transforms u u' ∧ w = u' ++ v) ∨ ∃ (v' : List g.ISym), g.Transforms v v' ∧ w = u ++ v'

A one-step indexed rewrite of an appended sentential form rewrites either the left side or the right side of the append.

theorem IndexedGrammar.derives_nil_of_append_left {T : Type} {g : IndexedGrammar T} {u v : List g.ISym} (hder : g.Derives (u ++ v) []) : g.Derives u []

If an appended sentential form derives [], then its left component also derives [].

theorem IndexedGrammar.derives_nil_of_append_right {T : Type} {g : IndexedGrammar T} {u v : List g.ISym} (hder : g.Derives (u ++ v) []) : g.Derives v []

If an appended sentential form derives [], then its right component also derives [].

theorem IndexedGrammar.derives_nil_of_append {T : Type} {g : IndexedGrammar T} {u v w : List g.ISym} (hder : g.Derives (u ++ v ++ w) []) : g.Derives v []

If u ++ v ++ w derives [], then the middle component derives [].

theorem IndexedGrammar.derivesIn_nil_of_append_left {T : Type} {g : IndexedGrammar T} {n : ℕ} {u v : List g.ISym} (hder : g.DerivesIn n (u ++ v) []) : ∃ m ≤ n, g.DerivesIn m u []

Counted form: if u ++ v derives [], then u derives [] within the original budget.

theorem IndexedGrammar.derivesIn_nil_of_append_right {T : Type} {g : IndexedGrammar T} {n : ℕ} {u v : List g.ISym} (hder : g.DerivesIn n (u ++ v) []) : ∃ m ≤ n, g.DerivesIn m v []

Counted form: if u ++ v derives [], then v derives [] within the original budget.

theorem IndexedGrammar.derivesIn_nil_of_mem {T : Type} {g : IndexedGrammar T} {n : ℕ} {w : List g.ISym} {s : g.ISym} (hder : g.DerivesIn n w []) (hs : s ∈ w) : ∃ m ≤ n, g.DerivesIn m [s] []

Counted form: every symbol in a sentential form deriving [] derives [] within the original budget.

theorem IndexedGrammar.derives_nil_of_mem {T : Type} {g : IndexedGrammar T} {w : List g.ISym} {s : g.ISym} (hder : g.Derives w []) (hs : s ∈ w) : g.Derives [s] []

Every symbol occurring in a sentential form that derives [] is nullable as a singleton sentential form.

theorem IndexedGrammar.terminal_mem_of_transforms {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} {t : T} (hstep : g.Transforms w₁ w₂) : ISym.terminal t ∈ w₁ → ISym.terminal t ∈ w₂

A terminal already present in a sentential form is still present after one indexed-grammar rewrite step. Indexed rules rewrite only one indexed nonterminal in its context.

theorem IndexedGrammar.terminal_mem_of_derives {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} {t : T} (hder : g.Derives w₁ w₂) : ISym.terminal t ∈ w₁ → ISym.terminal t ∈ w₂

A terminal already present in a sentential form is preserved by any indexed derivation.

theorem IndexedGrammar.not_derives_nil_of_terminal_mem {T : Type} {g : IndexedGrammar T} {w : List g.ISym} {t : T} (ht : ISym.terminal t ∈ w) : ¬g.Derives w []

A sentential form containing a terminal cannot derive the empty sentential form.

theorem IndexedGrammar.no_terminal_mem_of_derives_nil {T : Type} {g : IndexedGrammar T} {w : List g.ISym} (hder : g.Derives w []) (t : T) : ISym.terminal t ∉ w

If a sentential form derives [], it contains no terminal.

theorem IndexedGrammar.terminal_mem_expandRhs_of_mem {T : Type} {g : IndexedGrammar T} {rhs : List (IRhsSymbol T g.nt g.flag)} {σ : List g.flag} {t : T} (ht : IRhsSymbol.terminal t ∈ rhs) : ISym.terminal t ∈ g.expandRhs rhs σ

A terminal RHS symbol appears as the corresponding terminal in any expansion.

theorem IndexedGrammar.terminal_mem_rhs_of_mem_expandRhs {T : Type} {g : IndexedGrammar T} {rhs : List (IRhsSymbol T g.nt g.flag)} {σ : List g.flag} {t : T} (ht : ISym.terminal t ∈ g.expandRhs rhs σ) : IRhsSymbol.terminal t ∈ rhs

Terminals in an expanded RHS come exactly from terminal RHS symbols.

theorem IndexedGrammar.no_terminal_mem_rhs_of_expandRhs_derives_nil {T : Type} {g : IndexedGrammar T} {rhs : List (IRhsSymbol T g.nt g.flag)} {σ : List g.flag} (hder : g.Derives (g.expandRhs rhs σ) []) (t : T) : IRhsSymbol.terminal t ∉ rhs

If an expanded RHS can derive [], the original RHS contains no terminal symbols.

theorem IndexedGrammar.derives_nil_of_all_nullable_indexed {T : Type} {g : IndexedGrammar T} {w : List g.ISym} (hnullable : ∀ s ∈ w, ∃ (A : g.nt) (σ : List g.flag), s = ISym.indexed A σ ∧ g.IsNullable A σ) : g.Derives w []

A sentential form whose every symbol is a nullable indexed nonterminal derives the empty sentential form.

theorem IndexedGrammar.all_nullable_indexed_of_derives_nil {T : Type} {g : IndexedGrammar T} {w : List g.ISym} (hder : g.Derives w []) (s : g.ISym) : s ∈ w → ∃ (A : g.nt) (σ : List g.flag), s = ISym.indexed A σ ∧ g.IsNullable A σ

If a sentential form derives [], every symbol in it is a nullable indexed nonterminal.

theorem IndexedGrammar.derives_nil_iff_all_nullable_indexed {T : Type} {g : IndexedGrammar T} {w : List g.ISym} : g.Derives w [] ↔ ∀ s ∈ w, ∃ (A : g.nt) (σ : List g.flag), s = ISym.indexed A σ ∧ g.IsNullable A σ

A sentential form derives [] exactly when all of its symbols are nullable indexed nonterminals.

theorem IndexedGrammar.expandRhs_derives_nil_iff_all_nullable_rhs {T : Type} {g : IndexedGrammar T} {rhs : List (IRhsSymbol T g.nt g.flag)} {σ : List g.flag} : g.Derives (g.expandRhs rhs σ) [] ↔ ∀ s ∈ rhs, ∃ (A : g.nt) (push : Option g.flag), s = IRhsSymbol.nonterminal A push ∧ g.IsNullable A (match push with | none => σ | some f => f :: σ)

An expanded RHS derives [] exactly when every RHS symbol is a nonterminal nullable at the stack it receives from the expansion.

theorem IndexedGrammar.derivesIn_nil_of_expandRhs_nonterminal_mem {T : Type} {g : IndexedGrammar T} {n : ℕ} {rhs : List (IRhsSymbol T g.nt g.flag)} {σ : List g.flag} {B : g.nt} {push : Option g.flag} (hder : g.DerivesIn n (g.expandRhs rhs σ) []) (hs : IRhsSymbol.nonterminal B push ∈ rhs) : ∃ m ≤ n, g.DerivesIn m [ISym.indexed B (match push, hs with | none, hs => σ | some f, hs => f :: σ)] []

Counted extraction for one nonterminal occurrence in an expanded RHS deriving [].

inductive IndexedGrammar.NullableRhsSublist {T : Type} (g : IndexedGrammar T) (σ : List g.flag) : List (IRhsSymbol T g.nt g.flag) → List (IRhsSymbol T g.nt g.flag) → Prop

kept is obtained from rhs by deleting only RHS nonterminals that are nullable at the stack they receive during expansion.

• nil {T : Type} {g : IndexedGrammar T} {σ : List g.flag} : g.NullableRhsSublist σ [] []
• keep {T : Type} {g : IndexedGrammar T} {σ : List g.flag} (s : IRhsSymbol T g.nt g.flag) {rhs kept : List (IRhsSymbol T g.nt g.flag)} (h : g.NullableRhsSublist σ rhs kept) : g.NullableRhsSublist σ (s :: rhs) (s :: kept)
• drop_none {T : Type} {g : IndexedGrammar T} {σ : List g.flag} {A : g.nt} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (hnullable : g.IsNullable A σ) (h : g.NullableRhsSublist σ rhs kept) : g.NullableRhsSublist σ (IRhsSymbol.nonterminal A none :: rhs) kept
• drop_some {T : Type} {g : IndexedGrammar T} {σ : List g.flag} {A : g.nt} {f : g.flag} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (hnullable : g.IsNullable A (f :: σ)) (h : g.NullableRhsSublist σ rhs kept) : g.NullableRhsSublist σ (IRhsSymbol.nonterminal A (some f) :: rhs) kept

theorem IndexedGrammar.nullableRhsSublist_self {T : Type} (g : IndexedGrammar T) (σ : List g.flag) (rhs : List (IRhsSymbol T g.nt g.flag)) : g.NullableRhsSublist σ rhs rhs

theorem IndexedGrammar.NullableRhsSublist.sublist {T : Type} {g : IndexedGrammar T} {σ : List g.flag} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (h : g.NullableRhsSublist σ rhs kept) : kept.Sublist rhs

theorem IndexedGrammar.derives_expandRhs_of_nullableRhsSublist {T : Type} {g : IndexedGrammar T} {σ : List g.flag} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (h : g.NullableRhsSublist σ rhs kept) : g.Derives (g.expandRhs rhs σ) (g.expandRhs kept σ)

theorem IndexedGrammar.derives_context_expandRhs_of_nullableRhsSublist {T : Type} {g : IndexedGrammar T} {σ : List g.flag} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (h : g.NullableRhsSublist σ rhs kept) (u v : List g.ISym) : g.Derives (u ++ g.expandRhs rhs σ ++ v) (u ++ g.expandRhs kept σ ++ v)

theorem IndexedGrammar.derives_nil_of_nullableRhsSublist_nil {T : Type} {g : IndexedGrammar T} {σ : List g.flag} {rhs : List (IRhsSymbol T g.nt g.flag)} (h : g.NullableRhsSublist σ rhs []) : g.Derives (g.expandRhs rhs σ) []

theorem IndexedGrammar.NullableRhsSublist.kept_ne_nil_of_not_derives_nil {T : Type} {g : IndexedGrammar T} {σ : List g.flag} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (h : g.NullableRhsSublist σ rhs kept) (hnot : ¬g.Derives (g.expandRhs rhs σ) []) : kept ≠ []

theorem IndexedGrammar.exists_nonempty_nullableRhsSublist_of_not_derives_nil {T : Type} {g : IndexedGrammar T} {rhs : List (IRhsSymbol T g.nt g.flag)} {σ : List g.flag} (hnot : ¬g.Derives (g.expandRhs rhs σ) []) : ∃ (kept : List (IRhsSymbol T g.nt g.flag)), g.NullableRhsSublist σ rhs kept ∧ kept ≠ []

theorem IndexedGrammar.derives_rule_nullableRhsSublist_none {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} {σ : List g.flag} {kept : List (IRhsSymbol T g.nt g.flag)} (hr : r ∈ g.rules) (hconsume : r.consume = none) (hsub : g.NullableRhsSublist σ r.rhs kept) (u v : List g.ISym) : g.Derives (u ++ [ISym.indexed r.lhs σ] ++ v) (u ++ g.expandRhs kept σ ++ v)

theorem IndexedGrammar.derives_rule_nullableRhsSublist_some {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} {f : g.flag} {σ : List g.flag} {kept : List (IRhsSymbol T g.nt g.flag)} (hr : r ∈ g.rules) (hconsume : r.consume = some f) (hsub : g.NullableRhsSublist σ r.rhs kept) (u v : List g.ISym) : g.Derives (u ++ [ISym.indexed r.lhs (f :: σ)] ++ v) (u ++ g.expandRhs kept σ ++ v)

theorem IndexedGrammar.derives_rule_nullableRhsSublist {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} {σ : List g.flag} {kept : List (IRhsSymbol T g.nt g.flag)} (hr : r ∈ g.rules) (hsub : g.NullableRhsSublist σ r.rhs kept) (u v : List g.ISym) : g.Derives (match r.consume with | none => u ++ [ISym.indexed r.lhs σ] ++ v | some f => u ++ [ISym.indexed r.lhs (f :: σ)] ++ v) (u ++ g.expandRhs kept σ ++ v)

theorem IndexedGrammar.derives_empty_left_eq {T : Type} {g : IndexedGrammar T} {w : List g.ISym} (h : g.Derives [] w) : w = []

A derivation whose source sentential form is empty can only end at the empty sentential form.

theorem IndexedGrammar.exists_nullableRhsSublist_derives_to_terminals {T : Type} {g : IndexedGrammar T} {rhs : List (IRhsSymbol T g.nt g.flag)} {σ : List g.flag} {w : List T} (hder : g.Derives (g.expandRhs rhs σ) (List.map (fun (a : T) => ISym.terminal a) w)) : ∃ (kept : List (IRhsSymbol T g.nt g.flag)), g.NullableRhsSublist σ rhs kept ∧ g.Derives (g.expandRhs kept σ) (List.map (fun (a : T) => ISym.terminal a) w) ∧ (w ≠ [] → kept ≠ [])

If an expanded RHS derives a terminal word, then the same word is derived by some sublist obtained by deleting only nullable RHS nonterminals. Nonempty terminal output keeps at least one RHS symbol.

theorem IndexedGrammar.exists_nullableRhsSublist_derives_to_terminals_parts {T : Type} {g : IndexedGrammar T} {rhs : List (IRhsSymbol T g.nt g.flag)} {σ : List g.flag} {w : List T} (hder : g.Derives (g.expandRhs rhs σ) (List.map (fun (a : T) => ISym.terminal a) w)) : ∃ (kept : List (IRhsSymbol T g.nt g.flag)) (parts : List (List T)), g.NullableRhsSublist σ rhs kept ∧ w = parts.flatten ∧ List.Forall₂ (fun (s : IRhsSymbol T g.nt g.flag) (part : List T) => part ≠ [] ∧ g.Derives (g.expandRhs [s] σ) (List.map (fun (a : T) => ISym.terminal a) part)) kept parts

Branch-wise strengthening of exists_nullableRhsSublist_derives_to_terminals: every kept RHS symbol is assigned a nonempty terminal yield derived from that symbol.

theorem IndexedGrammar.exists_nullableRhsSublist_derivesIn_to_terminals_parts {T : Type} {g : IndexedGrammar T} {n : ℕ} {rhs : List (IRhsSymbol T g.nt g.flag)} {σ : List g.flag} {w : List T} (hder : g.DerivesIn n (g.expandRhs rhs σ) (List.map (fun (a : T) => ISym.terminal a) w)) : ∃ (kept : List (IRhsSymbol T g.nt g.flag)) (parts : List (ℕ × List T)), g.NullableRhsSublist σ rhs kept ∧ w = List.flatMap (fun (p : ℕ × List T) => p.2) parts ∧ (List.map (fun (p : ℕ × List T) => p.1) parts).sum ≤ n ∧ List.Forall₂ (fun (s : IRhsSymbol T g.nt g.flag) (p : ℕ × List T) => p.2 ≠ [] ∧ g.DerivesIn p.1 (g.expandRhs [s] σ) (List.map (fun (a : T) => ISym.terminal a) p.2)) kept parts

Counted branch-wise RHS pruning. Besides deleting nullable RHS nonterminals, this records a counted terminal yield for every kept symbol, and the kept budgets together do not exceed the original derivation budget.

theorem IndexedGrammar.exists_nonempty_nullableRhsSublist_derivesIn_to_terminals_parts {T : Type} {g : IndexedGrammar T} {n : ℕ} {rhs : List (IRhsSymbol T g.nt g.flag)} {σ : List g.flag} {w : List T} (hder : g.DerivesIn n (g.expandRhs rhs σ) (List.map (fun (a : T) => ISym.terminal a) w)) (hw : w ≠ []) : ∃ (kept : List (IRhsSymbol T g.nt g.flag)) (parts : List (ℕ × List T)), g.NullableRhsSublist σ rhs kept ∧ kept ≠ [] ∧ w = List.flatMap (fun (p : ℕ × List T) => p.2) parts ∧ (List.map (fun (p : ℕ × List T) => p.1) parts).sum ≤ n ∧ List.Forall₂ (fun (s : IRhsSymbol T g.nt g.flag) (p : ℕ × List T) => p.2 ≠ [] ∧ g.DerivesIn p.1 (g.expandRhs [s] σ) (List.map (fun (a : T) => ISym.terminal a) p.2)) kept parts

def IndexedGrammar.PrunedTransforms {T : Type} (g : IndexedGrammar T) (w₁ w₂ : List g.ISym) : Prop

One epsilon-pruned step: apply an original rule, but keep only a nonempty RHS sublist whose deleted nonterminals are nullable at the stack used by the rule application.

Equations

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

def IndexedGrammar.PrunedDerives {T : Type} (g : IndexedGrammar T) : List g.ISym → List g.ISym → Prop

Reflexive-transitive closure of epsilon-pruned indexed steps.

Equations

• g.PrunedDerives = Relation.ReflTransGen g.PrunedTransforms

theorem IndexedGrammar.prunedTransforms_length_le {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (hstep : g.PrunedTransforms w₁ w₂) : w₁.length ≤ w₂.length

theorem IndexedGrammar.prunedDerives_length_le {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (hder : g.PrunedDerives w₁ w₂) : w₁.length ≤ w₂.length

theorem IndexedGrammar.derives_of_prunedTransforms {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (hstep : g.PrunedTransforms w₁ w₂) : g.Derives w₁ w₂

theorem IndexedGrammar.derives_of_prunedDerives {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (hder : g.PrunedDerives w₁ w₂) : g.Derives w₁ w₂

theorem IndexedGrammar.prunedTransforms_with_prefix {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (u : List g.ISym) (hstep : g.PrunedTransforms w₁ w₂) : g.PrunedTransforms (u ++ w₁) (u ++ w₂)

theorem IndexedGrammar.prunedTransforms_with_suffix {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (v : List g.ISym) (hstep : g.PrunedTransforms w₁ w₂) : g.PrunedTransforms (w₁ ++ v) (w₂ ++ v)

theorem IndexedGrammar.prunedDerives_with_prefix {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (u : List g.ISym) (hder : g.PrunedDerives w₁ w₂) : g.PrunedDerives (u ++ w₁) (u ++ w₂)

theorem IndexedGrammar.prunedDerives_with_suffix {T : Type} {g : IndexedGrammar T} {w₁ w₂ : List g.ISym} (v : List g.ISym) (hder : g.PrunedDerives w₁ w₂) : g.PrunedDerives (w₁ ++ v) (w₂ ++ v)

theorem IndexedGrammar.prunedDerives_append {T : Type} {g : IndexedGrammar T} {u₁ u₂ v₁ v₂ : List g.ISym} (hu : g.PrunedDerives u₁ u₂) (hv : g.PrunedDerives v₁ v₂) : g.PrunedDerives (u₁ ++ v₁) (u₂ ++ v₂)

theorem IndexedGrammar.part_fst_le_sum_of_mem {T : Type} (parts : List (ℕ × List T)) {p : ℕ × List T} (hp : p ∈ parts) : p.1 ≤ (List.map (fun (q : ℕ × List T) => q.1) parts).sum

theorem IndexedGrammar.prunedDerives_expandRhs_to_terminals_of_forall₂_derivesIn {T : Type} {g : IndexedGrammar T} {N : ℕ} (hrec : ∀ {m : ℕ} {A : g.nt} {σ : List g.flag} {w : List T}, m < N → g.DerivesIn m [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) w) → w ≠ [] → g.PrunedDerives [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) w)) {σ : List g.flag} {kept : List (IRhsSymbol T g.nt g.flag)} {parts : List (ℕ × List T)} (hparts : List.Forall₂ (fun (s : IRhsSymbol T g.nt g.flag) (p : ℕ × List T) => p.2 ≠ [] ∧ g.DerivesIn p.1 (g.expandRhs [s] σ) (List.map (fun (a : T) => ISym.terminal a) p.2)) kept parts) (hlt : ∀ p ∈ parts, p.1 < N) : g.PrunedDerives (g.expandRhs kept σ) (List.map (fun (a : T) => ISym.terminal a) (List.flatMap (fun (p : ℕ × List T) => p.2) parts))

theorem IndexedGrammar.nullableRhsSublist_nil_of_expandRhs_derives_nil {T : Type} {g : IndexedGrammar T} {rhs : List (IRhsSymbol T g.nt g.flag)} {σ : List g.flag} (hder : g.Derives (g.expandRhs rhs σ) []) : g.NullableRhsSublist σ rhs []

theorem IndexedGrammar.exists_initial_rule_nullableRhsSublist_of_generates_nonempty {T : Type} {g : IndexedGrammar T} {w : List T} (hgen : g.Generates w) (hw : w ≠ []) : ∃ (r : IRule T g.nt g.flag) (kept : List (IRhsSymbol T g.nt g.flag)), r ∈ g.rules ∧ r.lhs = g.initial ∧ r.consume = none ∧ g.NullableRhsSublist [] r.rhs kept ∧ kept ≠ [] ∧ g.Derives (g.expandRhs kept []) (List.map (fun (a : T) => ISym.terminal a) w)

Every nonempty generated word has a first start-rule expansion whose nullable deletions leave a nonempty RHS deriving the same word.

theorem IndexedGrammar.exists_prunedTransforms_initial_of_generates_nonempty {T : Type} {g : IndexedGrammar T} {w : List T} (hgen : g.Generates w) (hw : w ≠ []) : ∃ (sent : List g.ISym), g.PrunedTransforms [ISym.indexed g.initial []] sent ∧ g.Derives sent (List.map (fun (a : T) => ISym.terminal a) w)

theorem IndexedGrammar.prunedDerives_indexed_to_terminals_of_derivesIn_nonempty {T : Type} {g : IndexedGrammar T} {n : ℕ} {A : g.nt} {σ : List g.flag} {w : List T} (hder : g.DerivesIn n [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) w)) (hw : w ≠ []) : g.PrunedDerives [ISym.indexed A σ] (List.map (fun (a : T) => ISym.terminal a) w)

theorem IndexedGrammar.prunedDerives_initial_of_generates_nonempty {T : Type} {g : IndexedGrammar T} {w : List T} (hgen : g.Generates w) (hw : w ≠ []) : g.PrunedDerives [ISym.indexed g.initial []] (List.map (fun (a : T) => ISym.terminal a) w)

Every nonempty generated word has a complete derivation using only ε-pruned steps.

theorem IndexedGrammar.ne_nil_of_prunedDerives_initial_to_terminals {T : Type} {g : IndexedGrammar T} {w : List T} (hder : g.PrunedDerives [ISym.indexed g.initial []] (List.map (fun (a : T) => ISym.terminal a) w)) : w ≠ []

A pruned derivation from the start symbol can only end in a nonempty terminal word.

theorem IndexedGrammar.prunedDerives_initial_to_terminals_iff_generates_nonempty {T : Type} {g : IndexedGrammar T} {w : List T} : g.PrunedDerives [ISym.indexed g.initial []] (List.map (fun (a : T) => ISym.terminal a) w) ↔ g.Generates w ∧ w ≠ []

Semantic ε-elimination: pruned derivations from the start generate exactly the nonempty part of the original language.

theorem IndexedGrammar.isNullable_cases_rule {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} (hnullable : g.IsNullable A σ) : (∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ g.Derives (g.expandRhs r.rhs σ) []) ∨ ∃ (f : g.flag) (ρ : List g.flag) (r : IRule T g.nt g.flag), σ = f :: ρ ∧ r ∈ g.rules ∧ r.lhs = A ∧ r.consume = some f ∧ g.Derives (g.expandRhs r.rhs ρ) []

First-step analysis for a nullable stacked nonterminal. Nullability is witnessed by a matching grammar rule whose expansion is nullable.

theorem IndexedGrammar.isNullable_of_derives_nullable {T : Type} {g : IndexedGrammar T} {A B : g.nt} {σ τ : List g.flag} (hder : g.Derives [ISym.indexed A σ] [ISym.indexed B τ]) (hnullable : g.IsNullable B τ) : g.IsNullable A σ

Nullability propagates backwards along a derivation.

theorem IndexedGrammar.isNullable_of_rule_derives_empty_none {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} {A : g.nt} {σ : List g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hconsume : r.consume = none) (hder : g.Derives (g.expandRhs r.rhs σ) []) : g.IsNullable A σ

If a non-consuming rule expands to a nullable sentential form, then its left-hand side is nullable at the same stack.

theorem IndexedGrammar.isNullable_of_rule_derives_empty_some {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} {A : g.nt} {f : g.flag} {σ : List g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hconsume : r.consume = some f) (hder : g.Derives (g.expandRhs r.rhs σ) []) : g.IsNullable A (f :: σ)

If a flag-consuming rule expands to a nullable sentential form, then its left-hand side is nullable when that flag is on top of the stack.

theorem IndexedGrammar.isNullable_iff_rule_derives_empty {T : Type} {g : IndexedGrammar T} {A : g.nt} {σ : List g.flag} : g.IsNullable A σ ↔ (∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ g.Derives (g.expandRhs r.rhs σ) []) ∨ ∃ (f : g.flag) (ρ : List g.flag) (r : IRule T g.nt g.flag), σ = f :: ρ ∧ r ∈ g.rules ∧ r.lhs = A ∧ r.consume = some f ∧ g.Derives (g.expandRhs r.rhs ρ) []

Rule-level characterization of nullable stacked nonterminals.

theorem IndexedGrammar.isNullable_cases_flagsSeparated {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) {A : g.nt} {σ : List g.flag} (hnullable : g.IsNullable A σ) : (∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = []) ∨ (∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs ≠ [] ∧ ∀ s ∈ r.rhs, ∃ (B : g.nt) (push : Option g.flag), s = IRhsSymbol.nonterminal B push ∧ g.IsNullable B (match push with | none => σ | some f => f :: σ)) ∨ ∃ (f : g.flag) (ρ : List g.flag) (r : IRule T g.nt g.flag) (B : g.nt), σ = f :: ρ ∧ r ∈ g.rules ∧ r.lhs = A ∧ r.consume = some f ∧ r.rhs = [IRhsSymbol.nonterminal B none] ∧ g.IsNullable B ρ

In a flag-separated grammar, nullability has three concrete sources: an explicit ε-rule, a non-consuming rule whose whole RHS is nullable at the inherited stack, or a pop rule whose single child is nullable after the pop.

theorem IndexedGrammar.isNullable_of_rule_all_nullable_none {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} {A : g.nt} {σ : List g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hconsume : r.consume = none) (hall : ∀ s ∈ r.rhs, ∃ (B : g.nt) (push : Option g.flag), s = IRhsSymbol.nonterminal B push ∧ g.IsNullable B (match push with | none => σ | some f => f :: σ)) : g.IsNullable A σ

A non-consuming rule whose expanded RHS is entirely nullable makes its LHS nullable.

theorem IndexedGrammar.isNullable_of_pop_rule_nullable_child {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} {A B : g.nt} {f : g.flag} {σ : List g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hconsume : r.consume = some f) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none]) (hB : g.IsNullable B σ) : g.IsNullable A (f :: σ)

A pop rule whose unique child is nullable after the pop makes its LHS nullable with the consumed flag on top of the stack.

theorem IndexedGrammar.isNullable_flagsSeparated_iff {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) {A : g.nt} {σ : List g.flag} : g.IsNullable A σ ↔ (∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = []) ∨ (∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs ≠ [] ∧ ∀ s ∈ r.rhs, ∃ (B : g.nt) (push : Option g.flag), s = IRhsSymbol.nonterminal B push ∧ g.IsNullable B (match push with | none => σ | some f => f :: σ)) ∨ ∃ (f : g.flag) (ρ : List g.flag) (r : IRule T g.nt g.flag) (B : g.nt), σ = f :: ρ ∧ r ∈ g.rules ∧ r.lhs = A ∧ r.consume = some f ∧ r.rhs = [IRhsSymbol.nonterminal B none] ∧ g.IsNullable B ρ

In a flag-separated grammar, nullability is exactly generated by explicit ε-rules, non-consuming all-nullable RHSs, and pop rules whose child is nullable after the pop.

theorem IndexedGrammar.isNullable_nil_iff_flagsSeparated {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) {A : g.nt} : g.IsNullable A [] ↔ (∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = []) ∨ ∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs ≠ [] ∧ ∀ s ∈ r.rhs, ∃ (B : g.nt) (push : Option g.flag), s = IRhsSymbol.nonterminal B push ∧ g.IsNullable B (match push with | none => [] | some f => [f])

Empty-stack specialization of the flag-separated nullability equations.

theorem IndexedGrammar.isNullable_cons_iff_flagsSeparated {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) {A : g.nt} {f : g.flag} {ρ : List g.flag} : g.IsNullable A (f :: ρ) ↔ (∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs = []) ∨ (∃ r ∈ g.rules, r.lhs = A ∧ r.consume = none ∧ r.rhs ≠ [] ∧ ∀ s ∈ r.rhs, ∃ (B : g.nt) (push : Option g.flag), s = IRhsSymbol.nonterminal B push ∧ g.IsNullable B (match push with | none => f :: ρ | some f' => f' :: f :: ρ)) ∨ ∃ (r : IRule T g.nt g.flag) (B : g.nt), r ∈ g.rules ∧ r.lhs = A ∧ r.consume = some f ∧ r.rhs = [IRhsSymbol.nonterminal B none] ∧ g.IsNullable B ρ

Nonempty-stack specialization of the flag-separated nullability equations.

theorem IndexedGrammar.isNullable_of_empty_rule_none {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} {A : g.nt} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hconsume : r.consume = none) (hrhs : r.rhs = []) (σ : List g.flag) : g.IsNullable A σ

An explicit rule A → ε makes A nullable at every stack.

theorem IndexedGrammar.isNullable_of_empty_rule_some {T : Type} {g : IndexedGrammar T} {r : IRule T g.nt g.flag} {A : g.nt} {f : g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hconsume : r.consume = some f) (hrhs : r.rhs = []) (σ : List g.flag) : g.IsNullable A (f :: σ)

An explicit rule Af → ε makes A nullable at every stack whose top flag is f.

def IndexedGrammar.NullableSet {T : Type} (g : IndexedGrammar T) : Set (g.nt × List g.flag)

The semantic set of nullable stacked nonterminals.

Equations

• g.NullableSet = {p : g.nt × List g.flag | g.IsNullable p.1 p.2}

def IndexedGrammar.NullableStep {T : Type} (g : IndexedGrammar T) (X : Set (g.nt × List g.flag)) : Set (g.nt × List g.flag)

One algebraic unfolding of stack-sensitive nullability for flag-separated grammars.

Equations

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

theorem IndexedGrammar.nullableStep_mono {T : Type} {g : IndexedGrammar T} {X Y : Set (g.nt × List g.flag)} (hXY : X ⊆ Y) : g.NullableStep X ⊆ g.NullableStep Y

theorem IndexedGrammar.nullableStep_sound {T : Type} {g : IndexedGrammar T} {X : Set (g.nt × List g.flag)} (hX : ∀ (A : g.nt) (σ : List g.flag), (A, σ) ∈ X → g.IsNullable A σ) : g.NullableStep X ⊆ g.NullableSet

theorem IndexedGrammar.nullableSet_subset_step_flagsSeparated {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) : g.NullableSet ⊆ g.NullableStep g.NullableSet

theorem IndexedGrammar.nullableStep_subset_nullableSet {T : Type} {g : IndexedGrammar T} : g.NullableStep g.NullableSet ⊆ g.NullableSet

theorem IndexedGrammar.nullableSet_fixedPoint_flagsSeparated {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) : g.NullableStep g.NullableSet = g.NullableSet

def IndexedGrammar.NullableApprox {T : Type} (g : IndexedGrammar T) : ℕ → Set (g.nt × List g.flag)

Finite unfoldings of the nullability equations, starting from no nullable states.

Equations

• g.NullableApprox 0 = ∅
• g.NullableApprox n.succ = g.NullableStep (g.NullableApprox n)

theorem IndexedGrammar.nullableApprox_sound {T : Type} (g : IndexedGrammar T) (n : ℕ) : g.NullableApprox n ⊆ g.NullableSet

theorem IndexedGrammar.nullableApprox_mono_succ {T : Type} (g : IndexedGrammar T) (n : ℕ) : g.NullableApprox n ⊆ g.NullableApprox (n + 1)

theorem IndexedGrammar.nullableApprox_mono {T : Type} (g : IndexedGrammar T) {m n : ℕ} (hmn : m ≤ n) : g.NullableApprox m ⊆ g.NullableApprox n

theorem IndexedGrammar.nullableApprox_complete_of_derivesIn_flagsSeparated {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) (n : ℕ) (A : g.nt) (σ : List g.flag) : g.DerivesIn n [ISym.indexed A σ] [] → (A, σ) ∈ g.NullableApprox (n + 1)

theorem IndexedGrammar.nullableSet_subset_iUnion_nullableApprox_flagsSeparated {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) : g.NullableSet ⊆ {p : g.nt × List g.flag | ∃ (n : ℕ), p ∈ g.NullableApprox n}

theorem IndexedGrammar.nullableSet_eq_iUnion_nullableApprox_flagsSeparated {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) : g.NullableSet = {p : g.nt × List g.flag | ∃ (n : ℕ), p ∈ g.NullableApprox n}

theorem IndexedGrammar.isNullable_iff_exists_nullableApprox_flagsSeparated {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) {A : g.nt} {σ : List g.flag} : g.IsNullable A σ ↔ ∃ (n : ℕ), (A, σ) ∈ g.NullableApprox n

inductive IndexedGrammar.ApproxNullableRhsSublist {T : Type} (g : IndexedGrammar T) (n : ℕ) (σ : List g.flag) : List (IRhsSymbol T g.nt g.flag) → List (IRhsSymbol T g.nt g.flag) → Prop

A RHS sublist whose deletions are justified by one finite nullable approximation rank.

• nil {T : Type} {g : IndexedGrammar T} {n : ℕ} {σ : List g.flag} : g.ApproxNullableRhsSublist n σ [] []
• keep {T : Type} {g : IndexedGrammar T} {n : ℕ} {σ : List g.flag} (s : IRhsSymbol T g.nt g.flag) {rhs kept : List (IRhsSymbol T g.nt g.flag)} (h : g.ApproxNullableRhsSublist n σ rhs kept) : g.ApproxNullableRhsSublist n σ (s :: rhs) (s :: kept)
• drop_none {T : Type} {g : IndexedGrammar T} {n : ℕ} {σ : List g.flag} {A : g.nt} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (hnullable : (A, σ) ∈ g.NullableApprox n) (h : g.ApproxNullableRhsSublist n σ rhs kept) : g.ApproxNullableRhsSublist n σ (IRhsSymbol.nonterminal A none :: rhs) kept
• drop_some {T : Type} {g : IndexedGrammar T} {n : ℕ} {σ : List g.flag} {A : g.nt} {f : g.flag} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (hnullable : (A, f :: σ) ∈ g.NullableApprox n) (h : g.ApproxNullableRhsSublist n σ rhs kept) : g.ApproxNullableRhsSublist n σ (IRhsSymbol.nonterminal A (some f) :: rhs) kept

theorem IndexedGrammar.ApproxNullableRhsSublist.toNullableRhsSublist {T : Type} {g : IndexedGrammar T} {n : ℕ} {σ : List g.flag} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (h : g.ApproxNullableRhsSublist n σ rhs kept) : g.NullableRhsSublist σ rhs kept

theorem IndexedGrammar.ApproxNullableRhsSublist.mono {T : Type} {g : IndexedGrammar T} {m n : ℕ} (hmn : m ≤ n) {σ : List g.flag} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (h : g.ApproxNullableRhsSublist m σ rhs kept) : g.ApproxNullableRhsSublist n σ rhs kept

theorem IndexedGrammar.exists_approxNullableRhsSublist_of_nullableRhsSublist_flagsSeparated {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) {σ : List g.flag} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (h : g.NullableRhsSublist σ rhs kept) : ∃ (n : ℕ), g.ApproxNullableRhsSublist n σ rhs kept

Relative nullable summaries

inductive IndexedGrammar.RelativeNullable {T : Type} (g : IndexedGrammar T) (base : Set g.nt) : List g.flag → g.nt → Prop

Nullability above an abstract suffix whose nullable nonterminals are given by base. RelativeNullable g base α A means that A is nullable on α ++ σ for every suffix σ whose nullable set is base.

• base {T : Type} {g : IndexedGrammar T} {base : Set g.nt} {A : g.nt} (hA : A ∈ base) : g.RelativeNullable base [] A
• empty_rule {T : Type} {g : IndexedGrammar T} {base : Set g.nt} {A : g.nt} {α : List g.flag} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hconsume : r.consume = none) (hrhs : r.rhs = []) : g.RelativeNullable base α A
• all_rule {T : Type} {g : IndexedGrammar T} {base : Set g.nt} {A : g.nt} {α : List g.flag} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hconsume : r.consume = none) (hrhs_ne : r.rhs ≠ []) (hterminal : ∀ (t : T), IRhsSymbol.terminal t ∉ r.rhs) (hall : ∀ (B : g.nt) (push : Option g.flag), IRhsSymbol.nonterminal B push ∈ r.rhs → g.RelativeNullable base (match push with | none => α | some f => f :: α) B) : g.RelativeNullable base α A
• pop_rule {T : Type} {g : IndexedGrammar T} {base : Set g.nt} {A B : g.nt} {f : g.flag} {α : List g.flag} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hconsume : r.consume = some f) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none]) (hB : g.RelativeNullable base α B) : g.RelativeNullable base (f :: α) A

theorem IndexedGrammar.RelativeNullable.sound {T : Type} {g : IndexedGrammar T} {base : Set g.nt} {σ α : List g.flag} {A : g.nt} (hbase : ∀ B ∈ base, g.IsNullable B σ) (h : g.RelativeNullable base α A) : g.IsNullable A (α ++ σ)

theorem IndexedGrammar.relativeNullable_complete_of_nullableApprox {T : Type} {g : IndexedGrammar T} {base : Set g.nt} {σ : List g.flag} (hbase : ∀ (B : g.nt), g.IsNullable B σ → B ∈ base) (n : ℕ) (α : List g.flag) (A : g.nt) : (A, α ++ σ) ∈ g.NullableApprox n → g.RelativeNullable base α A

theorem IndexedGrammar.RelativeNullable.complete_flagsSeparated {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) {base : Set g.nt} {σ α : List g.flag} {A : g.nt} (hbase : ∀ (B : g.nt), g.IsNullable B σ → B ∈ base) (hnullable : g.IsNullable A (α ++ σ)) : g.RelativeNullable base α A

theorem IndexedGrammar.relativeNullable_iff_flagsSeparated {T : Type} {g : IndexedGrammar T} (hfs : g.FlagsSeparated) {base : Set g.nt} {σ α : List g.flag} {A : g.nt} (hbase : ∀ (B : g.nt), B ∈ base ↔ g.IsNullable B σ) : g.RelativeNullable base α A ↔ g.IsNullable A (α ++ σ)

Finite-summary ε-elimination skeleton

def IndexedGrammar.stackSummaryEval {F Q : Type} (init : Q) (step : Q → F → Q) : List F → Q

Evaluate a finite stack summary. The transition step q f is the summary after pushing flag f on top of a stack with summary q.

Equations

• IndexedGrammar.stackSummaryEval init step [] = init
• IndexedGrammar.stackSummaryEval init step (f :: σ) = step (IndexedGrammar.stackSummaryEval init step σ) f

@[simp]

theorem IndexedGrammar.stackSummaryEval_nil {F Q : Type} (init : Q) (step : Q → F → Q) : stackSummaryEval init step [] = init

@[simp]

theorem IndexedGrammar.stackSummaryEval_cons {F Q : Type} (init : Q) (step : Q → F → Q) (f : F) (σ : List F) : stackSummaryEval init step (f :: σ) = step (stackSummaryEval init step σ) f

def IndexedGrammar.annotateStackWithSummary {F Q : Type} (init : Q) (step : Q → F → Q) : List F → List (F × Q)

Annotate every stack flag with the summary of the suffix below it.

Equations

• IndexedGrammar.annotateStackWithSummary init step [] = []
• IndexedGrammar.annotateStackWithSummary init step (f :: σ) = (f, IndexedGrammar.stackSummaryEval init step σ) :: IndexedGrammar.annotateStackWithSummary init step σ

@[simp]

theorem IndexedGrammar.annotateStackWithSummary_nil {F Q : Type} (init : Q) (step : Q → F → Q) : annotateStackWithSummary init step [] = []

@[simp]

theorem IndexedGrammar.annotateStackWithSummary_cons {F Q : Type} (init : Q) (step : Q → F → Q) (f : F) (σ : List F) : annotateStackWithSummary init step (f :: σ) = (f, stackSummaryEval init step σ) :: annotateStackWithSummary init step σ

@[simp]

theorem IndexedGrammar.map_fst_annotateStackWithSummary {F Q : Type} (init : Q) (step : Q → F → Q) (σ : List F) : List.map Prod.fst (annotateStackWithSummary init step σ) = σ

structure IndexedGrammar.NullableStackSummary {T : Type} (g : IndexedGrammar T) : Type 1

A finite stack summary recognizes exactly the nullable stacks when nullable_sound and nullable_complete are supplied later.

• state : Type
• instFintype : Fintype self.state
• init : self.state
• step : self.state → g.flag → self.state
• nullable : g.nt → self.state → Prop
• nullableDecidable (A : g.nt) (q : self.state) : Decidable (self.nullable A q)

def IndexedGrammar.NullableStackSummary.eval {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) : List g.flag → S.state

Equations

• S.eval = IndexedGrammar.stackSummaryEval S.init S.step

def IndexedGrammar.NullableStackSummary.annotateStack {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) : List g.flag → List (g.flag × S.state)

Equations

• S.annotateStack = IndexedGrammar.annotateStackWithSummary S.init S.step

@[simp]

theorem IndexedGrammar.NullableStackSummary.eval_nil {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) : S.eval [] = S.init

@[simp]

theorem IndexedGrammar.NullableStackSummary.eval_cons {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (f : g.flag) (σ : List g.flag) : S.eval (f :: σ) = S.step (S.eval σ) f

@[simp]

theorem IndexedGrammar.NullableStackSummary.map_fst_annotateStack {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (σ : List g.flag) : List.map Prod.fst (S.annotateStack σ) = σ

def IndexedGrammar.SummaryDroppableRhsSymbol {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (q : S.state) : IRhsSymbol T g.nt g.flag → Prop

A RHS symbol is droppable at summary state q when it is a nonterminal nullable at the stack summary it receives.

Equations

• IndexedGrammar.SummaryDroppableRhsSymbol S q (IRhsSymbol.terminal a) = False
• IndexedGrammar.SummaryDroppableRhsSymbol S q (IRhsSymbol.nonterminal A none) = S.nullable A q
• IndexedGrammar.SummaryDroppableRhsSymbol S q (IRhsSymbol.nonterminal A (some f)) = S.nullable A (S.step q f)

instance IndexedGrammar.summaryDroppableRhsSymbolDecidable {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (q : S.state) (s : IRhsSymbol T g.nt g.flag) : Decidable (SummaryDroppableRhsSymbol S q s)

Equations

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

inductive IndexedGrammar.SummaryNullableRhsSublist {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (q : S.state) : List (IRhsSymbol T g.nt g.flag) → List (IRhsSymbol T g.nt g.flag) → Prop

RHS sublist pruning justified by a finite stack summary.

• nil {T : Type} {g : IndexedGrammar T} {S : g.NullableStackSummary} {q : S.state} : SummaryNullableRhsSublist S q [] []
• keep {T : Type} {g : IndexedGrammar T} {S : g.NullableStackSummary} {q : S.state} (s : IRhsSymbol T g.nt g.flag) {rhs kept : List (IRhsSymbol T g.nt g.flag)} (h : SummaryNullableRhsSublist S q rhs kept) : SummaryNullableRhsSublist S q (s :: rhs) (s :: kept)
• drop {T : Type} {g : IndexedGrammar T} {S : g.NullableStackSummary} {q : S.state} {s : IRhsSymbol T g.nt g.flag} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (hdrop : SummaryDroppableRhsSymbol S q s) (h : SummaryNullableRhsSublist S q rhs kept) : SummaryNullableRhsSublist S q (s :: rhs) kept

def IndexedGrammar.summaryPrunedRhsList {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (q : S.state) : List (IRhsSymbol T g.nt g.flag) → List (List (IRhsSymbol T g.nt g.flag))

Enumerate all summary-justified RHS prunings.

Equations

• One or more equations did not get rendered due to their size.
• IndexedGrammar.summaryPrunedRhsList S q [] = [[]]

theorem IndexedGrammar.mem_summaryPrunedRhsList_iff {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (q : S.state) {rhs kept : List (IRhsSymbol T g.nt g.flag)} : kept ∈ summaryPrunedRhsList S q rhs ↔ SummaryNullableRhsSublist S q rhs kept

def IndexedGrammar.summaryLiftRhsSymbol {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (q : S.state) : IRhsSymbol T g.nt g.flag → IRhsSymbol T (g.nt × S.state) (g.flag × S.state)

Lift a kept RHS symbol into the summary grammar at current tail summary q. Pushed flags are annotated with the summary below the pushed flag.

Equations

• IndexedGrammar.summaryLiftRhsSymbol S q (IRhsSymbol.terminal a) = IRhsSymbol.terminal a
• IndexedGrammar.summaryLiftRhsSymbol S q (IRhsSymbol.nonterminal A none) = IRhsSymbol.nonterminal (A, q) none
• IndexedGrammar.summaryLiftRhsSymbol S q (IRhsSymbol.nonterminal A (some f)) = IRhsSymbol.nonterminal (A, S.step q f) (some (f, q))

def IndexedGrammar.summaryLiftRhs {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (q : S.state) (rhs : List (IRhsSymbol T g.nt g.flag)) : List (IRhsSymbol T (g.nt × S.state) (g.flag × S.state))

Equations

• IndexedGrammar.summaryLiftRhs S q rhs = List.map (IndexedGrammar.summaryLiftRhsSymbol S q) rhs

theorem IndexedGrammar.summaryLiftRhs_ne_nil {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (q : S.state) {rhs : List (IRhsSymbol T g.nt g.flag)} (hne : rhs ≠ []) : summaryLiftRhs S q rhs ≠ []

def IndexedGrammar.summaryRuleForKept {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (r : IRule T g.nt g.flag) (q : S.state) (kept : List (IRhsSymbol T g.nt g.flag)) : IRule T (g.nt × S.state) (g.flag × S.state)

Equations

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

noncomputable def IndexedGrammar.summaryRulesForRule {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (r : IRule T g.nt g.flag) : List (IRule T (g.nt × S.state) (g.flag × S.state))

Equations

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

noncomputable def IndexedGrammar.epsilonElimSummary {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) : IndexedGrammar T

Equations

• IndexedGrammar.epsilonElimSummary S = { nt := g.nt × S.state, flag := g.flag × S.state, initial := (g.initial, S.init), rules := List.flatMap (IndexedGrammar.summaryRulesForRule S) g.rules }

theorem IndexedGrammar.mem_summaryRulesForRule {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) {r : IRule T g.nt g.flag} {r' : IRule T (g.nt × S.state) (g.flag × S.state)} (hr' : r' ∈ summaryRulesForRule S r) : ∃ (q : S.state) (kept : List (IRhsSymbol T g.nt g.flag)), q ∈ Finset.univ.toList ∧ kept ∈ summaryPrunedRhsList S q r.rhs ∧ kept ≠ [] ∧ r' = summaryRuleForKept S r q kept

theorem IndexedGrammar.epsilonElimSummary_noEpsilon {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) : (epsilonElimSummary S).NoEpsilon'

def IndexedGrammar.summaryProjectISym {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) : (epsilonElimSummary S).ISym → g.ISym

Project an annotated-summary sentential symbol back to the original grammar.

Equations

• IndexedGrammar.summaryProjectISym S (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal t
• IndexedGrammar.summaryProjectISym S (IndexedGrammar.ISym.indexed A σ) = IndexedGrammar.ISym.indexed A.1 (List.map Prod.fst σ)

def IndexedGrammar.summaryProjectSF {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (w : List (epsilonElimSummary S).ISym) : List g.ISym

Equations

• IndexedGrammar.summaryProjectSF S w = List.map (IndexedGrammar.summaryProjectISym S) w

def IndexedGrammar.summaryLiftISym {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) : g.ISym → (epsilonElimSummary S).ISym

Lift an original sentential symbol with the correct stack summary and annotated flags.

Equations

• IndexedGrammar.summaryLiftISym S (IndexedGrammar.ISym.terminal t) = IndexedGrammar.ISym.terminal t
• IndexedGrammar.summaryLiftISym S (IndexedGrammar.ISym.indexed A σ) = IndexedGrammar.ISym.indexed (A, S.eval σ) (S.annotateStack σ)

def IndexedGrammar.summaryLiftSF {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (w : List g.ISym) : List (epsilonElimSummary S).ISym

Equations

• IndexedGrammar.summaryLiftSF S w = List.map (IndexedGrammar.summaryLiftISym S) w

@[simp]

theorem IndexedGrammar.summaryProjectISym_lift {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (s : g.ISym) : summaryProjectISym S (summaryLiftISym S s) = s

@[simp]

theorem IndexedGrammar.summaryProjectSF_lift {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (w : List g.ISym) : summaryProjectSF S (summaryLiftSF S w) = w

theorem IndexedGrammar.summaryProject_expandRhs_lift {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (q : S.state) (rhs : List (IRhsSymbol T g.nt g.flag)) (σ : List (g.flag × S.state)) : summaryProjectSF S ((epsilonElimSummary S).expandRhs (summaryLiftRhs S q rhs) σ) = g.expandRhs rhs (List.map Prod.fst σ)

theorem IndexedGrammar.SummaryNullableRhsSublist.toNullableRhsSublist_eval {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (hsound : ∀ (A : g.nt) (σ : List g.flag), S.nullable A (S.eval σ) → g.IsNullable A σ) {σ : List g.flag} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (h : SummaryNullableRhsSublist S (S.eval σ) rhs kept) : g.NullableRhsSublist σ rhs kept

Semantic soundness of summary-justified RHS deletion at an actually matching stack summary.

theorem IndexedGrammar.NullableRhsSublist.toSummary_eval {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (hcomplete : ∀ (A : g.nt) (σ : List g.flag), g.IsNullable A σ → S.nullable A (S.eval σ)) {σ : List g.flag} {rhs kept : List (IRhsSymbol T g.nt g.flag)} (h : g.NullableRhsSublist σ rhs kept) : SummaryNullableRhsSublist S (S.eval σ) rhs kept

Semantic completeness of summary-justified RHS deletion at an actually matching stack summary.

@[simp]

theorem IndexedGrammar.summaryLiftSF_nil {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) : summaryLiftSF S [] = []

@[simp]

theorem IndexedGrammar.summaryLiftSF_cons {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (s : g.ISym) (w : List g.ISym) : summaryLiftSF S (s :: w) = summaryLiftISym S s :: summaryLiftSF S w

@[simp]

theorem IndexedGrammar.summaryLiftSF_append {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (u v : List g.ISym) : summaryLiftSF S (u ++ v) = summaryLiftSF S u ++ summaryLiftSF S v

@[simp]

theorem IndexedGrammar.summaryLiftSF_terminals {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (w : List T) : summaryLiftSF S (List.map (fun (a : T) => ISym.terminal a) w) = List.map (fun (a : T) => ISym.terminal a) w

@[simp]

theorem IndexedGrammar.summaryProjectSF_terminals {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (w : List T) : summaryProjectSF S (List.map (fun (a : T) => ISym.terminal a) w) = List.map (fun (a : T) => ISym.terminal a) w

theorem IndexedGrammar.summaryLift_expandRhs_eval {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (rhs : List (IRhsSymbol T g.nt g.flag)) (σ : List g.flag) : (epsilonElimSummary S).expandRhs (summaryLiftRhs S (S.eval σ) rhs) (S.annotateStack σ) = summaryLiftSF S (g.expandRhs rhs σ)

theorem IndexedGrammar.summaryRuleForKept_mem_summaryRulesForRule {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) {r : IRule T g.nt g.flag} {q : S.state} {kept : List (IRhsSymbol T g.nt g.flag)} (hkeptMem : kept ∈ summaryPrunedRhsList S q r.rhs) (hkept : kept ≠ []) : summaryRuleForKept S r q kept ∈ summaryRulesForRule S r

theorem IndexedGrammar.summaryRuleForKept_mem_epsilonElimSummary_rules {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) {r : IRule T g.nt g.flag} {q : S.state} {kept : List (IRhsSymbol T g.nt g.flag)} (hr : r ∈ g.rules) (hkeptMem : kept ∈ summaryPrunedRhsList S q r.rhs) (hkept : kept ≠ []) : summaryRuleForKept S r q kept ∈ (epsilonElimSummary S).rules

def IndexedGrammar.SummaryWellAnnotatedISym {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) : (epsilonElimSummary S).ISym → Prop

The annotated summary carried by a nonterminal agrees with the summary of its stack, and each stack flag remembers the summary of the suffix below it.

Equations

• IndexedGrammar.SummaryWellAnnotatedISym S (IndexedGrammar.ISym.terminal t) = True
• IndexedGrammar.SummaryWellAnnotatedISym S (IndexedGrammar.ISym.indexed A σ) = (A.2 = S.eval (List.map Prod.fst σ) ∧ σ = S.annotateStack (List.map Prod.fst σ))

def IndexedGrammar.SummaryWellAnnotatedSF {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (w : List (epsilonElimSummary S).ISym) : Prop

Equations

• IndexedGrammar.SummaryWellAnnotatedSF S w = ∀ s ∈ w, IndexedGrammar.SummaryWellAnnotatedISym S s

theorem IndexedGrammar.summaryLiftISym_wellAnnotated {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (s : g.ISym) : SummaryWellAnnotatedISym S (summaryLiftISym S s)

theorem IndexedGrammar.summaryLiftSF_wellAnnotated {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (w : List g.ISym) : SummaryWellAnnotatedSF S (summaryLiftSF S w)

theorem IndexedGrammar.summaryWellAnnotated_expandRhs_lift {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) {q : S.state} {σ : List (g.flag × S.state)} (rhs : List (IRhsSymbol T g.nt g.flag)) (hq : q = S.eval (List.map Prod.fst σ)) (hσ : σ = S.annotateStack (List.map Prod.fst σ)) : SummaryWellAnnotatedSF S ((epsilonElimSummary S).expandRhs (summaryLiftRhs S q rhs) σ)

theorem IndexedGrammar.summaryTransforms_project_pruned_and_wellAnnotated {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (hsound : ∀ (A : g.nt) (σ : List g.flag), S.nullable A (S.eval σ) → g.IsNullable A σ) {w₁ w₂ : List (epsilonElimSummary S).ISym} (hwa : SummaryWellAnnotatedSF S w₁) (hstep : (epsilonElimSummary S).Transforms w₁ w₂) : g.PrunedTransforms (summaryProjectSF S w₁) (summaryProjectSF S w₂) ∧ SummaryWellAnnotatedSF S w₂

theorem IndexedGrammar.prunedDerives_project_of_summaryDerives {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (hsound : ∀ (A : g.nt) (σ : List g.flag), S.nullable A (S.eval σ) → g.IsNullable A σ) {w₁ w₂ : List (epsilonElimSummary S).ISym} (hder : (epsilonElimSummary S).Derives w₁ w₂) (hwa : SummaryWellAnnotatedSF S w₁) : g.PrunedDerives (summaryProjectSF S w₁) (summaryProjectSF S w₂) ∧ SummaryWellAnnotatedSF S w₂

theorem IndexedGrammar.prunedDerives_project_of_epsilonElimSummary_generates {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (hsound : ∀ (A : g.nt) (σ : List g.flag), S.nullable A (S.eval σ) → g.IsNullable A σ) {w : List T} (hgen : (epsilonElimSummary S).Generates w) : g.PrunedDerives [ISym.indexed g.initial []] (List.map (fun (a : T) => ISym.terminal a) w)

theorem IndexedGrammar.summaryTransforms_lift_of_prunedTransforms {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (hcomplete : ∀ (A : g.nt) (σ : List g.flag), g.IsNullable A σ → S.nullable A (S.eval σ)) {w₁ w₂ : List g.ISym} (hstep : g.PrunedTransforms w₁ w₂) : (epsilonElimSummary S).Transforms (summaryLiftSF S w₁) (summaryLiftSF S w₂)

theorem IndexedGrammar.summaryDerives_lift_of_prunedDerives {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (hcomplete : ∀ (A : g.nt) (σ : List g.flag), g.IsNullable A σ → S.nullable A (S.eval σ)) {w₁ w₂ : List g.ISym} (hder : g.PrunedDerives w₁ w₂) : (epsilonElimSummary S).Derives (summaryLiftSF S w₁) (summaryLiftSF S w₂)

theorem IndexedGrammar.epsilonElimSummary_generates_of_generates_nonempty {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (hcomplete : ∀ (A : g.nt) (σ : List g.flag), g.IsNullable A σ → S.nullable A (S.eval σ)) {w : List T} (hgen : g.Generates w) (hw : w ≠ []) : (epsilonElimSummary S).Generates w

theorem IndexedGrammar.generates_of_epsilonElimSummary_generates {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (hsound : ∀ (A : g.nt) (σ : List g.flag), S.nullable A (S.eval σ) → g.IsNullable A σ) {w : List T} (hgen : (epsilonElimSummary S).Generates w) : g.Generates w ∧ w ≠ []

theorem IndexedGrammar.epsilonElimSummary_generates_iff {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (hsound : ∀ (A : g.nt) (σ : List g.flag), S.nullable A (S.eval σ) → g.IsNullable A σ) (hcomplete : ∀ (A : g.nt) (σ : List g.flag), g.IsNullable A σ → S.nullable A (S.eval σ)) {w : List T} : (epsilonElimSummary S).Generates w ↔ g.Generates w ∧ w ≠ []

theorem IndexedGrammar.exists_noEpsilon_of_nullableStackSummary {T : Type} {g : IndexedGrammar T} (S : g.NullableStackSummary) (hsound : ∀ (A : g.nt) (σ : List g.flag), S.nullable A (S.eval σ) → g.IsNullable A σ) (hcomplete : ∀ (A : g.nt) (σ : List g.flag), g.IsNullable A σ → S.nullable A (S.eval σ)) : ∃ (g' : IndexedGrammar T), g'.NoEpsilon' ∧ ∀ (w : List T), w ≠ [] → (g'.Generates w ↔ g.Generates w)

noncomputable def IndexedGrammar.nullableSetAt {T : Type} (g : IndexedGrammar T) (σ : List g.flag) : Set g.nt

Equations

• g.nullableSetAt σ = {A : g.nt | g.IsNullable A σ}

def IndexedGrammar.relativeNullableStepSet {T : Type} (g : IndexedGrammar T) (base : Set g.nt) (f : g.flag) : Set g.nt

Equations

• g.relativeNullableStepSet base f = {A : g.nt | g.RelativeNullable base [f] A}

noncomputable def IndexedGrammar.nullableStackSummaryOfFinite {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : g.NullableStackSummary

Equations

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

theorem IndexedGrammar.nullableStackSummaryOfFinite_eval_iff {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (hfs : g.FlagsSeparated) (σ : List g.flag) (A : g.nt) : g.nullableStackSummaryOfFinite.nullable A (g.nullableStackSummaryOfFinite.eval σ) ↔ g.IsNullable A σ

theorem IndexedGrammar.nullableStackSummaryOfFinite_sound {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (hfs : g.FlagsSeparated) (A : g.nt) (σ : List g.flag) : g.nullableStackSummaryOfFinite.nullable A (g.nullableStackSummaryOfFinite.eval σ) → g.IsNullable A σ

theorem IndexedGrammar.nullableStackSummaryOfFinite_complete {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (hfs : g.FlagsSeparated) (A : g.nt) (σ : List g.flag) : g.IsNullable A σ → g.nullableStackSummaryOfFinite.nullable A (g.nullableStackSummaryOfFinite.eval σ)

theorem IndexedGrammar.exists_noEpsilon_of_fintype_flagsSeparated {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (hfs : g.FlagsSeparated) : ∃ (g' : IndexedGrammar T), g'.NoEpsilon' ∧ ∀ (w : List T), w ≠ [] → (g'.Generates w ↔ g.Generates w)

theorem IndexedGrammar.noEpsilon_iff_no_isNullable {T : Type} {g : IndexedGrammar T} : g.NoEpsilon' ↔ ∀ (A : g.nt) (σ : List g.flag), ¬g.IsNullable A σ

A grammar is ε-free exactly when no stacked nonterminal is nullable.

theorem IndexedGrammar.exists_noEpsilon_all {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') : ∃ (g' : IndexedGrammar T), g'.NoEpsilon' ∧ (g.StartNotOnRhs' → g'.StartNotOnRhs') ∧ ∀ (w : List T), g'.Generates w ↔ g.Generates w

If a grammar is already ε-free, it is an ε-free equivalent of itself.

theorem IndexedGrammar.exists_noEpsilon {T : Type} (g : IndexedGrammar T) (hne : g.NoEpsilon') : ∃ (g' : IndexedGrammar T), g'.NoEpsilon' ∧ (g.StartNotOnRhs' → g'.StartNotOnRhs') ∧ ∀ (w : List T), w ≠ [] → (g'.Generates w ↔ g.Generates w)