proposition: Lemma fold_le nt st (H : st <= fold_productions' (lookup_state fold_grammar) (opt.compile_productions (Lookup_string G nt))) : st <= lookup_state fold_grammar (of_nonterminal nt).
proof: Proof. unfold fold_grammar. rewrite pre_Fix_grammar_fixedpoint. unfold aggregate_step. rewrite lookup_state_aggregate_state_lub, <- least_upper_bound_correct_r. rewrite lookup_state_aggregate_prestep, (find_pre_Fix_grammar_to_lookup_state _ G). let v := match goal with |- context[if ?v then _ else _] => v end in destruct v eqn:Hvalid; unfold option_rect; [ | apply top_top ]. unfold step_constraints. unfold fixedpoint_by_abstract_interpretation at 3. unfold fold_constraints. erewrite eq_opt_Lookup_idx by (eassumption || reflexivity). rewrite <- list_to_productions_to_nonterminal. change (default_to_nonterminal ?nt) with (to_nonterminal nt). rewrite to_of_nonterminal by (eapply initial_nonterminals_correct; assumption). assumption. 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