Context-Free Language Closure Properties

This file proves that context-free languages are closed under substitution, and derives closure under concatenation, union, and Kleene star as corollaries. The proof follows the approach by Ullman and Hopcroft in "Introduction to Automata Theory, Languages and Computation".

The substitution grammar ContextFreeGrammar.subst g f is constructed by replacing each terminal a in g with the start symbol of f a, and adding all rules from every f a (for terminals actually used in g). The key technical lemma is that derivation steps from the two components commute: since F-rules (from the substituting grammars) never introduce nonterminals targeted by G-rules (from the original grammar), any mixed derivation can be reordered into a G-phase followed by an F-phase (ContextFreeGrammar.derives_commute_of_not_mem_output).

Main definitions

• ContextFreeGrammar.subst: The substitution of a context-free grammar g by a family of context-free grammars f.

Main theorems

• Language.IsContextFree.subst: Context-free languages are closed under substitution.
• Language.IsContextFree.mul: Context-free languages are closed under concatenation.
• Language.IsContextFree.add: Context-free languages are closed under union.
• Language.IsContextFree.kstar: Context-free languages are closed under Kleene star.

def ContextFreeGrammar.usedTerminals {α : Type} [DecidableEq α] (g : ContextFreeGrammar α) : Finset α

The set of terminals used in a context-free grammar g is the set of all terminals appearing in the right-hand side of any rule in g.

Equations

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

def ContextFreeGrammar.subst_rules_f {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] : Finset (ContextFreeRule β (g.NT ⊕ (a : α) × (f a).NT))

The rules from the substituting grammars f a are lifted to the combined non-terminal type g.NT ⊕ (Σ a, (f a).NT). We only include rules for terminals a that are actually used in g.

Equations

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

def ContextFreeGrammar.subst_rules_g {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) : Finset (ContextFreeRule β (g.NT ⊕ (a : α) × (f a).NT))

The rules of the original grammar g are transformed. Non-terminals n become Sum.inl n, and terminals a are replaced by the start symbol of the substituting grammar f a, which is Sum.inr ⟨a, (f a).initial⟩.

Equations

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

@[reducible]

def ContextFreeGrammar.subst {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] : ContextFreeGrammar β

The substitution grammar is constructed by taking the disjoint union of non-terminals and the union of the transformed rules from g and the lifted rules from f.

Equations

• g.subst f = { NT := g.NT ⊕ (a : α) × (f a).NT, initial := Sum.inl g.initial, rules := g.subst_rules_g f ∪ g.subst_rules_f f }

def ContextFreeGrammar.liftSymbolG {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) (s : Symbol α g.NT) : Symbol β (g.NT ⊕ (a : α) × (f a).NT)

liftSymbolG maps symbols from g to the substitution grammar. Non-terminals are mapped to the left component of the sum, and terminals are mapped to the start symbol of the corresponding substituting grammar.

Equations

• g.liftSymbolG f (Symbol.nonterminal n) = Symbol.nonterminal (Sum.inl n)
• g.liftSymbolG f (Symbol.terminal a) = Symbol.nonterminal (Sum.inr ⟨a, (f a).initial⟩)

def ContextFreeGrammar.liftSymbolF {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) (a : α) (s : Symbol β (f a).NT) : Symbol β (g.NT ⊕ (a : α) × (f a).NT)

liftSymbolF maps symbols from f a to the substitution grammar. Non-terminals are mapped to the right component of the sum, and terminals are kept as terminals.

Equations

• g.liftSymbolF f a (Symbol.nonterminal n) = Symbol.nonterminal (Sum.inr ⟨a, n⟩)
• g.liftSymbolF f a (Symbol.terminal b) = Symbol.terminal b

