  Context-free grammar simplification is a subject of high importance in
computer language processing technology as well as in formal language theory.
This paper presents a formalization, using the Coq proof assistant, of the fact
that general context-free grammars generate languages that can be also
generated by simpler and equivalent context-free grammars. Namely, useless
symbol elimination, inaccessible symbol elimination, unit rules elimination and
empty rules elimination operations were described and proven correct with
respect to the preservation of the language generated by the original grammar.
