proposition: Lemma fold_grammar_correct_production str ps (p : parse_of_production G str ps) : exists P, P str /\ related P (fold_production' (lookup_state fold_grammar) (opt.compile_production ps)).
proof: Proof. unfold fold_production'. induction p as [|str n pat pats p ps IHps]. { eexists; split; [ | apply on_nil_production_correct ]; assumption. } { simpl. apply fold_grammar_correct_item' in p. destruct IHps as [P [IHps0 IHps1]], p as [Ps [IHp0 IHp1]]. eexists; split; [ | apply combine_production_correct ]; hnf; eauto using ex_intro, conj with nocore. } Qed.
imports: Coq.Sets.Ensembles Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Fix.FromAbstractInterpretationDefinitions Fiat.Parsers.ContextFreeGrammar.Fix.Fix Fiat.Parsers.ContextFreeGrammar.Fix.Properties Fiat.Common