theorem ContextFreeGrammar.rule_mem_subst {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (r : ContextFreeRule α g.NT) (hr : r ∈ g.rules) : { input := Sum.inl r.input, output := List.map (g.liftSymbolG f) r.output } ∈ (g.subst f).rules

If r is in g.rules, then the lifted rule (non-terminals to Sum.inl, terminals to the start symbol of f a) is in the rules of g.subst f.

theorem ContextFreeGrammar.produces_lift_g {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] {u v : List (Symbol α g.NT)} (h : g.Produces u v) : (g.subst f).Produces (List.map (g.liftSymbolG f) u) (List.map (g.liftSymbolG f) v)

If g produces v from u in one step, then g.subst f produces the lifted version of v from the lifted version of u.

theorem ContextFreeGrammar.derives_lift_g {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] {u v : List (Symbol α g.NT)} (h : g.Derives u v) : (g.subst f).Derives (List.map (g.liftSymbolG f) u) (List.map (g.liftSymbolG f) v)

If g derives v from u, then g.subst f derives the lifted version of v from the lifted version of u.

theorem ContextFreeGrammar.rule_mem_subst_f {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (a : α) (ha : a ∈ g.usedTerminals) (r : ContextFreeRule β (f a).NT) (hr : r ∈ (f a).rules) : { input := Sum.inr ⟨a, r.input⟩, output := List.map (g.liftSymbolF f a) r.output } ∈ (g.subst f).rules

If a is a used terminal in g and r is a rule in f a, then the lifted rule (where non-terminals are tagged with a) is in the substitution grammar.

theorem ContextFreeGrammar.produces_lift_f {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (a : α) (ha : a ∈ g.usedTerminals) {u v : List (Symbol β (f a).NT)} (h : (f a).Produces u v) : (g.subst f).Produces (List.map (g.liftSymbolF f a) u) (List.map (g.liftSymbolF f a) v)

If a substituting grammar f a produces v from u, then the substitution grammar g.subst f produces the lifted version of v from the lifted version of u.

theorem ContextFreeGrammar.derives_lift_f {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (a : α) (ha : a ∈ g.usedTerminals) {u v : List (Symbol β (f a).NT)} (h : (f a).Derives u v) : (g.subst f).Derives (List.map (g.liftSymbolF f a) u) (List.map (g.liftSymbolF f a) v)

If a substituting grammar f a derives v from u, then the substitution grammar g.subst f derives the lifted version of v from the lifted version of u.

theorem ContextFreeGrammar.subst_derives_prod {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (u : List α) (W : List (List β)) (h : List.Forall₂ (fun (w : List β) (a : α) => w ∈ (f a).language) W u) (hu : ∀ a ∈ u, a ∈ g.usedTerminals) : (g.subst f).Derives (List.map (fun (a : α) => g.liftSymbolG f (Symbol.terminal a)) u) (List.map Symbol.terminal W.flatten)

If each W[i] is in (f u[i]).language, then g.subst f derives the concatenation of W from the lifted terminals of u.

theorem ContextFreeGrammar.mem_usedTerminals_of_rule_output {α : Type} [DecidableEq α] (g : ContextFreeGrammar α) (r : ContextFreeRule α g.NT) (hr : r ∈ g.rules) (a : α) (ha : Symbol.terminal a ∈ r.output) : a ∈ g.usedTerminals

If a terminal appears in the output of a rule in the grammar, it is in the set of used terminals.

theorem ContextFreeGrammar.terminals_of_produces {α : Type} [DecidableEq α] (g : ContextFreeGrammar α) {u v : List (Symbol α g.NT)} (h : g.Produces u v) (a : α) : Symbol.terminal a ∈ v → Symbol.terminal a ∈ u ∨ a ∈ g.usedTerminals

If g produces v from u, then any terminal in v is either in u or is a used terminal of g.

theorem ContextFreeGrammar.terminals_of_derives {α : Type} [DecidableEq α] (g : ContextFreeGrammar α) {u v : List (Symbol α g.NT)} (h : g.Derives u v) (a : α) : Symbol.terminal a ∈ v → Symbol.terminal a ∈ u ∨ a ∈ g.usedTerminals

If g derives v from u, then any terminal in v is either in u or is a used terminal of g.

theorem ContextFreeGrammar.usedTerminals_of_mem_language {α : Type} [DecidableEq α] (g : ContextFreeGrammar α) (w : List α) (hw : w ∈ g.language) (a : α) : a ∈ w → a ∈ g.usedTerminals

Any terminal in a string in the language of g must be a used terminal of g.

theorem ContextFreeGrammar.subst_language_subset_1 {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (w : List β) : (w ∈ g.language.subst fun (a : α) => (f a).language) → w ∈ (g.subst f).language

The substitution of the languages is a subset of the language of the substitution grammar.

theorem ContextFreeGrammar.mem_liftSymbolF_nonterminal_iff {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) (a : α) (u : List (Symbol β (f a).NT)) (x : g.NT ⊕ (a : α) × (f a).NT) : Symbol.nonterminal x ∈ List.map (g.liftSymbolF f a) u → ∃ (n : (f a).NT), x = Sum.inr ⟨a, n⟩

If a non-terminal symbol appears in a string lifted from f a, it must be of the form Sum.inr ⟨a, n⟩.

def ContextFreeGrammar.is_G_rule {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) (r : ContextFreeRule β (g.NT ⊕ (a : α) × (f a).NT)) : Prop

A rule is a G-rule if its input non-terminal comes from G (left side of the sum).

Equations

• g.is_G_rule f r = match r.input with | Sum.inl val => True | Sum.inr val => False

def ContextFreeGrammar.is_F_rule {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) (r : ContextFreeRule β (g.NT ⊕ (a : α) × (f a).NT)) : Prop

A rule is an F-rule if its input non-terminal comes from one of the F grammars (Sum.inr).

Equations

• g.is_F_rule f r = match r.input with | Sum.inl val => False | Sum.inr val => True

theorem ContextFreeGrammar.input_eq_of_rewrites_lifted {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) (a : α) (u : List (Symbol β (f a).NT)) (r : ContextFreeRule β (g.NT ⊕ (a : α) × (f a).NT)) (v : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h : r.Rewrites (List.map (g.liftSymbolF f a) u) v) : ∃ (n : (f a).NT), r.input = Sum.inr ⟨a, n⟩

If a rule rewrites a string lifted from f a, its input must be of the form Sum.inr ⟨a, n⟩.

theorem ContextFreeGrammar.liftSymbolF_injective {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) (a : α) : Function.Injective (g.liftSymbolF f a)

The function liftSymbolF is injective.

theorem ContextFreeGrammar.produces_lift_f_inv {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (a : α) (u : List (Symbol β (f a).NT)) (v' : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h : (g.subst f).Produces (List.map (g.liftSymbolF f a) u) v') : ∃ (v : List (Symbol β (f a).NT)), v' = List.map (g.liftSymbolF f a) v ∧ (f a).Produces u v

If g.subst f produces v' from a lifted string of f a symbols, then v' is a lifting of some v produced by f a.

def ContextFreeGrammar.ProducesG {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) (u v : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) : Prop

ProducesG is the relation of single-step productions using only G-rules.

Equations

• g.ProducesG f u v = ∃ r ∈ g.subst_rules_g f, r.Rewrites u v

def ContextFreeGrammar.ProducesF {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (u v : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) : Prop

ProducesF is the relation of single-step productions using only F-rules.

Equations

• g.ProducesF f u v = ∃ r ∈ g.subst_rules_f f, r.Rewrites u v

def ContextFreeGrammar.DerivesG {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) (u v : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) : Prop

DerivesG is the relation of derivations using only G-rules.

Equations

• g.DerivesG f u v = Relation.ReflTransGen (g.ProducesG f) u v

def ContextFreeGrammar.DerivesF {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (u v : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) : Prop

DerivesF is the relation of derivations using only F-rules.

Equations

• g.DerivesF f u v = Relation.ReflTransGen (g.ProducesF f) u v

theorem ContextFreeGrammar.derivesF_derivesG_commute {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (u v w : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h_F : g.DerivesF f u v) (h_G : g.DerivesG f v w) : ∃ (v' : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))), g.DerivesG f u v' ∧ g.DerivesF f v' w

If we have a sequence of F-productions followed by a sequence of G-productions, we can move all F-productions to the end. This is a corollary of derives_commute_of_not_mem_output: F-rules output only Sum.inr nonterminals, so they never introduce the Sum.inl inputs that G-rules target.

theorem ContextFreeGrammar.produces_subst_iff {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (u v : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) : (g.subst f).Produces u v ↔ g.ProducesG f u v ∨ g.ProducesF f u v

A production in the substitution grammar is either a G-production or an F-production.

theorem ContextFreeGrammar.derives_split_G_F {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (u w : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h : (g.subst f).Derives u w) : ∃ (v : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))), g.DerivesG f u v ∧ g.DerivesF f v w

Any derivation in the substitution grammar can be rearranged into a sequence of G-rules followed by a sequence of F-rules.

theorem ContextFreeGrammar.producesF_lift_f {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (a : α) (ha : a ∈ g.usedTerminals) {u v : List (Symbol β (f a).NT)} (h : (f a).Produces u v) : g.ProducesF f (List.map (g.liftSymbolF f a) u) (List.map (g.liftSymbolF f a) v)

If f a produces v from u, then g.subst f produces the lifted v from the lifted u using an F-rule.

theorem ContextFreeGrammar.producesG_unlift {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) (u : List (Symbol α g.NT)) (v' : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h : g.ProducesG f (List.map (g.liftSymbolG f) u) v') : ∃ (v : List (Symbol α g.NT)), v' = List.map (g.liftSymbolG f) v ∧ g.Produces u v

If g.subst f produces v' from a lifted u via a G-rule, then v' is a lifting of some v produced by g from u.

theorem ContextFreeGrammar.derivesG_unlift {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) (u : List (Symbol α g.NT)) (v' : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h : g.DerivesG f (List.map (g.liftSymbolG f) u) v') : ∃ (v : List (Symbol α g.NT)), v' = List.map (g.liftSymbolG f) v ∧ g.Derives u v

If g.subst f derives v' from a lifted u using only G-rules, then v' is a lifting of some v derived by g from u.

theorem ContextFreeGrammar.is_terminal_of_lift_no_inl {α β : Type} (g : ContextFreeGrammar α) (f : α → ContextFreeGrammar β) (u : List (Symbol α g.NT)) (h : ∀ s ∈ List.map (g.liftSymbolG f) u, ∀ (n : g.NT), s ≠ Symbol.nonterminal (Sum.inl n)) (s : Symbol α g.NT) : s ∈ u → ∃ (a : α), s = Symbol.terminal a

If the lifted string has no Sum.inl non-terminals, then the original string consists only of terminals.

theorem ContextFreeGrammar.producesF_unlift {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (a : α) (u : List (Symbol β (f a).NT)) (v' : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h : g.ProducesF f (List.map (g.liftSymbolF f a) u) v') : ∃ (v : List (Symbol β (f a).NT)), v' = List.map (g.liftSymbolF f a) v ∧ (f a).Produces u v

If g.subst f produces v' from a lifted u (from component a) via an F-rule, then v' is a lifting of some v produced by f a from u.

theorem ContextFreeGrammar.derivesF_unlift {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (a : α) (u : List (Symbol β (f a).NT)) (v' : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h : g.DerivesF f (List.map (g.liftSymbolF f a) u) v') : ∃ (v : List (Symbol β (f a).NT)), v' = List.map (g.liftSymbolF f a) v ∧ (f a).Derives u v

If g.subst f derives v' from a lifted u (from component a) using only F-rules, then v' is a lifting of some v derived by f a from u.

theorem ContextFreeGrammar.not_mem_inl_of_producesF {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (u v : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h : g.ProducesF f u v) (h_no_inl : ∀ s ∈ v, ∀ (n : g.NT), s ≠ Symbol.nonterminal (Sum.inl n)) (s : Symbol β (g.NT ⊕ (a : α) × (f a).NT)) : s ∈ u → ∀ (n : g.NT), s ≠ Symbol.nonterminal (Sum.inl n)

If an F-production results in a string with no Sum.inl non-terminals, then the input string also had no Sum.inl non-terminals.

theorem ContextFreeGrammar.subst_language_subset_1' {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (w : List β) : (w ∈ g.language.subst fun (a : α) => (f a).language) → w ∈ (g.subst f).language

The substitution of the languages is a subset of the language of the substitution grammar.

theorem ContextFreeGrammar.not_mem_inl_of_derivesF {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (u v : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h : g.DerivesF f u v) (h_no_inl : ∀ s ∈ v, ∀ (n : g.NT), s ≠ Symbol.nonterminal (Sum.inl n)) (s : Symbol β (g.NT ⊕ (a : α) × (f a).NT)) : s ∈ u → ∀ (n : g.NT), s ≠ Symbol.nonterminal (Sum.inl n)

If an F-derivation results in a string with no Sum.inl non-terminals, then the input string also had no Sum.inl non-terminals.

theorem ContextFreeGrammar.ProducesF.split_append {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (u v w : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h : g.ProducesF f (u ++ v) w) : (∃ (u' : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))), g.ProducesF f u u' ∧ w = u' ++ v) ∨ ∃ (v' : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))), g.ProducesF f v v' ∧ w = u ++ v'

If ProducesF transforms u ++ v to w, then the transformation occurs entirely within u or entirely within v.

theorem ContextFreeGrammar.DerivesF.split_append {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (u v w : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h : g.DerivesF f (u ++ v) w) : ∃ (u' : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (v' : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))), g.DerivesF f u u' ∧ g.DerivesF f v v' ∧ w = u' ++ v'

If DerivesF transforms u ++ v to w, then w splits into u' and v' such that u derives u' and v derives v' using only F-rules.

theorem ContextFreeGrammar.DerivesF_distrib {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (u w : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) (h : g.DerivesF f u w) : ∃ (W : List (List (Symbol β (g.NT ⊕ (a : α) × (f a).NT)))), w = W.flatten ∧ List.Forall₂ (fun (s : Symbol β (g.NT ⊕ (a : α) × (f a).NT)) (w' : List (Symbol β (g.NT ⊕ (a : α) × (f a).NT))) => g.DerivesF f [s] w') u W

If u derives w using F-rules, then w can be split into parts corresponding to each symbol in u.

theorem ContextFreeGrammar.DerivesF_terminal_of_lift {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (a : α) (w : List β) (h : g.DerivesF f [Symbol.nonterminal (Sum.inr ⟨a, (f a).initial⟩)] (List.map Symbol.terminal w)) : w ∈ (f a).language

If the lifted start symbol of f a F-derives a lifted terminal string w, then w ∈ (f a).language.

theorem ContextFreeGrammar.mem_subst_of_derivesF {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (u : List α) (w : List β) (h : g.DerivesF f (List.map (fun (a : α) => Symbol.nonterminal (Sum.inr ⟨a, (f a).initial⟩)) u) (List.map Symbol.terminal w)) : w ∈ (List.map (fun (a : α) => (f a).language) u).prod

If lifted start symbols of u F-derive a terminal string w, then w is in the product of the languages (f a).language for each a ∈ u.

theorem ContextFreeGrammar.subst_language_subset_2 {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] (w : List β) : w ∈ (g.subst f).language → w ∈ g.language.subst fun (a : α) => (f a).language

The language of the substitution grammar is a subset of the substitution of the languages.

theorem ContextFreeGrammar.subst_language_eq {α β : Type} [DecidableEq α] [DecidableEq β] (g : ContextFreeGrammar α) [DecidableEq g.NT] (f : α → ContextFreeGrammar β) [(a : α) → DecidableEq (f a).NT] : (g.subst f).language = g.language.subst fun (a : α) => (f a).language

The language of the substitution grammar is exactly the substitution of the languages of the component grammars. This proves that context-free languages are closed under substitution.

theorem Language.IsContextFree.subst {α β : Type} (L : Language α) (f : α → Language β) (hL : L.IsContextFree) (hf : ∀ (a : α), (f a).IsContextFree) : (L.subst f).IsContextFree

Context-free languages are closed under substitution.

Main corollaries: Closure under concatenation, union, and Kleene star

theorem isContextFree_singleton {α : Type} (w : List α) : {w}.IsContextFree

Singleton language is context-free

theorem isContextFree_pair_bool : {[false], [true]}.IsContextFree

Finite language {[false], [true]} is context-free

theorem isContextFree_univ_unit : Language.IsContextFree Set.univ

The universal language over Unit is context-free

theorem Language.IsContextFree.mul {α : Type} {L₁ L₂ : Language α} (h₁ : L₁.IsContextFree) (h₂ : L₂.IsContextFree) : (L₁ * L₂).IsContextFree

Context free languages are closed under concatenation / multiplication

theorem Language.IsContextFree.add {α : Type} {L₁ L₂ : Language α} (h₁ : L₁.IsContextFree) (h₂ : L₂.IsContextFree) : (L₁ + L₂).IsContextFree

Context free languages are closed under addition / union

theorem Language.IsContextFree.kstar {α : Type} {L : Language α} (h : L.IsContextFree) : (KStar.kstar L).IsContextFree

Context free languages are closed under the Kleene Star operation