Context-Free Splitting Lemmas #

This file proves decomposition lemmas for derivations that start from short lists of nonterminals.

Main declarations #

theorem head_tail_split {T : Type} {g : CF_grammar T} (x : List (symbol T g.nt)) (s : symbol T g.nt) (ss : List (symbol T g.nt)) (hyp : CF_derives g (s :: ss) x) :

∃ (u : List (symbol T g.nt)) (v : List (symbol T g.nt)), CF_derives g [s] u ∧ CF_derives g ss v ∧ u ++ v = x

If a list x is derived from a head symbol s followed by tail symbols ss, then x can be split into u (derived from s) and v (derived from ss).

theorem concatenation_can_be_split {T : Type} {g : CF_grammar T} (x : List (symbol T g.nt)) (s t : symbol T g.nt) (hyp : CF_derives g [s, t] x) :

∃ (u : List (symbol T g.nt)) (v : List (symbol T g.nt)), CF_derives g [s] u ∧ CF_derives g [t] v ∧ u ++ v = x

Corollary: derivation from two symbols can be split. This is a direct application of the more general head_tail_split lemma.

theorem concatenation_can_be_split_2 {T : Type} {g : CF_grammar T} (x : List (symbol T g.nt)) (s t t' : symbol T g.nt) (hyp : CF_derives g [s, t, t'] x) :

∃ (u : List (symbol T g.nt)) (v : List (symbol T g.nt)) (w : List (symbol T g.nt)), CF_derives g [s] u ∧ CF_derives g [t] v ∧ CF_derives g [t'] w ∧ u ++ v ++ w = x

Corollary: derivation from three symbols can be split. This is a direct application of the more general head_tail_split lemma.